# HG changeset patch
# User wenzelm
# Date 930920685 -7200
# Node ID 7d0f7ad5a35fd6915afb896756052758ad599daa
# Parent  1dcac1789759f1a30608f64a494e9530959412ff
added 'txt';

diff -r 1dcac1789759 -r 7d0f7ad5a35f src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Jul 02 15:04:31 1999 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Fri Jul 02 15:04:45 1999 +0200
@@ -41,11 +41,12 @@
 
 
 
-(** theory sections **)
+(** formal comments **)
 
-(* formal comments *)
+val txtP = OuterSyntax.command "txt" "formal comment (proof)" K.prf_decl
+  (P.comment >> (Toplevel.proof o IsarThy.add_txt));
 
-val textP = OuterSyntax.command "text" "formal comments" K.thy_decl
+val textP = OuterSyntax.command "text" "formal comment (theory)" K.thy_decl
   (P.comment >> (Toplevel.theory o IsarThy.add_text));
 
 val titleP = OuterSyntax.command "title" "document title" K.thy_heading
@@ -65,6 +66,9 @@
   (P.comment >> (Toplevel.theory o IsarThy.add_subsubsection));
 
 
+
+(** theory sections **)
+
 (* classes and sorts *)
 
 val classesP =
@@ -545,12 +549,12 @@
   (*theory structure*)
   theoryP, end_excursionP, kill_excursionP, contextP, update_contextP,
   (*theory sections*)
-  textP, titleP, chapterP, sectionP, subsectionP, subsubsectionP,
-  classesP, classrelP, defaultsortP, typedeclP, typeabbrP, nontermP,
-  aritiesP, constsP, syntaxP, translationsP, axiomsP, defsP,
-  constdefsP, theoremsP, lemmasP, globalP, localP, pathP, useP, mlP,
-  setupP, parse_ast_translationP, parse_translationP,
-  print_translationP, typed_print_translationP,
+  txtP, textP, titleP, chapterP, sectionP, subsectionP,
+  subsubsectionP, classesP, classrelP, defaultsortP, typedeclP,
+  typeabbrP, nontermP, aritiesP, constsP, syntaxP, translationsP,
+  axiomsP, defsP, constdefsP, theoremsP, lemmasP, globalP, localP,
+  pathP, useP, mlP, setupP, parse_ast_translationP,
+  parse_translationP, print_translationP, typed_print_translationP,
   print_ast_translationP, token_translationP, oracleP,
   (*proof commands*)
   theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, presumeP,