Mercurial Mercurial > hg > tm / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
thys/recursive.thy
changeset 130 1e89c65f844b
parent 129 c3832c4963c4
child 131 e995ae949731 
--- a/thys/recursive.thy	Wed Feb 06 03:37:26 2013 +0000
+++ b/thys/recursive.thy	Wed Feb 06 04:11:06 2013 +0000
@@ -4868,7 +4868,7 @@
 
 lemma recursive_compile_to_tm_correct3: 
   assumes "rec_calc_rel recf args r"
-  shows "\<exists> m n. {\<lambda>tp. tp = ([Bk, Bk], <args>)} tm_of_rec recf {\<lambda>tp. tp = (Bk \<up> m, <r> @ Bk \<up> n)}"
+  shows "{\<lambda>tp. tp = ([Bk, Bk], <args>)} tm_of_rec recf {\<lambda>tp. \<exists>k l. tp = (Bk \<up> k, <r> @ Bk \<up> l)}"
 using recursive_compile_to_tm_correct2[OF _ assms] 
 apply(auto)
 apply(case_tac "rec_ci recf")
tm