src/HOL/hologic.ML
changeset 9473 7d13a5ace928
parent 9362 b78d4246a320
child 9856 c34d3c94298c
equal deleted inserted replaced
9472:b63b21f370ca 9473:7d13a5ace928
    15   val false_const: term
    15   val false_const: term
    16   val true_const: term
    16   val true_const: term
    17   val mk_setT: typ -> typ
    17   val mk_setT: typ -> typ
    18   val dest_setT: typ -> typ
    18   val dest_setT: typ -> typ
    19   val mk_Trueprop: term -> term
    19   val mk_Trueprop: term -> term
       
    20   val atomic_Trueprop: string -> term
    20   val dest_Trueprop: term -> term
    21   val dest_Trueprop: term -> term
    21   val conj: term
    22   val conj: term
    22   val disj: term
    23   val disj: term
    23   val imp: term
    24   val imp: term
    24   val Not: term
    25   val Not: term
   101 
   102 
   102 val Trueprop = Const ("Trueprop", boolT --> propT);
   103 val Trueprop = Const ("Trueprop", boolT --> propT);
   103 
   104 
   104 fun mk_Trueprop P = Trueprop $ P;
   105 fun mk_Trueprop P = Trueprop $ P;
   105 
   106 
       
   107 fun atomic_Trueprop x = mk_Trueprop (Free (x, boolT));
       
   108 
   106 fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
   109 fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
   107   | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
   110   | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
   108 
   111 
   109 
   112 
   110 val conj = Const ("op &", [boolT, boolT] ---> boolT)
   113 val conj = Const ("op &", [boolT, boolT] ---> boolT)