# HG changeset patch
# User wenzelm
# Date 981056659 -3600
# Node ID 646c929b629315e99ee54827340789194573d2e2
# Parent  e968e5bfe98db776b66f3f1cb1ed0620d59acc63
tuned

diff -r e968e5bfe98d -r 646c929b6293 src/HOL/ex/Multiquote.thy
--- 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
diff -r e968e5bfe98d -r 646c929b6293 src/HOL/ex/StringEx.thy
--- 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:
 
diff -r e968e5bfe98d -r 646c929b6293 src/Pure/Isar/README
--- 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)