# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1322180825 0
# Node ID 1d1165432c9f50d32ac38dfbd05d198e6594d872
# Parent  3778bddfb824ede5ad41e4c78b0de18b1c171d8e# Parent  615780a701b6de75457159a1d2e2759961be94f5
merged

diff -r 615780a701b6 -r 1d1165432c9f ProgTutorial/First_Steps.thy
--- a/ProgTutorial/First_Steps.thy	Thu Nov 17 16:33:49 2011 +0000
+++ b/ProgTutorial/First_Steps.thy	Fri Nov 25 00:27:05 2011 +0000
@@ -941,9 +941,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 615780a701b6 -r 1d1165432c9f ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Thu Nov 17 16:33:49 2011 +0000
+++ b/ProgTutorial/Tactical.thy	Fri Nov 25 00:27:05 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 615780a701b6 -r 1d1165432c9f progtutorial.pdf
Binary file progtutorial.pdf has changed