Mercurial Mercurial > hg > nominal2 / 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.
FSet.thy
changeset 221 f219011a5e3c
parent 219 329111e1c4ba
child 225 9b8e039ae960 
--- a/FSet.thy	Wed Oct 28 15:25:36 2009 +0100
+++ b/FSet.thy	Wed Oct 28 16:05:59 2009 +0100
@@ -306,8 +306,12 @@
   apply (metis)
   done
 
+ML {* (atomize_thm @{thm list_induct_hol4}) *}
+
+ML {* regularise (prop_of (atomize_thm @{thm list_induct_hol4})) @{typ "'a list"} @{term "op \<approx>"} @{context} *}
+
 prove list_induct_r: {*
-   build_regularize_goal (atomize_thm @{thm list_induct_hol4}) @{typ "'a List.list"} @{term "op \<approx>"} @{context} *}
+   build_regularize_goal (atomize_thm @{thm list_induct_hol4}) @{typ "'a list"} @{term "op \<approx>"} @{context} *}
   apply (simp only: equiv_res_forall[OF equiv_list_eq])
   thm RIGHT_RES_FORALL_REGULAR
   apply (rule RIGHT_RES_FORALL_REGULAR)
nominal2