src/Pure/Isar/isar_thy.ML
changeset 6108 2c9ed58c30ba
parent 6091 e3cdbd929a24
child 6198 7fa2deb92b39
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Tue Jan 12 17:19:13 1999 +0100
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Tue Jan 12 17:19:53 1999 +0100
     1.3 @@ -45,7 +45,7 @@
     1.4    val then_tac: Method.text -> ProofHistory.T -> ProofHistory.T
     1.5    val proof: Method.text option -> ProofHistory.T -> ProofHistory.T
     1.6    val terminal_proof: Method.text -> ProofHistory.T -> ProofHistory.T
     1.7 -  val trivial_proof: ProofHistory.T -> ProofHistory.T
     1.8 +  val immediate_proof: ProofHistory.T -> ProofHistory.T
     1.9    val default_proof: ProofHistory.T -> ProofHistory.T
    1.10    val use_mltext: string -> theory option -> theory option
    1.11    val use_mltext_theory: string -> theory -> theory
    1.12 @@ -167,7 +167,7 @@
    1.13  val proof = ProofHistory.applys o Method.proof;
    1.14  val end_block = ProofHistory.applys_close Method.end_block;
    1.15  val terminal_proof = ProofHistory.applys_close o Method.terminal_proof;
    1.16 -val trivial_proof = ProofHistory.applys_close Method.trivial_proof;
    1.17 +val immediate_proof = ProofHistory.applys_close Method.immediate_proof;
    1.18  val default_proof = ProofHistory.applys_close Method.default_proof;
    1.19  
    1.20