# HG changeset patch
# User wenzelm
# Date 1451229602 -3600
# Node ID 3c8c390a8f0a4ed648062aa576ca3f159fad481d
# Parent  e1205f814159868a79f600eaecc372c402468a80
tuned document;

diff -r e1205f814159 -r 3c8c390a8f0a src/HOL/Isar_Examples/Schroeder_Bernstein.thy
--- a/src/HOL/Isar_Examples/Schroeder_Bernstein.thy	Sun Dec 27 16:00:41 2015 +0100
+++ b/src/HOL/Isar_Examples/Schroeder_Bernstein.thy	Sun Dec 27 16:20:02 2015 +0100
@@ -10,7 +10,7 @@
 
 text \<open>
   See also:
-  \<^item> @{file "~~/src/HOL/ex/Set_Theory.thy"}
+  \<^item> @{file "$ISABELLE_HOME/src/HOL/ex/Set_Theory.thy"}
   \<^item> @{url "http://planetmath.org/proofofschroederbernsteintheoremusingtarskiknastertheorem"}
   \<^item> Springer LNCS 828 (cover page)
 \<close>
diff -r e1205f814159 -r 3c8c390a8f0a src/HOL/Isar_Examples/document/root.tex
--- a/src/HOL/Isar_Examples/document/root.tex	Sun Dec 27 16:00:41 2015 +0100
+++ b/src/HOL/Isar_Examples/document/root.tex	Sun Dec 27 16:20:02 2015 +0100
@@ -1,4 +1,5 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[utf8]{inputenc}
 \usepackage[only,bigsqcap]{stmaryrd}
 \usepackage{ifthen,proof,amssymb,isabelle,isabellesym}
 \isabellestyle{it}
diff -r e1205f814159 -r 3c8c390a8f0a src/HOL/ROOT
--- a/src/HOL/ROOT	Sun Dec 27 16:00:41 2015 +0100
+++ b/src/HOL/ROOT	Sun Dec 27 16:20:02 2015 +0100
@@ -624,25 +624,25 @@
   description {*
     Miscellaneous Isabelle/Isar examples.
   *}
+  options [quick_and_dirty]
   theories [document = false]
     "~~/src/HOL/Library/Lattice_Syntax"
     "../Number_Theory/Primes"
-  theories [quick_and_dirty]
-    Structured_Statements
   theories
-    Basic_Logic
+    Knaster_Tarski
+    Peirce
+    Drinker
     Cantor
     Schroeder_Bernstein
-    Drinker
+    Structured_Statements
+    Basic_Logic
     Expr_Compiler
     Fibonacci
     Group
     Group_Context
     Group_Notepad
     Hoare_Ex
-    Knaster_Tarski
     Mutilated_Checkerboard
-    Peirce
     Puzzle
     Summation
     First_Order_Logic