11 val mk_Trueprop : term -> term |
11 val mk_Trueprop : term -> term |
12 val dest_Trueprop : term -> term |
12 val dest_Trueprop : term -> term |
13 val conj : term |
13 val conj : term |
14 val disj : term |
14 val disj : term |
15 val imp : term |
15 val imp : term |
|
16 val mk_conj : term * term -> term |
|
17 val mk_disj : term * term -> term |
|
18 val mk_imp : term * term -> term |
16 val dest_imp : term -> term*term |
19 val dest_imp : term -> term*term |
17 val all_const : typ -> term |
20 val all_const : typ -> term |
18 val mk_all : term * term -> term |
21 val mk_all : term * term -> term |
19 val exists_const : typ -> term |
22 val exists_const : typ -> term |
20 val mk_exists : term * term -> term |
23 val mk_exists : term * term -> term |
40 |
43 |
41 val conj = Const("op &", [oT,oT]--->oT) |
44 val conj = Const("op &", [oT,oT]--->oT) |
42 and disj = Const("op |", [oT,oT]--->oT) |
45 and disj = Const("op |", [oT,oT]--->oT) |
43 and imp = Const("op -->", [oT,oT]--->oT); |
46 and imp = Const("op -->", [oT,oT]--->oT); |
44 |
47 |
|
48 fun mk_conj (t1, t2) = conj $ t1 $ t2 |
|
49 and mk_disj (t1, t2) = disj $ t1 $ t2 |
|
50 and mk_imp (t1, t2) = imp $ t1 $ t2; |
|
51 |
45 fun dest_imp (Const("op -->",_) $ A $ B) = (A, B) |
52 fun dest_imp (Const("op -->",_) $ A $ B) = (A, B) |
46 | dest_imp t = raise TERM ("dest_imp", [t]); |
53 | dest_imp t = raise TERM ("dest_imp", [t]); |
47 |
54 |
48 fun eq_const T = Const ("op =", [T, T] ---> oT); |
55 fun eq_const T = Const ("op =", [T, T] ---> oT); |
49 fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u; |
56 fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u; |