# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1329316409 0
# Node ID 500d1abbc98c87b9a1062d1ccf35ffdad2f21c6b
# Parent  caa7331904544bbafb49da779a7089f6d212b1ea
updated to Isabelle 15 Feb

diff -r caa733190454 -r 500d1abbc98c ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Mon Jan 16 07:40:17 2012 +0000
+++ b/ProgTutorial/Tactical.thy	Wed Feb 15 14:33:29 2012 +0000
@@ -796,7 +796,7 @@
   "\<lbrakk>?P2; ?Q1\<rbrakk> \<Longrightarrow> (?P2 \<or> ?Q2) \<and> (?P1 \<or> ?Q1)"}
 
   If you need to instantiate lists of theorems, you can use the
-  functions @{ML_ind RL in Drule} and @{ML_ind MRL in Drule}. For 
+  functions @{ML_ind RL in Drule} and @{ML_ind OF in Drule}. For 
   example in the code below, every theorem in the second list is 
   instantiated with every theorem in the first.
 
diff -r caa733190454 -r 500d1abbc98c progtutorial.pdf
Binary file progtutorial.pdf has changed