Mercurial Mercurial > hg > nominal2 / 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
authorChristian Urban <urbanc@in.tum.de>
Fri, 22 Jul 2011 11:52:12 +0100
changeset 2983 4436039cc5e1
parent 2982 4a00077c008f
child 2984 1b39ba5db2c1
child 2985 05ccb61aa628
tuned
Nominal/nominal_mutual.ML file | annotate | diff | comparison | revisions 
--- a/Nominal/nominal_mutual.ML	Fri Jul 22 11:37:16 2011 +0100
+++ b/Nominal/nominal_mutual.ML	Fri Jul 22 11:52:12 2011 +0100
@@ -306,6 +306,7 @@
     val ([p_name], ctxt') = Variable.variant_fixes ["p"] ctxt
     val p = Free (p_name, @{typ perm})
 
+    (* extracting the acc-premises from the induction theorems *)
     val acc_prems = 
      map prop_of induct_thms
      |> map2 forall_elim_list argss
nominal2