equal
deleted
inserted
replaced
1 (* Title: HOL/Tools/Qelim/cooper.ML |
1 (* Title: HOL/Tools/Qelim/cooper.ML |
2 Author: Amine Chaieb, TU Muenchen |
2 Author: Amine Chaieb, TU Muenchen |
3 *) |
3 *) |
4 |
4 |
5 signature COOPER = |
5 signature COOPER = |
6 sig |
6 sig |
7 val cooper_conv : Proof.context -> conv |
7 val cooper_conv : Proof.context -> conv |
8 exception COOPER of string * exn |
8 exception COOPER of string * exn |
9 end; |
9 end; |
10 |
10 |
11 structure Cooper: COOPER = |
11 structure Cooper: COOPER = |
12 struct |
12 struct |
13 |
13 |
14 open Conv; |
14 open Conv; |
15 open Normalizer; |
|
16 |
15 |
17 exception COOPER of string * exn; |
16 exception COOPER of string * exn; |
18 fun simp_thms_conv ctxt = |
17 fun simp_thms_conv ctxt = |
19 Simplifier.rewrite (Simplifier.context ctxt HOL_basic_ss addsimps @{thms simp_thms}); |
18 Simplifier.rewrite (Simplifier.context ctxt HOL_basic_ss addsimps @{thms simp_thms}); |
20 val FWD = Drule.implies_elim_list; |
19 val FWD = Drule.implies_elim_list; |