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.
fixed 'txt';
authorwenzelm
Sat, 03 Jul 1999 00:22:53 +0200
changeset 6890 05732285677e
parent 6889 adcf91ad5add
child 6891 7bb02d03035d
fixed 'txt';
src/Pure/Isar/isar_syn.ML file | annotate | diff | comparison | revisions
src/Pure/Isar/isar_thy.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/isar_syn.ML	Sat Jul 03 00:21:35 1999 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sat Jul 03 00:22:53 1999 +0200
@@ -44,7 +44,7 @@
 (** formal comments **)
 
 val txtP = OuterSyntax.command "txt" "formal comment (proof)" K.prf_decl
-  (P.comment >> (Toplevel.proof o IsarThy.add_txt));
+  (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_txt)));
 
 val textP = OuterSyntax.command "text" "formal comment (theory)" K.thy_decl
   (P.comment >> (Toplevel.theory o IsarThy.add_text));
--- a/src/Pure/Isar/isar_thy.ML	Sat Jul 03 00:21:35 1999 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Sat Jul 03 00:22:53 1999 +0200
@@ -156,7 +156,7 @@
 
 (* formal comments *)
 
-fun add_txt comment prf = prf;
+fun add_txt comment = ProofHistory.apply Proof.assert_forward;
 fun add_text comment thy = thy;
 fun add_title title author date thy = thy;
 val add_chapter = add_text;
isabelle