# HG changeset patch
# User wenzelm
# Date 939898074 -7200
# Node ID 3e75fbd4a46bb478d62eef0ad6c8e9a2cf40d3c4
# Parent  8d5d3163fd814c5f69d0a906d61a0c28674a6b9e
renamed verbatim/verb to text_raw/txt_raw;

diff -r 8d5d3163fd81 -r 3e75fbd4a46b src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Oct 14 12:46:30 1999 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Oct 14 12:47:54 1999 +0200
@@ -58,8 +58,8 @@
 val textP = OuterSyntax.markup_command "text" "formal comment (theory)" K.thy_decl
   (P.comment >> (Toplevel.theory o IsarThy.add_text));
 
-val verbatimP = OuterSyntax.verbatim_command "verbatim" "verbatim document preparation text"
-  K.thy_decl (P.comment >> (Toplevel.theory o IsarThy.add_verbatim));
+val text_rawP = OuterSyntax.verbatim_command "text_raw" "raw document preparation text"
+  K.thy_decl (P.comment >> (Toplevel.theory o IsarThy.add_text_raw));
 
 
 val sectP = OuterSyntax.markup_command "sect" "formal comment (proof)" K.prf_decl
@@ -74,8 +74,8 @@
 val txtP = OuterSyntax.markup_command "txt" "formal comment (proof)" K.prf_decl
   (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_txt)));
 
-val verbP = OuterSyntax.verbatim_command "verb" "verbatim document preparation text (proof)"
-  K.prf_decl (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_verb)));
+val txt_rawP = OuterSyntax.verbatim_command "txt_raw" "raw document preparation text (proof)"
+  K.prf_decl (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_txt_raw)));
 
 
 
@@ -607,7 +607,7 @@
   theoryP, end_excursionP, kill_excursionP, contextP,
   (*markup commands*)
   headerP, chapterP, sectionP, subsectionP, subsubsectionP, textP,
-  verbatimP, sectP, subsectP, subsubsectP, txtP, verbP,
+  text_rawP, sectP, subsectP, subsubsectP, txtP, txt_rawP,
   (*theory sections*)
   classesP, classrelP, defaultsortP, typedeclP, typeabbrP, nontermP,
   aritiesP, constsP, syntaxP, translationsP, axiomsP, defsP,
diff -r 8d5d3163fd81 -r 3e75fbd4a46b src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Thu Oct 14 12:46:30 1999 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Thu Oct 14 12:47:54 1999 +0200
@@ -13,12 +13,12 @@
   val add_subsection: Comment.text -> theory -> theory
   val add_subsubsection: Comment.text -> theory -> theory
   val add_text: Comment.text -> theory -> theory
-  val add_verbatim: Comment.text -> theory -> theory
+  val add_text_raw: Comment.text -> theory -> theory
   val add_sect: Comment.text -> ProofHistory.T -> ProofHistory.T
   val add_subsect: Comment.text -> ProofHistory.T -> ProofHistory.T
   val add_subsubsect: Comment.text -> ProofHistory.T -> ProofHistory.T
   val add_txt: Comment.text -> ProofHistory.T -> ProofHistory.T
-  val add_verb: Comment.text -> ProofHistory.T -> ProofHistory.T
+  val add_txt_raw: Comment.text -> ProofHistory.T -> ProofHistory.T
   val add_classes: (bclass * xclass list) list * Comment.text -> theory -> theory
   val add_classes_i: (bclass * class list) list * Comment.text  -> theory -> theory
   val add_classrel: (xclass * xclass) * Comment.text -> theory -> theory
@@ -172,7 +172,7 @@
   Toplevel.keep (fn state => if Toplevel.is_toplevel state then () else raise Toplevel.UNDEF);
 
 fun add_text comment thy = thy:theory;
-val add_verbatim = add_text;
+val add_text_raw = add_text;
 val add_chapter = add_text;
 
 fun gen_add_section add present txt thy =
@@ -183,7 +183,7 @@
 val add_subsubsection = gen_add_section add_text Present.subsubsection;
 
 fun add_txt comment = ProofHistory.apply Proof.assert_forward;
-val add_verb = add_txt;
+val add_txt_raw = add_txt;
 val add_sect = add_txt;
 val add_subsect = add_txt;
 val add_subsubsect = add_txt;