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.
Nominal/Nominal2.thy
changeset 2474 6e37bfb62474
parent 2471 894599a50af3
child 2475 486d4647bb37 
--- a/Nominal/Nominal2.thy	Sun Sep 05 06:42:53 2010 +0800
+++ b/Nominal/Nominal2.thy	Sun Sep 05 07:00:19 2010 +0800
@@ -539,6 +539,8 @@
       ||>> lift_thms qtys [] raw_exhaust_thms
     else raise TEST lthyA
 
+  val qinducts = Project_Rule.projections lthyA qinduct
+
   (* supports lemmas *) 
   val qsupports_thms =
     if get_STEPS lthy > 28
@@ -573,6 +575,7 @@
      ||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", []), qfv_qbn_eqvts) 
      ||>> Local_Theory.note ((thms_suffix "size_eqvt", []), qsize_eqvt)
      ||>> Local_Theory.note ((thms_suffix "induct", []), [qinduct]) 
+     ||>> Local_Theory.note ((thms_suffix "inducts", []), qinducts) 
      ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts)
      ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms)
      ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms)
nominal2