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 |
|
13 val dest_Trueprop : term -> term |
12 val dest_Trueprop : term -> term |
14 val not : term |
13 val not : term |
15 val conj : term |
14 val conj : term |
16 val disj : term |
15 val disj : term |
17 val imp : term |
16 val imp : term |
41 val oT = Type("o",[]); |
40 val oT = Type("o",[]); |
42 |
41 |
43 val Trueprop = Const("Trueprop", oT-->propT); |
42 val Trueprop = Const("Trueprop", oT-->propT); |
44 |
43 |
45 fun mk_Trueprop P = Trueprop $ P; |
44 fun mk_Trueprop P = Trueprop $ P; |
46 |
|
47 fun atomic_Trueprop x = mk_Trueprop (Free (x, oT)); |
|
48 |
45 |
49 fun dest_Trueprop (Const ("Trueprop", _) $ P) = P |
46 fun dest_Trueprop (Const ("Trueprop", _) $ P) = P |
50 | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]); |
47 | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]); |
51 |
48 |
52 (** Logical constants **) |
49 (** Logical constants **) |