equal
deleted
inserted
replaced
6 and proof generation for multiple quantified formulae. |
6 and proof generation for multiple quantified formulae. |
7 *) |
7 *) |
8 |
8 |
9 signature QELIM = |
9 signature QELIM = |
10 sig |
10 sig |
11 val tproof_of_mlift_qelim: Sign.sg -> (term -> bool) -> |
11 val tproof_of_mlift_qelim: theory -> (term -> bool) -> |
12 (string list -> term -> thm) -> (term -> thm) -> |
12 (string list -> term -> thm) -> (term -> thm) -> |
13 (term -> thm) -> term -> thm |
13 (term -> thm) -> term -> thm |
14 |
14 |
15 end; |
15 end; |
16 |
16 |
17 structure Qelim : QELIM = |
17 structure Qelim : QELIM = |
18 struct |
18 struct |
19 open CooperDec; |
19 open CooperDec; |
20 open CooperProof; |
20 open CooperProof; |
21 |
21 |
22 val cboolT = ctyp_of (sign_of HOL.thy) HOLogic.boolT; |
22 val cboolT = ctyp_of HOL.thy HOLogic.boolT; |
23 |
23 |
24 (* List of the theorems to be used in the following*) |
24 (* List of the theorems to be used in the following*) |
25 |
25 |
26 val qe_ex_conj = thm "qe_ex_conj"; |
26 val qe_ex_conj = thm "qe_ex_conj"; |
27 val qe_ex_nconj = thm "qe_ex_nconj"; |
27 val qe_ex_nconj = thm "qe_ex_nconj"; |