# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1329317266 0
# Node ID 386375b7a22abbc3b20429aa93625e34484e8d2c
# Parent  500d1abbc98c87b9a1062d1ccf35ffdad2f21c6b# Parent  dcefee89bf62bd69f4fc0763efbf8b790ea59a18
merged

diff -r dcefee89bf62 -r 386375b7a22a ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Sat Jan 21 15:35:47 2012 +0000
+++ b/ProgTutorial/Tactical.thy	Wed Feb 15 14:47:46 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 dcefee89bf62 -r 386375b7a22a progtutorial.pdf
Binary file progtutorial.pdf has changed