tuned comment;
authorwenzelm
Sat, 31 Mar 2012 15:21:35 +0200
changeset 47236 973ab740a25d
parent 47235 a92d3620e156
child 47237 b61a11dea74c
tuned comment;
src/Pure/assumption.ML
--- 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};