tuned
authorwenzelm
Thu Feb 01 20:44:19 2001 +0100 (2001-02-01)
changeset 11020646c929b6293
parent 11019 e968e5bfe98d
child 11021 41de937d338b
tuned
src/HOL/ex/Multiquote.thy
src/HOL/ex/StringEx.thy
src/Pure/Isar/README
     1.1 --- a/src/HOL/ex/Multiquote.thy	Thu Feb 01 20:43:59 2001 +0100
     1.2 +++ b/src/HOL/ex/Multiquote.thy	Thu Feb 01 20:44:19 2001 +0100
     1.3 @@ -41,8 +41,8 @@
     1.4  
     1.5  text {* advanced examples *}
     1.6  term ".(.(\<acute>\<acute>x + \<acute>y).)."
     1.7 -term ".(.(\<acute>\<acute>x + \<acute>y). o \<acute>f)."
     1.8 -term ".(\<acute>(f o \<acute>g))."
     1.9 -term ".(.( \<acute>\<acute>(f o \<acute>g) ).)."
    1.10 +term ".(.(\<acute>\<acute>x + \<acute>y). \<circ> \<acute>f)."
    1.11 +term ".(\<acute>(f \<circ> \<acute>g))."
    1.12 +term ".(.( \<acute>\<acute>(f \<circ> \<acute>g) ).)."
    1.13  
    1.14  end
     2.1 --- a/src/HOL/ex/StringEx.thy	Thu Feb 01 20:43:59 2001 +0100
     2.2 +++ b/src/HOL/ex/StringEx.thy	Thu Feb 01 20:44:19 2001 +0100
     2.3 @@ -1,3 +1,5 @@
     2.4 +
     2.5 +header {* String examples *}
     2.6  
     2.7  theory StringEx = Main:
     2.8  
     3.1 --- a/src/Pure/Isar/README	Thu Feb 01 20:43:59 2001 +0100
     3.2 +++ b/src/Pure/Isar/README	Thu Feb 01 20:44:19 2001 +0100
     3.3 @@ -4,6 +4,7 @@
     3.4  This directory contains the Isabelle/Isar subsystem -- Intelligible
     3.5  Semi-Automated Reasoning for Isabelle.  Interesting modules include:
     3.6  
     3.7 +  ProofContext  (structure of Isar proof contexts)
     3.8    Proof		(core of the Isar/VM interpreter)
     3.9    Args		(concrete argument syntax of attributes and methods)
    3.10    Method	(proof methods)
    3.11 @@ -11,7 +12,7 @@
    3.12  
    3.13    LocalDefs	(local definitions)
    3.14    Calculation	(calculational proofs)
    3.15 -  ObtainFun     (generalized existence reasoning)
    3.16 +  Obtain        (generalized existence reasoning)
    3.17  
    3.18    Toplevel	(the Isabelle/Isar toplevel)
    3.19    IsarThy	(Isar derived theory operations)