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/nominal_mutual.ML
changeset 2983 4436039cc5e1
parent 2982 4a00077c008f
child 3045 d0ad264f8c4f 
--- 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