# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1396523816 -3600
# Node ID 638ed040e6f8b59d3b0c30526643aa13788b11a5
# Parent  c53d74b34123779dcfb05f8071bdbf4b5a6b8c6e
updated

diff -r c53d74b34123 -r 638ed040e6f8 ProgTutorial/Essential.thy
--- a/ProgTutorial/Essential.thy	Thu Mar 13 17:16:49 2014 +0000
+++ b/ProgTutorial/Essential.thy	Thu Apr 03 12:16:56 2014 +0100
@@ -192,8 +192,8 @@
   where a coercion is inserted in the second component and 
 
   @{ML_response [display,gray] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})" 
-  "(Const (\"==>\", \<dots>) $ \<dots> $ \<dots>, 
- Const (\"==>\", \<dots>) $ \<dots> $ \<dots>)"}
+  "(Const (\"Pure.imp\", \<dots>) $ \<dots> $ \<dots>, 
+ Const (\"Pure.imp\", \<dots>) $ \<dots> $ \<dots>)"}
 
   where it is not (since it is already constructed by a meta-implication). 
   The purpose of the @{text "Trueprop"}-coercion is to embed formulae of
diff -r c53d74b34123 -r 638ed040e6f8 ProgTutorial/First_Steps.thy
--- a/ProgTutorial/First_Steps.thy	Thu Mar 13 17:16:49 2014 +0000
+++ b/ProgTutorial/First_Steps.thy	Thu Apr 03 12:16:56 2014 +0100
@@ -856,7 +856,7 @@
   of this antiquotation is that it does not allow you to use schematic
   variables in terms. If you want to have an antiquotation that does not have
   this restriction, you can implement your own using the function @{ML_ind
-  inline in ML_Antiquote} from the structure @{ML_struct ML_Antiquote}. The code
+  inline in ML_Antiquotation} from the structure @{ML_struct ML_Antiquotation}. The code
   for the antiquotation @{text "term_pat"} is as follows.
 *}
 
@@ -869,7 +869,7 @@
          |> ML_Syntax.print_term
          |> ML_Syntax.atomic
 in
-  ML_Antiquote.inline @{binding "term_pat"} (parser >> term_pat)
+  ML_Antiquotation.inline @{binding "term_pat"} (parser >> term_pat)
 end*}
 
 text {*
@@ -906,7 +906,7 @@
           |> ML_Syntax.atomic
       end
 in
-  ML_Antiquote.inline @{binding "typ_pat"} (parser >> typ_pat)
+  ML_Antiquotation.inline @{binding "typ_pat"} (parser >> typ_pat)
 end*}
 
 text {*
@@ -921,9 +921,9 @@
   code harder to read, than making it easier. 
 
   \begin{readmore}
-  The file @{ML_file "Pure/ML/ml_antiquote.ML"} contains the the definitions
-  for most antiquotations. Most of the basic operations on ML-syntax are implemented 
-  in @{ML_file "Pure/ML/ml_syntax.ML"}.
+  The files @{ML_file "Pure/ML/ml_antiquotation.ML"} and @{ML_file "Pure/ML/ml_antiquotations.ML"}
+  contain the infrastructure and definitions for most antiquotations. Most of the basic operations 
+  on ML-syntax are implemented in @{ML_file "Pure/ML/ml_syntax.ML"}.
   \end{readmore}
 *}
 
diff -r c53d74b34123 -r 638ed040e6f8 ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Thu Mar 13 17:16:49 2014 +0000
+++ b/ProgTutorial/Tactical.thy	Thu Apr 03 12:16:56 2014 +0100
@@ -250,7 +250,7 @@
   form @{text "C \<Longrightarrow> #C"}; when the proof is finished we are left with @{text
   "#C"}. Since the goal @{term C} can potentially be an implication, there is a
   ``protector'' wrapped around it (the wrapper is the outermost constant
-  @{text "Const (\"prop\", bool \<Rightarrow> bool)"}; in the figure we make it visible
+  @{text "Const (\"Pure.prop\", bool \<Rightarrow> bool)"}; in the figure we make it visible
   as a @{text #}). This wrapper prevents that premises of @{text C} are
   misinterpreted as open subgoals. While tactics can operate on the subgoals
   (the @{text "A\<^sub>i"} above), they are expected to leave the conclusion
@@ -264,7 +264,7 @@
   \begin{boxedminipage}{\textwidth}
   \begin{isabelle}
 *}
-notation (output) "prop"  ("#_" [1000] 1000)
+notation (output) "Pure.prop"  ("#_" [1000] 1000)
 
 lemma 
   shows "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B" 
@@ -1483,10 +1483,10 @@
 
   \footnote{\bf FIXME: Why does it print out ??.unknown}
 
-  Adding also the congruence rule @{thm [source] UN_cong} 
+  Adding also the congruence rule @{thm [source] strong_INF_cong} 
 *}
 
-ML %grayML{*val ss2 = ss1 |> Simplifier.add_cong (@{thm UN_cong} RS @{thm eq_reflection}) *}
+ML %grayML{*val ss2 = ss1 |> Simplifier.add_cong (@{thm strong_INF_cong} RS @{thm eq_reflection}) *}
 
 text {*
   gives
@@ -1496,7 +1496,8 @@
 "Simplification rules:
   ??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)
 Congruences rules:
-  UNION: \<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> C x = D x\<rbrakk> \<Longrightarrow> \<Union>x\<in>A. C x \<equiv> \<Union>x\<in>B. D x
+  Complete_Lattices.Inf_class.INFIMUM: 
+    \<lbrakk>A1 = B1; \<And>x. x \<in> B1 =simp=> C1 x = D1 x\<rbrakk> \<Longrightarrow> INFIMUM A1 C1 \<equiv> INFIMUM B1 D1
 Simproc patterns:"}
 
   Notice that we had to add these lemmas as meta-equations. The @{ML empty_ss} 
@@ -2116,7 +2117,7 @@
 in
   Thm.prop_of (Thm.beta_conversion true ctrm)
 end"
-"Const (\"==\",\<dots>) $ 
+"Const (\"Pure.eq\",\<dots>) $ 
   (Abs (\"x\",\<dots>,Abs (\"y\",\<dots>,\<dots>)) $\<dots>$\<dots>) $ 
     (Const (\"Groups.plus_class.plus\",\<dots>) $ \<dots> $ \<dots>)"} 
 
diff -r c53d74b34123 -r 638ed040e6f8 progtutorial.pdf
Binary file progtutorial.pdf has changed