Mercurial Mercurial > repos > isabelle / 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 message;
authorwenzelm
Wed, 10 Jun 2015 11:52:54 +0200
changeset 60413 0824fd1e9c40
parent 60412 285c7ff27728
child 60414 f25f2f2ba48c
tuned message;
src/Pure/Isar/proof_context.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/proof_context.ML	Wed Jun 10 11:14:46 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Jun 10 11:52:54 2015 +0200
@@ -1385,12 +1385,12 @@
         else [Pretty.block (Pretty.str "fixed variables:" :: Pretty.brk 1 ::
           Pretty.commas (map prt_fix fixes))];
 
-      (*prems*)
-      val prt_prems =
+      (*assumptions*)
+      val prt_assms =
         (case Assumption.all_prems_of ctxt of
           [] => []
-        | prems => [Pretty.big_list "prems:" [pretty_fact ctxt ("", prems)]]);
-    in prt_structs @ prt_fixes @ prt_prems end;
+        | prems => [Pretty.big_list "assumptions:" [pretty_fact ctxt ("", prems)]]);
+    in prt_structs @ prt_fixes @ prt_assms end;
 
 
 (* main context *)
isabelle