src/FOL/fologic.ML

 Abstract syntax operations for FOL.
 *)
 
 signature FOLOGIC =
 sig
-  val mk_Trueprop: term -> term
-  val dest_Trueprop: term -> 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 dest_eq: term -> term * term
 end;
 
 structure FOLogic: FOLOGIC =
 struct
-
-fun mk_Trueprop P = \<^Const>\<open>Trueprop for P\<close>;
-
-val dest_Trueprop = \<^Const_fn>\<open>Trueprop for P => P\<close>;
 
 fun mk_conj (t1, t2) = \<^Const>\<open>conj for t1 t2\<close>
 and mk_disj (t1, t2) = \<^Const>\<open>disj for t1 t2\<close>
 and mk_imp (t1, t2) = \<^Const>\<open>imp for t1 t2\<close>
 and mk_iff (t1, t2) = \<^Const>\<open>iff for t1 t2\<close>;