199 val axiom3 = Logic.mk_implies |
199 val axiom3 = Logic.mk_implies |
200 (HOLogic.mk_Trueprop (cprm_eq $ pi1 $ pi2), |
200 (HOLogic.mk_Trueprop (cprm_eq $ pi1 $ pi2), |
201 HOLogic.mk_Trueprop (HOLogic.mk_eq (cperm $ pi1 $ x, cperm $ pi2 $ x))); |
201 HOLogic.mk_Trueprop (HOLogic.mk_eq (cperm $ pi1 $ x, cperm $ pi2 $ x))); |
202 in |
202 in |
203 AxClass.add_axclass_i (cl_name, ["HOL.type"]) |
203 AxClass.add_axclass_i (cl_name, ["HOL.type"]) |
204 [((cl_name^"1", axiom1),[Attrib.theory Simplifier.simp_add]), |
204 [((cl_name^"1", axiom1),[Simplifier.simp_add]), |
205 ((cl_name^"2", axiom2),[]), |
205 ((cl_name^"2", axiom2),[]), |
206 ((cl_name^"3", axiom3),[])] thy |
206 ((cl_name^"3", axiom3),[])] thy |
207 end) ak_names_types thy6; |
207 end) ak_names_types thy6; |
208 |
208 |
209 (* proves that every pt_<ak>-type together with <ak>-type *) |
209 (* proves that every pt_<ak>-type together with <ak>-type *) |