equal
deleted
inserted
replaced
15 val true_const: term |
15 val true_const: term |
16 val mk_setT: typ -> typ |
16 val mk_setT: typ -> typ |
17 val dest_setT: typ -> typ |
17 val dest_setT: typ -> typ |
18 val Trueprop: term |
18 val Trueprop: term |
19 val mk_Trueprop: term -> term |
19 val mk_Trueprop: term -> term |
|
20 val is_Trueprop: term -> bool |
20 val dest_Trueprop: term -> term |
21 val dest_Trueprop: term -> term |
21 val conj: term |
22 val conj: term |
22 val disj: term |
23 val disj: term |
23 val imp: term |
24 val imp: term |
24 val Not: term |
25 val Not: term |
117 |
118 |
118 val Trueprop = Const ("Trueprop", boolT --> propT); |
119 val Trueprop = Const ("Trueprop", boolT --> propT); |
119 |
120 |
120 fun mk_Trueprop P = Trueprop $ P; |
121 fun mk_Trueprop P = Trueprop $ P; |
121 |
122 |
|
123 fun is_Trueprop (Const ("Trueprop", _) $ _) = true |
|
124 | is_Trueprop t = false; |
|
125 |
122 fun dest_Trueprop (Const ("Trueprop", _) $ P) = P |
126 fun dest_Trueprop (Const ("Trueprop", _) $ P) = P |
123 | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]); |
127 | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]); |
124 |
128 |
125 |
129 |
126 val conj = Const ("op &", [boolT, boolT] ---> boolT) |
130 val conj = Const ("op &", [boolT, boolT] ---> boolT) |