author | wenzelm |
Sat, 31 Mar 2012 15:21:35 +0200 | |
changeset 47236 | 973ab740a25d |
parent 47235 | a92d3620e156 |
child 47237 | b61a11dea74c |
--- 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};