src/HOL/Tools/hologic.ML
changeset 40845 15b97bd4b5c0
parent 40627 becf5d5187cc
child 41339 481c89fabcbc
     1.1 --- a/src/HOL/Tools/hologic.ML	Wed Dec 01 15:03:44 2010 +0100
     1.2 +++ b/src/HOL/Tools/hologic.ML	Wed Dec 01 15:35:40 2010 +0100
     1.3 @@ -8,6 +8,7 @@
     1.4  sig
     1.5    val typeS: sort
     1.6    val typeT: typ
     1.7 +  val mk_comp: term * term -> term
     1.8    val boolN: string
     1.9    val boolT: typ
    1.10    val Trueprop: term
    1.11 @@ -142,6 +143,16 @@
    1.12  val typeT = Type_Infer.anyT typeS;
    1.13  
    1.14  
    1.15 +(* functions *)
    1.16 +
    1.17 +fun mk_comp (f, g) =
    1.18 +  let
    1.19 +    val fT = fastype_of f;
    1.20 +    val gT = fastype_of g;
    1.21 +    val compT = fT --> gT --> domain_type gT --> range_type fT;
    1.22 +  in Const ("Fun.comp", compT) $ f $ g end;
    1.23 +
    1.24 +
    1.25  (* bool and set *)
    1.26  
    1.27  val boolN = "HOL.bool";