exported after_qed for arity proofs
authorhaftmann
Tue Aug 09 15:44:24 2005 +0200 (2005-08-09 ago)
changeset 17041dee6f7047cae
parent 17040 6682c93b7d9f
child 17042 da5cfaa258f7
exported after_qed for arity proofs
src/Pure/axclass.ML
     1.1 --- a/src/Pure/axclass.ML	Tue Aug 09 11:44:38 2005 +0200
     1.2 +++ b/src/Pure/axclass.ML	Tue Aug 09 15:44:24 2005 +0200
     1.3 @@ -19,10 +19,14 @@
     1.4    val add_inst_subclass_i: class * class -> tactic -> theory -> theory
     1.5    val add_inst_arity: xstring * string list * string -> tactic -> theory -> theory
     1.6    val add_inst_arity_i: string * sort list * sort -> tactic -> theory -> theory
     1.7 -  val instance_subclass_proof: xstring * xstring -> bool -> theory -> ProofHistory.T
     1.8 -  val instance_subclass_proof_i: class * class -> bool -> theory -> ProofHistory.T
     1.9 -  val instance_arity_proof: xstring * string list * string -> bool -> theory -> ProofHistory.T
    1.10 -  val instance_arity_proof_i: string * sort list * sort -> bool -> theory -> ProofHistory.T
    1.11 +  val instance_subclass_proof: xstring * xstring -> (theory -> theory)
    1.12 +    -> bool -> theory -> ProofHistory.T
    1.13 +  val instance_subclass_proof_i: class * class -> (theory -> theory)
    1.14 +    -> bool -> theory -> ProofHistory.T
    1.15 +  val instance_arity_proof: xstring * string list * string -> (theory -> theory)
    1.16 +    -> bool -> theory -> ProofHistory.T
    1.17 +  val instance_arity_proof_i: string * sort list * sort -> (theory -> theory)
    1.18 +    -> bool -> theory -> ProofHistory.T
    1.19    val intro_classes_tac: thm list -> tactic
    1.20    val default_intro_classes_tac: thm list -> tactic
    1.21  
    1.22 @@ -317,9 +321,9 @@
    1.23  
    1.24  local
    1.25  
    1.26 -fun inst_proof mk_prop add_thms inst int theory =
    1.27 +fun inst_proof mk_prop add_thms inst after_qed int theory =
    1.28    theory
    1.29 -  |> IsarThy.multi_theorem_i Drule.internalK (K I) ProofContext.export_standard
    1.30 +  |> IsarThy.multi_theorem_i Drule.internalK (K after_qed) ProofContext.export_standard
    1.31      ("", [fn (thy, th) => (add_thms [th] thy, th)]) []
    1.32      (map (fn t => (("", []), [(t, ([], []))])) (mk_prop theory inst)) int;
    1.33  
    1.34 @@ -368,8 +372,8 @@
    1.35  
    1.36  val instanceP =
    1.37    OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
    1.38 -    ((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.xname) >> instance_subclass_proof ||
    1.39 -      (P.xname -- (P.$$$ "::" |-- P.arity) >> P.triple2) >> instance_arity_proof)
    1.40 +    ((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.xname) >> (fn i => instance_subclass_proof i I) ||
    1.41 +      (P.xname -- (P.$$$ "::" |-- P.arity) >> P.triple2) >> (fn i => instance_arity_proof i I))
    1.42        >> (Toplevel.print oo Toplevel.theory_to_proof));
    1.43  
    1.44  val _ = OuterSyntax.add_parsers [axclassP, instanceP];