src/HOL/Tools/hologic.ML
changeset 45977 e3accf78bb07
parent 45740 132a3e1c0fe5
child 46216 7fcdb5562461
equal deleted inserted replaced
45976:9dc0d950baa9 45977:e3accf78bb07
   160 val boolN = "HOL.bool";
   160 val boolN = "HOL.bool";
   161 val boolT = Type (boolN, []);
   161 val boolT = Type (boolN, []);
   162 
   162 
   163 fun mk_induct_forall T = Const ("HOL.induct_forall", (T --> boolT) --> boolT);
   163 fun mk_induct_forall T = Const ("HOL.induct_forall", (T --> boolT) --> boolT);
   164 
   164 
   165 fun mk_setT T = T --> boolT;
   165 fun mk_setT T = Type ("Set.set", [T]);
   166 
   166 
   167 fun dest_setT (Type ("fun", [T, Type ("HOL.bool", [])])) = T
   167 fun dest_setT (Type ("Set.set", [T])) = T
   168   | dest_setT T = raise TYPE ("dest_setT: set type expected", [T], []);
   168   | dest_setT T = raise TYPE ("dest_setT: set type expected", [T], []);
   169 
   169 
   170 fun mk_set T ts =
   170 fun mk_set T ts =
   171   let
   171   let
   172     val sT = mk_setT T;
   172     val sT = mk_setT T;