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

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

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

Binary file progtutorial.pdf has changed