src/FOL/fologic.ML
changeset 9850 bee6eb4b6a42
parent 9543 ce61d1c1a509
child 10384 a499b9ce2ffe
equal deleted inserted replaced
9849:71ad08ad2cf0 9850:bee6eb4b6a42
     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
    12   val atomic_Trueprop	: string -> term
    13   val dest_Trueprop	: term -> term
    13   val dest_Trueprop	: term -> term
       
    14   val not		: term
    14   val conj		: term
    15   val conj		: term
    15   val disj		: term
    16   val disj		: term
    16   val imp		: term
    17   val imp		: term
    17   val iff		: term
    18   val iff		: term
    18   val mk_conj		: term * term -> term
    19   val mk_conj		: term * term -> term
    48 fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
    49 fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
    49   | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
    50   | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
    50 
    51 
    51 (** Logical constants **)
    52 (** Logical constants **)
    52 
    53 
    53 val conj = Const("op &", [oT,oT]--->oT)
    54 val not = Const ("Not", oT --> oT);
    54 and disj = Const("op |", [oT,oT]--->oT)
    55 val conj = Const("op &", [oT,oT]--->oT);
    55 and imp = Const("op -->", [oT,oT]--->oT)
    56 val disj = Const("op |", [oT,oT]--->oT);
    56 and iff = Const("op <->", [oT,oT]--->oT);
    57 val imp = Const("op -->", [oT,oT]--->oT)
       
    58 val iff = Const("op <->", [oT,oT]--->oT);
    57 
    59 
    58 fun mk_conj (t1, t2) = conj $ t1 $ t2
    60 fun mk_conj (t1, t2) = conj $ t1 $ t2
    59 and mk_disj (t1, t2) = disj $ t1 $ t2
    61 and mk_disj (t1, t2) = disj $ t1 $ t2
    60 and mk_imp (t1, t2) = imp $ t1 $ t2
    62 and mk_imp (t1, t2) = imp $ t1 $ t2
    61 and mk_iff (t1, t2) = iff $ t1 $ t2;
    63 and mk_iff (t1, t2) = iff $ t1 $ t2;