added dest_concls;
authorwenzelm
Thu Oct 04 15:40:05 2001 +0200 (2001-10-04)
changeset 11683f2268239b93f
parent 11682 d9063229b4a1
child 11684 abd396ca7ef9
added dest_concls;
src/HOL/hologic.ML
     1.1 --- a/src/HOL/hologic.ML	Thu Oct 04 15:39:43 2001 +0200
     1.2 +++ b/src/HOL/hologic.ML	Thu Oct 04 15:40:05 2001 +0200
     1.3 @@ -28,6 +28,7 @@
     1.4    val mk_imp: term * term -> term
     1.5    val dest_imp: term -> term * term
     1.6    val dest_conj: term -> term list
     1.7 +  val dest_concls: term -> term list
     1.8    val eq_const: typ -> term
     1.9    val all_const: typ -> term
    1.10    val exists_const: typ -> term
    1.11 @@ -125,6 +126,9 @@
    1.12  fun dest_conj (Const ("op &", _) $ t $ t') = t :: dest_conj t'
    1.13    | dest_conj t = [t];
    1.14  
    1.15 +fun imp_concl_of t = imp_concl_of (#2 (dest_imp t)) handle TERM _ => t;
    1.16 +val dest_concls = map imp_concl_of o dest_conj o dest_Trueprop;
    1.17 +
    1.18  fun eq_const T = Const ("op =", [T, T] ---> boolT);
    1.19  fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
    1.20