changeset 47236 | 973ab740a25d |
parent 46493 | 7e69b9f3149f |
child 54567 | cfe53047dc16 |
--- a/src/Pure/assumption.ML Fri Mar 30 21:08:00 2012 +0200 +++ b/src/Pure/assumption.ML Sat Mar 31 15:21:35 2012 +0200 @@ -56,7 +56,7 @@ datatype data = Data of {assms: (export * cterm list) list, (*assumes: A ==> _*) - prems: thm list}; (*prems: A |- A*) + prems: thm list}; (*prems: A |- norm_hhf A*) fun make_data (assms, prems) = Data {assms = assms, prems = prems};