src/Pure/Isar/isar_thy.ML
changeset 8562 ce0e2b8e8844
parent 8466 f7b06595d0c8
child 8588 b7c3f264f8ac
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Thu Mar 23 21:36:43 2000 +0100
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Thu Mar 23 21:37:13 2000 +0100
     1.3 @@ -143,6 +143,7 @@
     1.4      -> Toplevel.transition -> Toplevel.transition
     1.5    val finally_i: (thm list * Comment.interest) option * Comment.text
     1.6      -> Toplevel.transition -> Toplevel.transition
     1.7 +  val moreover: Comment.text -> Toplevel.transition -> Toplevel.transition
     1.8    val parse_ast_translation: string -> theory -> theory
     1.9    val parse_translation: string -> theory -> theory
    1.10    val print_translation: string -> theory -> theory
    1.11 @@ -454,6 +455,7 @@
    1.12  fun also_i x = proof''' (ProofHistory.applys o gen_calc get_thmss_i Calculation.also x);
    1.13  fun finally x = proof''' (ProofHistory.applys o gen_calc get_thmss Calculation.finally x);
    1.14  fun finally_i x = proof''' (ProofHistory.applys o gen_calc get_thmss_i Calculation.finally x);
    1.15 +fun moreover comment = proof''' (ProofHistory.apply o Calculation.moreover);
    1.16  
    1.17  end;
    1.18