changeset 9473 | 7d13a5ace928 |
parent 7692 | 89bbce6f5c17 |
child 9543 | ce61d1c1a509 |
--- a/src/FOL/fologic.ML Sun Jul 30 13:01:50 2000 +0200 +++ b/src/FOL/fologic.ML Sun Jul 30 13:02:14 2000 +0200 @@ -9,6 +9,7 @@ sig val oT : typ val mk_Trueprop : term -> term + val atomic_Trueprop : string -> term val dest_Trueprop : term -> term val conj : term val disj : term @@ -36,6 +37,8 @@ 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]);