changeset 10384 | a499b9ce2ffe |
parent 9850 | bee6eb4b6a42 |
child 11668 | 548ba68385a3 |
--- a/src/FOL/fologic.ML Fri Nov 03 21:31:11 2000 +0100 +++ b/src/FOL/fologic.ML Fri Nov 03 21:31:53 2000 +0100 @@ -9,7 +9,6 @@ sig val oT : typ val mk_Trueprop : term -> term - val atomic_Trueprop : string -> term val dest_Trueprop : term -> term val not : term val conj : term @@ -44,8 +43,6 @@ fun mk_Trueprop P = Trueprop $ P; -fun atomic_Trueprop x = mk_Trueprop (Free (x, oT)); - fun dest_Trueprop (Const ("Trueprop", _) $ P) = P | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);