# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1322164441 0
# Node ID 3778bddfb824ede5ad41e4c78b0de18b1c171d8e
# Parent  80eb66aefc665e25281423110347e6ee89e3c57f
updated to Isabelle 24 November

diff -r 80eb66aefc66 -r 3778bddfb824 ProgTutorial/First_Steps.thy
--- a/ProgTutorial/First_Steps.thy	Sat Nov 12 11:45:39 2011 +0000
+++ b/ProgTutorial/First_Steps.thy	Thu Nov 24 19:54:01 2011 +0000
@@ -938,9 +938,13 @@
   val parser = Args.context -- Scan.lift Args.name_source
 
   fun typ_pat (ctxt, str) =
-     str |> Syntax.parse_typ ctxt
-         |> ML_Syntax.print_typ
-         |> ML_Syntax.atomic
+    let
+      val ctxt' = Proof_Context.set_mode Proof_Context.mode_schematic ctxt
+    in 
+      str |> Syntax.read_typ ctxt'
+          |> ML_Syntax.print_typ
+          |> ML_Syntax.atomic
+      end
 in
   ML_Antiquote.inline @{binding "typ_pat"} (parser >> typ_pat)
 end*}
diff -r 80eb66aefc66 -r 3778bddfb824 ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Sat Nov 12 11:45:39 2011 +0000
+++ b/ProgTutorial/Tactical.thy	Thu Nov 24 19:54:01 2011 +0000
@@ -1406,12 +1406,11 @@
   \begin{isabelle}
   \begin{tabular}{l@ {\hspace{10mm}}l}
   @{ML_ind addsimps in Raw_Simplifier}    & @{ML_ind delsimps in Raw_Simplifier}\\
-  @{ML_ind addcongs in Raw_Simplifier}    & @{ML_ind delcongs in Raw_Simplifier}\\
   @{ML_ind addsimprocs in Raw_Simplifier} & @{ML_ind delsimprocs in Raw_Simplifier}\\
+  @{ML_ind add_cong in Raw_Simplifier}    & @{ML_ind del_cong in Raw_Simplifier}\\
   \end{tabular}
   \end{isabelle}
 
-  \footnote{\bf FIXME: What about splitters? @{ML addsplits}, @{ML delsplits}}
 *}
 
 text_raw {*
@@ -1476,7 +1475,7 @@
   Adding also the congruence rule @{thm [source] UN_cong} 
 *}
 
-ML{*val ss2 = ss1 addcongs [@{thm UN_cong} RS @{thm eq_reflection}] *}
+ML{*val ss2 = Simplifier.add_cong (@{thm UN_cong} RS @{thm eq_reflection}) ss1 *}
 
 text {*
   gives
diff -r 80eb66aefc66 -r 3778bddfb824 progtutorial.pdf
Binary file progtutorial.pdf has changed