merged

--- a/Admin/build	Wed Mar 14 17:19:08 2012 +0000
+++ b/Admin/build	Wed Mar 14 17:19:30 2012 +0000
@@ -23,9 +23,10 @@
   Produce Isabelle distribution modules from current repository sources.
   The MODULES list may contain any of the following:
 
-    all             all modules below
+    all             all modules below *except* doc-src
     browser         graph browser (requires jdk)
     doc             documentation (requires latex and rail)
+    doc-src         documentation sources from Isabelle theories
     jars            Isabelle/Scala layer (requires Scala in \$SCALA_HOME)
     jars_fresh      fresh build of jars
 
@@ -82,6 +83,25 @@
 }
 
 
+function build_doc-src ()
+{
+  echo "###"
+  echo "### Building documentation sources..."
+  echo "###"
+
+  cd "$ISABELLE_HOME/doc-src"
+  for DOC in $(cat Dirs)
+  do
+    pushd "$DOC" >/dev/null
+    if [[ -f "IsaMakefile" ]]
+    then
+      "$ISABELLE_TOOL" make || exit $?
+    fi
+    popd >/dev/null
+  done
+}
+
+
 function build_jars ()
 {
   pushd "$ISABELLE_HOME/src/Pure" >/dev/null
@@ -98,6 +118,7 @@
     all) build_all;;
     browser) build_browser;;
     doc) build_doc;;
+    doc-src) build_doc-src;;
     jars) build_jars;;
     jars_fresh) build_jars -f;;
     *) fail "Bad module $MODULE"

--- a/Admin/makedist	Wed Mar 14 17:19:08 2012 +0000
+++ b/Admin/makedist	Wed Mar 14 17:19:30 2012 +0000
@@ -4,7 +4,7 @@
 
 ## global settings
 
-REPOS_NAME="${REPOS_NAME:-isabelle}"
+REPOS_NAME="isabelle"
 REPOS="${REPOS:-http://isabelle.in.tum.de/repos/${REPOS_NAME}}"
 DISTPREFIX="${DISTPREFIX:-~/tmp/isadist}"
 
@@ -94,8 +94,14 @@
 echo "### Retrieving Mercurial repository $VERSION"
 echo "###"
 
-{ wget -q "$REPOS/archive/${VERSION}.tar.gz" -O- | tar -xzf -; } || \
-  fail "Failed to retrieve $VERSION"
+if expr match "$REPOS" "https\?://" > /dev/null
+then
+  { wget -q "$REPOS/archive/${VERSION}.tar.gz" -O- | tar -xzf -; } || \
+    fail "Failed to retrieve $VERSION"
+else
+  { hg --repository "$REPOS" archive --type tgz - | tar -xzf -; } || \
+    fail "Failed to retrieve $VERSION"
+fi
 
 IDENT=$(echo * | sed "s/${REPOS_NAME}-//")
 
@@ -224,5 +230,4 @@
 
 rm -rf "${DISTNAME}-old"
 
-
 echo "DONE"

--- a/Admin/mira.py	Wed Mar 14 17:19:08 2012 +0000
+++ b/Admin/mira.py	Wed Mar 14 17:19:30 2012 +0000
@@ -17,6 +17,7 @@
 from mira.tools import tool
 from mira import schedule, misc
 from mira.environment import scheduler
+from mira import repositories
 
 # build and evaluation tools
 
@@ -256,6 +257,21 @@
     """HOL image"""
     return build_isabelle_image('HOL', 'Pure', 'HOL', *args)
 
+@configuration(repos = [Isabelle], deps = [(HOL, [0])])
+def HOL_Library(*args):
+    """HOL-Library image"""
+    return build_isabelle_image('HOL', 'HOL', 'HOL-Library', *args)
+
+@configuration(repos = [Isabelle], deps = [(Pure, [0])])
+def ZF(*args):
+    """ZF image"""
+    return build_isabelle_image('ZF', 'Pure', 'ZF', *args)
+
+@configuration(repos = [Isabelle], deps = [(HOL, [0])])
+def HOL_HOLCF(*args):
+    """HOLCF image"""
+    return build_isabelle_image('HOL/HOLCF', 'HOL', 'HOLCF', *args)
+
 @configuration(repos = [Isabelle], deps = [(Pure_64, [0])])
 def HOL_64(*args):
     """HOL image (64 bit)"""
@@ -292,6 +308,40 @@
     return isabelle_makeall(*args)
 
 
+# distribution and documentation Build
+
+@configuration(repos = [Isabelle], deps = [])
+def Distribution(env, case, paths, dep_paths, playground):
+    """Build of distribution"""
+    ## FIXME This is rudimentary; study Admin/CHECKLIST to complete this configuration accordingly
+    isabelle_home = paths[0]
+    (return_code, log) = env.run_process(path.join(isabelle_home, 'Admin', 'makedist'),
+      REPOS = repositories.get(Isabelle).local_path, DISTPREFIX = os.getcwd())
+    return (return_code == 0, '', ## FIXME might add summary here
+      {}, {'log': log}, None) ## FIXME might add proper result here
+
+@configuration(repos = [Isabelle], deps = [
+    (HOL, [0]),
+    (HOL_HOLCF, [0]),
+    (ZF, [0]),
+    (HOL_Library, [0])
+  ])
+def Documentation_images(*args):
+    """Isabelle images needed to build the documentation"""
+    return isabelle_dependency_only(*args)
+
+@configuration(repos = [Isabelle], deps = [(Documentation_images, [0])])
+def Documentation(env, case, paths, dep_paths, playground):
+    """Build of documentation"""
+    isabelle_home = paths[0]
+    dep_path = dep_paths[0]
+    prepare_isabelle_repository(isabelle_home, env.settings.contrib, dep_path,
+      usedir_options = default_usedir_options)
+    (return_code, log) = env.run_process(path.join(isabelle_home, 'Admin', 'build', 'doc-src'))
+    return (return_code == 0, extract_isabelle_run_summary(log),
+      extract_report_data(isabelle_home, log), {'log': log}, None)
+
+
 # Mutabelle configurations
 
 def invoke_mutabelle(theory, env, case, paths, dep_paths, playground):

--- a/doc-src/TutorialI/CTL/CTL.thy	Wed Mar 14 17:19:08 2012 +0000
+++ b/doc-src/TutorialI/CTL/CTL.thy	Wed Mar 14 17:19:30 2012 +0000
@@ -370,11 +370,11 @@
 
 lemma "lfp(eufix A B) \<subseteq> eusem A B"
 apply(rule lfp_lowerbound)
-apply(auto simp add: eusem_def eufix_def);
- apply(rule_tac x = "[]" in exI);
+apply(auto simp add: eusem_def eufix_def)
+ apply(rule_tac x = "[]" in exI)
  apply simp
-apply(rule_tac x = "y#xc" in exI);
-apply simp;
+apply(rule_tac x = "xa#xb" in exI)
+apply simp
 done
 
 lemma mono_eufix: "mono(eufix A B)";