src/Pure/Isar/isar_thy.ML
changeset 6888 d0c68ebdabc5
parent 6885 1dcac1789759
child 6890 05732285677e
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Fri Jul 02 15:05:16 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Fri Jul 02 19:04:32 1999 +0200
     1.3 @@ -121,6 +121,7 @@
     1.4    val terminal_proof: Method.text * Comment.interest -> Toplevel.transition -> Toplevel.transition
     1.5    val immediate_proof: Toplevel.transition -> Toplevel.transition
     1.6    val default_proof: Toplevel.transition -> Toplevel.transition
     1.7 +  val skip_proof: Toplevel.transition -> Toplevel.transition
     1.8    val also: ((string * Args.src list) list * Comment.interest) option * Comment.text
     1.9      -> Toplevel.transition -> Toplevel.transition
    1.10    val also_i: (thm list * Comment.interest) option * Comment.text
    1.11 @@ -331,6 +332,7 @@
    1.12  
    1.13  val local_immediate_proof = proof'' (ProofHistory.applys_close o Method.local_immediate_proof);
    1.14  val local_default_proof = proof'' (ProofHistory.applys_close o Method.local_default_proof);
    1.15 +val local_skip_proof = proof'' (ProofHistory.applys_close o SkipProof.local_skip_proof);
    1.16  
    1.17  
    1.18  (* global endings *)
    1.19 @@ -357,6 +359,7 @@
    1.20  val global_terminal_proof = global_result o Method.global_terminal_proof o Comment.ignore_interest;
    1.21  val global_immediate_proof = global_result Method.global_immediate_proof;
    1.22  val global_default_proof = global_result Method.global_default_proof;
    1.23 +val global_skip_proof = global_result SkipProof.global_skip_proof;
    1.24  
    1.25  
    1.26  (* common endings *)
    1.27 @@ -365,6 +368,7 @@
    1.28  fun terminal_proof meth = local_terminal_proof meth o global_terminal_proof meth;
    1.29  val immediate_proof = local_immediate_proof o global_immediate_proof;
    1.30  val default_proof = local_default_proof o global_default_proof;
    1.31 +val skip_proof = local_skip_proof o global_skip_proof;
    1.32  
    1.33  
    1.34  (* calculational proof commands *)