--- 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>
--- 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}
--- 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