equal
deleted
inserted
replaced
7 |
7 |
8 signature FOLOGIC = |
8 signature FOLOGIC = |
9 sig |
9 sig |
10 val oT : typ |
10 val oT : typ |
11 val mk_Trueprop : term -> term |
11 val mk_Trueprop : term -> term |
|
12 val atomic_Trueprop : string -> term |
12 val dest_Trueprop : term -> term |
13 val dest_Trueprop : term -> term |
13 val conj : term |
14 val conj : term |
14 val disj : term |
15 val disj : term |
15 val imp : term |
16 val imp : term |
16 val mk_conj : term * term -> term |
17 val mk_conj : term * term -> term |
33 val oT = Type("o",[]); |
34 val oT = Type("o",[]); |
34 |
35 |
35 val Trueprop = Const("Trueprop", oT-->propT); |
36 val Trueprop = Const("Trueprop", oT-->propT); |
36 |
37 |
37 fun mk_Trueprop P = Trueprop $ P; |
38 fun mk_Trueprop P = Trueprop $ P; |
|
39 |
|
40 fun atomic_Trueprop x = mk_Trueprop (Free (x, oT)); |
38 |
41 |
39 fun dest_Trueprop (Const ("Trueprop", _) $ P) = P |
42 fun dest_Trueprop (Const ("Trueprop", _) $ P) = P |
40 | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]); |
43 | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]); |
41 |
44 |
42 (** Logical constants **) |
45 (** Logical constants **) |