# HG changeset patch # User haftmann # Date 1138021571 -3600 # Node ID 4e41252eae57aa753e375adb3d4e3350e497a479 # Parent aa82bd41555d31285beaac680acb024fd4d6a924 exported after_qed for axclass instance diff -r aa82bd41555d -r 4e41252eae57 src/Pure/axclass.ML --- a/src/Pure/axclass.ML Mon Jan 23 11:41:54 2006 +0100 +++ b/src/Pure/axclass.ML Mon Jan 23 14:06:11 2006 +0100 @@ -22,8 +22,8 @@ val add_inst_arity_i: string * sort list * sort -> tactic -> theory -> theory val instance_subclass: xstring * xstring -> theory -> Proof.state val instance_subclass_i: class * class -> theory -> Proof.state - val instance_arity: xstring * string list * string -> theory -> Proof.state - val instance_arity_i: string * sort list * sort -> theory -> Proof.state + val instance_arity: (theory -> theory) -> xstring * string list * string -> theory -> Proof.state + val instance_arity_i: (theory -> theory) -> string * sort list * sort -> theory -> Proof.state val read_arity: theory -> xstring * string list * string -> arity val cert_arity: theory -> string * sort list * sort -> arity val intro_classes_tac: thm list -> tactic @@ -303,19 +303,22 @@ local -fun gen_instance mk_prop add_thms inst thy = thy +fun gen_instance mk_prop add_thms after_qed inst thy = + thy |> ProofContext.init - |> Proof.theorem_i Drule.internalK NONE (fold add_thms) NONE ("", []) - (map (fn t => (("", []), [(t, ([], []))])) (mk_prop thy inst)); + |> Proof.theorem_i Drule.internalK NONE (after_qed oo fold add_thms) NONE ("", []) + (map (fn t => (("", []), [(t, ([], []))])) (mk_prop thy inst)); in val instance_subclass = - gen_instance (single oo (mk_classrel oo read_classrel)) add_classrel_thms; + gen_instance (single oo (mk_classrel oo read_classrel)) add_classrel_thms I; val instance_subclass_i = - gen_instance (single oo (mk_classrel oo cert_classrel)) add_classrel_thms; -val instance_arity = gen_instance (mk_arities oo read_arity) add_arity_thms; -val instance_arity_i = gen_instance (mk_arities oo cert_arity) add_arity_thms; + gen_instance (single oo (mk_classrel oo cert_classrel)) add_classrel_thms I; +val instance_arity = + gen_instance (mk_arities oo read_arity) add_arity_thms; +val instance_arity_i = + gen_instance (mk_arities oo cert_arity) add_arity_thms; end; @@ -354,7 +357,7 @@ val instanceP = OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal ((P.xname -- ((P.$$$ "\\" || P.$$$ "<") |-- P.!!! P.xname) >> instance_subclass || - P.xname -- (P.$$$ "::" |-- P.!!! P.arity) >> (instance_arity o P.triple2)) + P.xname -- (P.$$$ "::" |-- P.!!! P.arity) >> (instance_arity I o P.triple2)) >> (Toplevel.print oo Toplevel.theory_to_proof)); val _ = OuterSyntax.add_parsers [axclassP, instanceP];