summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/FOL/fologic.ML

changeset 32449 | 696d64ed85da |

parent 31974 | e81979a703a4 |

child 38500 | d5477ee35820 |

--- a/src/FOL/fologic.ML Sat Aug 29 10:50:04 2009 +0200 +++ b/src/FOL/fologic.ML Sat Aug 29 12:01:25 2009 +0200 @@ -6,28 +6,28 @@ signature FOLOGIC = sig - val oT : typ - val mk_Trueprop : term -> term - val dest_Trueprop : term -> term - val not : term - val conj : term - val disj : term - val imp : term - val iff : term - val mk_conj : term * term -> term - val mk_disj : term * term -> term - val mk_imp : term * term -> term - val dest_imp : term -> term*term - val dest_conj : term -> term list - val mk_iff : term * term -> term - val dest_iff : term -> term*term - val all_const : typ -> term - val mk_all : term * term -> term - val exists_const : typ -> term - val mk_exists : term * term -> term - val eq_const : typ -> term - val mk_eq : term * term -> term - val dest_eq : term -> term*term + val oT: typ + val mk_Trueprop: term -> term + val dest_Trueprop: term -> term + val not: term + val conj: term + val disj: term + val imp: term + val iff: term + val mk_conj: term * term -> term + val mk_disj: term * term -> term + val mk_imp: term * term -> term + val dest_imp: term -> term * term + val dest_conj: term -> term list + val mk_iff: term * term -> term + val dest_iff: term -> term * term + val all_const: typ -> term + val mk_all: term * term -> term + val exists_const: typ -> term + val mk_exists: term * term -> term + val eq_const: typ -> term + val mk_eq: term * term -> term + val dest_eq: term -> term * term val mk_binop: string -> term * term -> term val mk_binrel: string -> term * term -> term val dest_bin: string -> typ -> term -> term * term @@ -46,7 +46,8 @@ fun dest_Trueprop (Const ("Trueprop", _) $ P) = P | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]); -(** Logical constants **) + +(* Logical constants *) val not = Const ("Not", oT --> oT); val conj = Const("op &", [oT,oT]--->oT); @@ -80,6 +81,7 @@ fun exists_const T = Const ("Ex", [T --> oT] ---> oT); fun mk_exists (Free(x,T),P) = exists_const T $ (absfree (x,T,P)); + (* binary oprations and relations *) fun mk_binop c (t, u) = @@ -97,5 +99,4 @@ else raise TERM ("dest_bin " ^ c, [tm]) | dest_bin c _ tm = raise TERM ("dest_bin " ^ c, [tm]); - end;