added atomic_Trueprop;
authorwenzelm
Sun Jul 30 13:02:14 2000 +0200 (2000-07-30)
changeset 94737d13a5ace928
parent 9472 b63b21f370ca
child 9474 b0ce3b7c9c26
added atomic_Trueprop;
src/FOL/fologic.ML
src/HOL/hologic.ML
     1.1 --- a/src/FOL/fologic.ML	Sun Jul 30 13:01:50 2000 +0200
     1.2 +++ b/src/FOL/fologic.ML	Sun Jul 30 13:02:14 2000 +0200
     1.3 @@ -9,6 +9,7 @@
     1.4  sig
     1.5    val oT		: typ
     1.6    val mk_Trueprop	: term -> term
     1.7 +  val atomic_Trueprop	: string -> term
     1.8    val dest_Trueprop	: term -> term
     1.9    val conj		: term
    1.10    val disj		: term
    1.11 @@ -36,6 +37,8 @@
    1.12  
    1.13  fun mk_Trueprop P = Trueprop $ P;
    1.14  
    1.15 +fun atomic_Trueprop x = mk_Trueprop (Free (x, oT));
    1.16 +
    1.17  fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
    1.18    | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
    1.19  
     2.1 --- a/src/HOL/hologic.ML	Sun Jul 30 13:01:50 2000 +0200
     2.2 +++ b/src/HOL/hologic.ML	Sun Jul 30 13:02:14 2000 +0200
     2.3 @@ -17,6 +17,7 @@
     2.4    val mk_setT: typ -> typ
     2.5    val dest_setT: typ -> typ
     2.6    val mk_Trueprop: term -> term
     2.7 +  val atomic_Trueprop: string -> term
     2.8    val dest_Trueprop: term -> term
     2.9    val conj: term
    2.10    val disj: term
    2.11 @@ -103,6 +104,8 @@
    2.12  
    2.13  fun mk_Trueprop P = Trueprop $ P;
    2.14  
    2.15 +fun atomic_Trueprop x = mk_Trueprop (Free (x, boolT));
    2.16 +
    2.17  fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
    2.18    | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
    2.19