Mercurial Mercurial > hg > isabelle-cookbook / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authorChristian Urban <urbanc@in.tum.de>
Wed, 15 Feb 2012 14:47:46 +0000
changeset 511 386375b7a22a
parent 510 500d1abbc98c (diff)
parent 509 dcefee89bf62 (current diff)
child 512 231ec0c45bff
merged
ProgTutorial/Tactical.thy file | annotate | diff | comparison | revisions
progtutorial.pdf file | annotate | diff | comparison | revisions 
--- 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.
 
Binary file progtutorial.pdf has changed
isabelle-cookbook