blob: 529a1050977ba95d85a8eec27480c5450d895c82 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
open Util
open Pp
open Term
open Tacmach
open Fol
type prover = Simplify | CVCLite | Harvey
let dp prover gl =
let concl = pf_concl gl in
if not (is_Prop (pf_type_of gl concl)) then error "not a proposition";
error "not yet implemented"
let simplify = dp Simplify
let cvc_lite = dp CVCLite
let harvey = dp Harvey
|
