--- a/src/HOL/Tools/specification_package.ML Mon May 09 16:38:56 2005 +0200
+++ b/src/HOL/Tools/specification_package.ML Mon May 09 16:40:11 2005 +0200
@@ -29,9 +29,6 @@
val helper = Goals.result()
end
-(* Akin to HOLogic.exists_const *)
-fun choice_const T = Const("Hilbert_Choice.Eps",(T-->HOLogic.boolT)-->T)
-
(* Actual code *)
local
@@ -45,7 +42,8 @@
val cdefname = if thname = ""
then Thm.def_name (Sign.base_name cname)
else thname
- val def_eq = Logic.mk_equals (Const(cname_full,ctype),choice_const ctype $ P)
+ val def_eq = Logic.mk_equals (Const(cname_full,ctype),
+ HOLogic.choice_const ctype $ P)
val (thy',thms) = PureThy.add_defs_i covld [((cdefname,def_eq),[])] thy
val thm' = [thm,hd thms] MRS helper
in
--- a/src/HOL/hologic.ML Mon May 09 16:38:56 2005 +0200
+++ b/src/HOL/hologic.ML Mon May 09 16:40:11 2005 +0200
@@ -27,12 +27,14 @@
val mk_disj: term * term -> term
val mk_imp: term * term -> term
val dest_conj: term -> term list
+ val dest_disj: term -> term list
val dest_imp: term -> term * term
val dest_not: term -> term
val dest_concls: term -> term list
val eq_const: typ -> term
val all_const: typ -> term
val exists_const: typ -> term
+ val choice_const: typ -> term
val Collect_const: typ -> term
val mk_eq: term * term -> term
val dest_eq: term -> term * term
@@ -137,6 +139,9 @@
fun dest_conj (Const ("op &", _) $ t $ t') = t :: dest_conj t'
| dest_conj t = [t];
+fun dest_disj (Const ("op |", _) $ t $ t') = t :: dest_disj t'
+ | dest_disj t = [t];
+
fun dest_imp (Const("op -->",_) $ A $ B) = (A, B)
| dest_imp t = raise TERM ("dest_imp", [t]);
@@ -159,6 +164,8 @@
fun exists_const T = Const ("Ex", [T --> boolT] ---> boolT);
fun mk_exists (x, T, P) = exists_const T $ absfree (x, T, P);
+fun choice_const T = Const("Hilbert_Choice.Eps", (T --> boolT) --> T)
+
fun Collect_const T = Const ("Collect", [T --> boolT] ---> mk_setT T);
fun mk_Collect (a, T, t) = Collect_const T $ absfree (a, T, t);