src/HOL/Tools/hologic.ML
changeset 38555 bd6359ed1636
parent 38550 925c4d7b291e
child 38786 e46e7a9cb622
     1.1 --- a/src/HOL/Tools/hologic.ML	Thu Aug 19 16:03:01 2010 +0200
     1.2 +++ b/src/HOL/Tools/hologic.ML	Thu Aug 19 16:03:07 2010 +0200
     1.3 @@ -143,15 +143,15 @@
     1.4  
     1.5  (* bool and set *)
     1.6  
     1.7 -val boolN = "bool";
     1.8 +val boolN = "HOL.bool";
     1.9  val boolT = Type (boolN, []);
    1.10  
    1.11 -val true_const =  Const ("True", boolT);
    1.12 -val false_const = Const ("False", boolT);
    1.13 +val true_const =  Const ("HOL.True", boolT);
    1.14 +val false_const = Const ("HOL.False", boolT);
    1.15  
    1.16  fun mk_setT T = T --> boolT;
    1.17  
    1.18 -fun dest_setT (Type ("fun", [T, Type ("bool", [])])) = T
    1.19 +fun dest_setT (Type ("fun", [T, Type ("HOL.bool", [])])) = T
    1.20    | dest_setT T = raise TYPE ("dest_setT: set type expected", [T], []);
    1.21  
    1.22  fun mk_set T ts =
    1.23 @@ -181,11 +181,11 @@
    1.24  
    1.25  (* logic *)
    1.26  
    1.27 -val Trueprop = Const ("Trueprop", boolT --> propT);
    1.28 +val Trueprop = Const ("HOL.Trueprop", boolT --> propT);
    1.29  
    1.30  fun mk_Trueprop P = Trueprop $ P;
    1.31  
    1.32 -fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
    1.33 +fun dest_Trueprop (Const ("HOL.Trueprop", _) $ P) = P
    1.34    | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
    1.35  
    1.36  fun conj_intr thP thQ =
    1.37 @@ -233,7 +233,7 @@
    1.38  fun dest_imp (Const ("op -->", _) $ A $ B) = (A, B)
    1.39    | dest_imp  t = raise TERM ("dest_imp", [t]);
    1.40  
    1.41 -fun dest_not (Const ("Not", _) $ t) = t
    1.42 +fun dest_not (Const ("HOL.Not", _) $ t) = t
    1.43    | dest_not t = raise TERM ("dest_not", [t]);
    1.44  
    1.45  fun eq_const T = Const ("op =", T --> T --> boolT);
    1.46 @@ -242,11 +242,11 @@
    1.47  fun dest_eq (Const ("op =", _) $ lhs $ rhs) = (lhs, rhs)
    1.48    | dest_eq t = raise TERM ("dest_eq", [t])
    1.49  
    1.50 -fun all_const T = Const ("All", [T --> boolT] ---> boolT);
    1.51 +fun all_const T = Const ("HOL.All", [T --> boolT] ---> boolT);
    1.52  fun mk_all (x, T, P) = all_const T $ absfree (x, T, P);
    1.53  fun list_all (xs, t) = fold_rev (fn (x, T) => fn P => all_const T $ Abs (x, T, P)) xs t;
    1.54  
    1.55 -fun exists_const T = Const ("Ex", [T --> boolT] ---> boolT);
    1.56 +fun exists_const T = Const ("HOL.Ex", [T --> boolT] ---> boolT);
    1.57  fun mk_exists (x, T, P) = exists_const T $ absfree (x, T, P);
    1.58  
    1.59  fun choice_const T = Const("Hilbert_Choice.Eps", (T --> boolT) --> T);