--- a/src/HOL/ex/Multiquote.thy Thu Feb 01 20:43:59 2001 +0100
+++ b/src/HOL/ex/Multiquote.thy Thu Feb 01 20:44:19 2001 +0100
@@ -41,8 +41,8 @@
text {* advanced examples *}
term ".(.(\<acute>\<acute>x + \<acute>y).)."
-term ".(.(\<acute>\<acute>x + \<acute>y). o \<acute>f)."
-term ".(\<acute>(f o \<acute>g))."
-term ".(.( \<acute>\<acute>(f o \<acute>g) ).)."
+term ".(.(\<acute>\<acute>x + \<acute>y). \<circ> \<acute>f)."
+term ".(\<acute>(f \<circ> \<acute>g))."
+term ".(.( \<acute>\<acute>(f \<circ> \<acute>g) ).)."
end
--- a/src/HOL/ex/StringEx.thy Thu Feb 01 20:43:59 2001 +0100
+++ b/src/HOL/ex/StringEx.thy Thu Feb 01 20:44:19 2001 +0100
@@ -1,3 +1,5 @@
+
+header {* String examples *}
theory StringEx = Main:
--- a/src/Pure/Isar/README Thu Feb 01 20:43:59 2001 +0100
+++ b/src/Pure/Isar/README Thu Feb 01 20:44:19 2001 +0100
@@ -4,6 +4,7 @@
This directory contains the Isabelle/Isar subsystem -- Intelligible
Semi-Automated Reasoning for Isabelle. Interesting modules include:
+ ProofContext (structure of Isar proof contexts)
Proof (core of the Isar/VM interpreter)
Args (concrete argument syntax of attributes and methods)
Method (proof methods)
@@ -11,7 +12,7 @@
LocalDefs (local definitions)
Calculation (calculational proofs)
- ObtainFun (generalized existence reasoning)
+ Obtain (generalized existence reasoning)
Toplevel (the Isabelle/Isar toplevel)
IsarThy (Isar derived theory operations)