src/HOLCF/Tools/Domain/domain_library.ML
changeset 37145 01aa36932739
parent 36692 54b64d4ad524
child 37391 476270a6c2dc
equal deleted inserted replaced
37144:fd6308b4df72 37145:01aa36932739
   183 fun mk_disj (S,T) = disj $ S $ T;
   183 fun mk_disj (S,T) = disj $ S $ T;
   184 fun mk_imp  (S,T) = imp  $ S $ T;
   184 fun mk_imp  (S,T) = imp  $ S $ T;
   185 fun mk_lam  (x,T) = Abs(x,dummyT,T);
   185 fun mk_lam  (x,T) = Abs(x,dummyT,T);
   186 fun mk_all  (x,P) = HOLogic.mk_all (x,dummyT,P);
   186 fun mk_all  (x,P) = HOLogic.mk_all (x,dummyT,P);
   187 fun mk_ex   (x,P) = mk_exists (x,dummyT,P);
   187 fun mk_ex   (x,P) = mk_exists (x,dummyT,P);
   188 fun mk_constrainall (x,typ,P) = %%:"All" $ (TypeInfer.constrain (typ --> boolT) (mk_lam(x,P)));
   188 fun mk_constrainall (x,typ,P) = %%:"All" $ (Type_Infer.constrain (typ --> boolT) (mk_lam(x,P)));
   189 end
   189 end
   190 
   190 
   191 fun mk_All  (x,P) = %%:"all" $ mk_lam(x,P); (* meta universal quantification *)
   191 fun mk_All  (x,P) = %%:"all" $ mk_lam(x,P); (* meta universal quantification *)
   192 
   192 
   193 infixr 0 ===>;  fun S ===> T = %%:"==>" $ S $ T;
   193 infixr 0 ===>;  fun S ===> T = %%:"==>" $ S $ T;