Fixed: NameError: name 'locale_encoding' is not defined File /bin/rst2html.py, line 17, in <module> from docutils.core import publish_cmdline, default_description File /usr/lib/python2.7/site-packages/docutils/core.py, line 20, in <module> from docutils import frontend, io, utils, readers, writers File /usr/lib/python2.7/site-packages/docutils/frontend.py, line 41, in <module> import docutils.utils File /usr/lib/python2.7/site-packages/docutils/utils/__init__.py, line 20, in <module> import docutils.io File /usr/lib/python2.7/site-packages/docutils/io.py, line 18, in <module> from docutils.utils.error_reporting import locale_encoding, ErrorString, ErrorOutput File /usr/lib/python2.7/site-packages/docutils/utils/error_reporting.py, line 60, in <module> codecs.lookup(locale_encoding or '') # None -> '' NameError: name 'locale_encoding' is not defined

     1

.. -*- coding: utf-8; -*-

     2

     3

===========

     4

 Isabelle.

     5

===========

     6

.. contents::

     7

   :local:

     8

     9

Prepare user work dir.

    10

======================

    11

::

    12

    13

  $ cd ~/isabelle

    14

  $ isatool mkdir HOL my-proof-dir

    15