# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1238402030 -3600
# Node ID 7e04dc2368b060ed6522c2a94570aacfe4fe1171
# Parent  e60dbcba719d161f63d555eca656fb4f8aa17279
updated to latest Isabelle

diff -r e60dbcba719d -r 7e04dc2368b0 ProgTutorial/Solutions.thy
--- a/ProgTutorial/Solutions.thy	Mon Mar 30 08:17:22 2009 +0000
+++ b/ProgTutorial/Solutions.thy	Mon Mar 30 09:33:50 2009 +0100
@@ -65,7 +65,7 @@
   val sum = HOLogic.mk_number @{typ "nat"} (n1 + n2)
   val goal = Logic.mk_equals (t, sum)
 in
-  Goal.prove ctxt [] [] goal (K (arith_tac ctxt 1))
+  Goal.prove ctxt [] [] goal (K (Arith_Data.arith_tac ctxt 1))
 end
 
 fun add_sp_aux ss t =
diff -r e60dbcba719d -r 7e04dc2368b0 ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Mon Mar 30 08:17:22 2009 +0000
+++ b/ProgTutorial/Tactical.thy	Mon Mar 30 09:33:50 2009 +0100
@@ -1644,7 +1644,7 @@
   val num = HOLogic.mk_number @{typ "nat"} n
   val goal = Logic.mk_equals (t, num)
 in
-  Goal.prove ctxt [] [] goal (K (arith_tac ctxt 1))
+  Goal.prove ctxt [] [] goal (K (Arith_Data.arith_tac ctxt 1))
 end*}
 
 text {*
@@ -1652,7 +1652,8 @@
   @{text num} (Line 3), and then generates the meta-equation @{text "t \<equiv> num"} 
   (Line 4), which it proves by the arithmetic tactic in Line 6. 
 
-  For our purpose at the moment, proving the meta-equation using @{ML arith_tac} is
+  For our purpose at the moment, proving the meta-equation using 
+  @{ML Arith_Data.arith_tac} is
   fine, but there is also an alternative employing the simplifier with a very
   restricted simpset. For the kind of lemmas we want to prove, the simpset
   @{text "num_ss"} in the code will suffice.
@@ -1671,7 +1672,7 @@
 text {*
   The advantage of @{ML get_thm_alt} is that it leaves very little room for 
   something to go wrong; in contrast it is much more difficult to predict 
-  what happens with @{ML arith_tac}, especially in more complicated 
+  what happens with @{ML Arith_Data.arith_tac}, especially in more complicated 
   circumstances. The disatvantage of @{ML get_thm_alt} is to find a simpset
   that is sufficiently powerful to solve every instance of the lemmas
   we like to prove. This requires careful tuning, but is often necessary in 
diff -r e60dbcba719d -r 7e04dc2368b0 progtutorial.pdf
Binary file progtutorial.pdf has changed