src/Pure/Isar/isar_thy.ML
changeset 7862 3e75fbd4a46b
parent 7851 4a6df182b093
child 7909 824ea50b8dbb
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Thu Oct 14 12:46:30 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Thu Oct 14 12:47:54 1999 +0200
     1.3 @@ -13,12 +13,12 @@
     1.4    val add_subsection: Comment.text -> theory -> theory
     1.5    val add_subsubsection: Comment.text -> theory -> theory
     1.6    val add_text: Comment.text -> theory -> theory
     1.7 -  val add_verbatim: Comment.text -> theory -> theory
     1.8 +  val add_text_raw: Comment.text -> theory -> theory
     1.9    val add_sect: Comment.text -> ProofHistory.T -> ProofHistory.T
    1.10    val add_subsect: Comment.text -> ProofHistory.T -> ProofHistory.T
    1.11    val add_subsubsect: Comment.text -> ProofHistory.T -> ProofHistory.T
    1.12    val add_txt: Comment.text -> ProofHistory.T -> ProofHistory.T
    1.13 -  val add_verb: Comment.text -> ProofHistory.T -> ProofHistory.T
    1.14 +  val add_txt_raw: Comment.text -> ProofHistory.T -> ProofHistory.T
    1.15    val add_classes: (bclass * xclass list) list * Comment.text -> theory -> theory
    1.16    val add_classes_i: (bclass * class list) list * Comment.text  -> theory -> theory
    1.17    val add_classrel: (xclass * xclass) * Comment.text -> theory -> theory
    1.18 @@ -172,7 +172,7 @@
    1.19    Toplevel.keep (fn state => if Toplevel.is_toplevel state then () else raise Toplevel.UNDEF);
    1.20  
    1.21  fun add_text comment thy = thy:theory;
    1.22 -val add_verbatim = add_text;
    1.23 +val add_text_raw = add_text;
    1.24  val add_chapter = add_text;
    1.25  
    1.26  fun gen_add_section add present txt thy =
    1.27 @@ -183,7 +183,7 @@
    1.28  val add_subsubsection = gen_add_section add_text Present.subsubsection;
    1.29  
    1.30  fun add_txt comment = ProofHistory.apply Proof.assert_forward;
    1.31 -val add_verb = add_txt;
    1.32 +val add_txt_raw = add_txt;
    1.33  val add_sect = add_txt;
    1.34  val add_subsect = add_txt;
    1.35  val add_subsubsect = add_txt;