equal
deleted
inserted
replaced
17 val iff : term |
17 val iff : term |
18 val mk_conj : term * term -> term |
18 val mk_conj : term * term -> term |
19 val mk_disj : term * term -> term |
19 val mk_disj : term * term -> term |
20 val mk_imp : term * term -> term |
20 val mk_imp : term * term -> term |
21 val dest_imp : term -> term*term |
21 val dest_imp : term -> term*term |
|
22 val dest_conj : term -> term list |
|
23 val dest_concls : term -> term list |
22 val mk_iff : term * term -> term |
24 val mk_iff : term * term -> term |
23 val dest_iff : term -> term*term |
25 val dest_iff : term -> term*term |
24 val all_const : typ -> term |
26 val all_const : typ -> term |
25 val mk_all : term * term -> term |
27 val mk_all : term * term -> term |
26 val exists_const : typ -> term |
28 val exists_const : typ -> term |
60 and mk_iff (t1, t2) = iff $ t1 $ t2; |
62 and mk_iff (t1, t2) = iff $ t1 $ t2; |
61 |
63 |
62 fun dest_imp (Const("op -->",_) $ A $ B) = (A, B) |
64 fun dest_imp (Const("op -->",_) $ A $ B) = (A, B) |
63 | dest_imp t = raise TERM ("dest_imp", [t]); |
65 | dest_imp t = raise TERM ("dest_imp", [t]); |
64 |
66 |
|
67 fun dest_conj (Const ("op &", _) $ t $ t') = t :: dest_conj t' |
|
68 | dest_conj t = [t]; |
|
69 |
|
70 fun imp_concl_of t = imp_concl_of (#2 (dest_imp t)) handle TERM _ => t; |
|
71 val dest_concls = map imp_concl_of o dest_conj o dest_Trueprop; |
|
72 |
65 fun dest_iff (Const("op <->",_) $ A $ B) = (A, B) |
73 fun dest_iff (Const("op <->",_) $ A $ B) = (A, B) |
66 | dest_iff t = raise TERM ("dest_iff", [t]); |
74 | dest_iff t = raise TERM ("dest_iff", [t]); |
67 |
75 |
68 fun eq_const T = Const ("op =", [T, T] ---> oT); |
76 fun eq_const T = Const ("op =", [T, T] ---> oT); |
69 fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u; |
77 fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u; |