equal
deleted
inserted
replaced
10 data-slot. |
10 data-slot. |
11 *) |
11 *) |
12 |
12 |
13 signature NOMINAL_THMDECLS = |
13 signature NOMINAL_THMDECLS = |
14 sig |
14 sig |
|
15 val nominal_eqvt_debug: bool Config.T |
15 val eqvt_add: attribute |
16 val eqvt_add: attribute |
16 val eqvt_del: attribute |
17 val eqvt_del: attribute |
17 val eqvt_force_add: attribute |
18 val eqvt_force_add: attribute |
18 val eqvt_force_del: attribute |
19 val eqvt_force_del: attribute |
19 val setup: theory -> theory |
20 val setup: theory -> theory |
67 full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps perm_pi_simp))] |
68 full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps perm_pi_simp))] |
68 end; |
69 end; |
69 |
70 |
70 fun get_derived_thm ctxt hyp concl orig_thm pi typi = |
71 fun get_derived_thm ctxt hyp concl orig_thm pi typi = |
71 let |
72 let |
72 val thy = Proof_Context.theory_of ctxt; |
|
73 val pi' = Var (pi, typi); |
73 val pi' = Var (pi, typi); |
74 val lhs = Const (@{const_name "perm"}, typi --> HOLogic.boolT --> HOLogic.boolT) $ pi' $ hyp; |
74 val lhs = Const (@{const_name "perm"}, typi --> HOLogic.boolT --> HOLogic.boolT) $ pi' $ hyp; |
75 val ([goal_term, pi''], ctxt') = Variable.import_terms false |
75 val ([goal_term, pi''], ctxt') = Variable.import_terms false |
76 [HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, concl)), pi'] ctxt |
76 [HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, concl)), pi'] ctxt |
77 val _ = writeln (Syntax.string_of_term ctxt' goal_term); |
77 val _ = writeln (Syntax.string_of_term ctxt' goal_term); |