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 add_sect etc.;
authorwenzelm
Tue, 24 Aug 1999 11:50:34 +0200
changeset 7332 60534b9018ae
parent 7331 aee8f76fe54c
child 7333 6cb15c6f1d9f
fixed add_sect etc.;
src/Pure/Isar/isar_thy.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/isar_thy.ML	Tue Aug 24 11:50:17 1999 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Tue Aug 24 11:50:34 1999 +0200
@@ -160,7 +160,7 @@
 
 (* formal comments *)
 
-fun add_text comment thy = thy;
+fun add_text comment thy = thy:theory;
 fun add_title title author date thy = thy;
 val add_chapter = add_text;
 val add_section = add_text;
@@ -168,9 +168,9 @@
 val add_subsubsection = add_text;
 
 fun add_txt comment = ProofHistory.apply Proof.assert_forward;
-val add_sect = add_text;
-val add_subsect = add_text;
-val add_subsubsect = add_text;
+val add_sect = add_txt;
+val add_subsect = add_txt;
+val add_subsubsect = add_txt;
 
 
 (* signature and syntax *)
isabelle