Mercurial Mercurial > repos > isabelle / 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.
tuned;
authorwenzelm
Thu, 01 Jun 2006 23:09:34 +0200
changeset 19758 093690d4ba60
parent 19757 4a2a71c31968
child 19759 2d0896653e7a
tuned;
src/LCF/LCF.thy file | annotate | diff | comparison | revisions 
--- a/src/LCF/LCF.thy	Thu Jun 01 23:07:51 2006 +0200
+++ b/src/LCF/LCF.thy	Thu Jun 01 23:09:34 2006 +0200
@@ -370,7 +370,8 @@
   shows "P(FIX(f),FIX(g))"
   apply (rule FIX1 [THEN ssubst, of _ f g])
   apply (rule FIX2 [THEN ssubst, of _ f g])
-  apply (rule induct [OF 1, where ?f = "%x. <f(FST(x)),g(SND(x))>"])
+  apply (rule induct [where ?f = "%x. <f(FST(x)),g(SND(x))>"])
+  apply (rule 1)
   apply simp
   apply (rule 2)
   apply (simp add: expand_all_PROD)
isabelle