renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
authorhaftmann
Tue Sep 26 13:34:16 2006 +0200 (2006-09-26)
changeset 20713823967ef47f1
parent 20712 b3cd1233167f
child 20714 6a122dba034c
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
src/HOL/Algebra/abstract/order.ML
src/HOL/HOL.thy
src/HOL/Hyperreal/NSA.thy
src/HOL/Integ/IntDef.thy
src/HOL/Integ/cooper_dec.ML
src/HOL/Integ/cooper_proof.ML
src/HOL/Integ/int_arith1.ML
src/HOL/Integ/nat_simprocs.ML
src/HOL/Integ/presburger.ML
src/HOL/Integ/reflected_cooper.ML
src/HOL/Lambda/WeakNorm.thy
src/HOL/Library/EfficientNat.thy
src/HOL/Library/ExecutableRat.thy
src/HOL/Library/comm_ring.ML
src/HOL/Nat.thy
src/HOL/OrderedGroup.ML
src/HOL/Prolog/Func.thy
src/HOL/Prolog/Type.ML
src/HOL/Real/ferrante_rackoff_proof.ML
src/HOL/Tools/Presburger/cooper_dec.ML
src/HOL/Tools/Presburger/cooper_proof.ML
src/HOL/Tools/Presburger/presburger.ML
src/HOL/Tools/Presburger/reflected_cooper.ML
src/HOL/arith_data.ML
src/HOL/ex/Abstract_NAT.thy
src/HOL/ex/Codegenerator.thy
src/HOL/ex/mesontest2.ML
src/HOL/hologic.ML
src/HOLCF/Pcpo.thy
src/Provers/Arith/abel_cancel.ML
     1.1 --- a/src/HOL/Algebra/abstract/order.ML	Tue Sep 26 13:34:15 2006 +0200
     1.2 +++ b/src/HOL/Algebra/abstract/order.ML	Tue Sep 26 13:34:16 2006 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  (*** Term order for commutative rings ***)
     1.5  
     1.6  fun ring_ord (Const (a, _)) =
     1.7 -    find_index (fn a' => a = a') ["0", "HOL.plus", "HOL.uminus", "HOL.minus", "1", "HOL.times"]
     1.8 +    find_index (fn a' => a = a') ["HOL.zero", "HOL.plus", "HOL.uminus", "HOL.minus", "HOL.one", "HOL.times"]
     1.9    | ring_ord _ = ~1;
    1.10  
    1.11  fun termless_ring (a, b) = (Term.term_lpo ring_ord (a, b) = LESS);
    1.12 @@ -22,7 +22,7 @@
    1.13  val plus = Const ("HOL.plus", [intT, intT]--->intT);
    1.14  val mult = Const ("HOL.times", [intT, intT]--->intT);
    1.15  val uminus = Const ("HOL.uminus", intT-->intT);
    1.16 -val one = Const ("1", intT);
    1.17 +val one = Const ("HOL.one", intT);
    1.18  val f = Const("f", intT-->intT);
    1.19  
    1.20  *)
     2.1 --- a/src/HOL/HOL.thy	Tue Sep 26 13:34:15 2006 +0200
     2.2 +++ b/src/HOL/HOL.thy	Tue Sep 26 13:34:16 2006 +0200
     2.3 @@ -191,11 +191,16 @@
     2.4  
     2.5  subsubsection {* Generic algebraic operations *}
     2.6  
     2.7 -axclass zero \<subseteq> type
     2.8 -axclass one \<subseteq> type
     2.9 +class zero =
    2.10 +  fixes zero :: "'a"                       ("\<^loc>0")
    2.11 +
    2.12 +class one =
    2.13 +  fixes one  :: "'a"                       ("\<^loc>1")
    2.14 +
    2.15 +hide (open) const zero one
    2.16  
    2.17  class plus =
    2.18 -  fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>+" 65)
    2.19 +  fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"   (infixl "\<^loc>+" 65)
    2.20  
    2.21  class minus =
    2.22    fixes uminus :: "'a \<Rightarrow> 'a" 
    2.23 @@ -203,31 +208,25 @@
    2.24    fixes abs    :: "'a \<Rightarrow> 'a"
    2.25  
    2.26  class times =
    2.27 -  fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>*" 70)
    2.28 +  fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<^loc>*" 70)
    2.29  
    2.30  class inverse = 
    2.31    fixes inverse :: "'a \<Rightarrow> 'a"
    2.32 -  fixes divide :: "'a \<Rightarrow> 'a => 'a" (infixl "\<^loc>'/" 70)
    2.33 -
    2.34 -global
    2.35 -
    2.36 -consts
    2.37 -  "0"           :: "'a::zero"                       ("0")
    2.38 -  "1"           :: "'a::one"                        ("1")
    2.39 +  fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>'/" 70)
    2.40  
    2.41  syntax
    2.42    "_index1"  :: index    ("\<^sub>1")
    2.43  translations
    2.44    (index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>"
    2.45  
    2.46 -local
    2.47 -
    2.48  typed_print_translation {*
    2.49 -  let
    2.50 -    fun tr' c = (c, fn show_sorts => fn T => fn ts =>
    2.51 -      if T = dummyT orelse not (! show_types) andalso can Term.dest_Type T then raise Match
    2.52 -      else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T);
    2.53 -  in [tr' "0", tr' "1"] end;
    2.54 +let
    2.55 +  fun tr' c = (c, fn show_sorts => fn T => fn ts =>
    2.56 +    if T = dummyT orelse not (! show_types) andalso can Term.dest_Type T then raise Match
    2.57 +    else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T);
    2.58 +in
    2.59 +  map (tr' o prefix Syntax.constN) ["HOL.one", "HOL.zero"]
    2.60 +end;
    2.61  *} -- {* show types that are presumably too general *}
    2.62  
    2.63  syntax
    2.64 @@ -1357,7 +1356,6 @@
    2.65  
    2.66  hide const induct_forall induct_implies induct_equal induct_conj
    2.67  
    2.68 -
    2.69  text {* Method setup. *}
    2.70  
    2.71  ML {*
     3.1 --- a/src/HOL/Hyperreal/NSA.thy	Tue Sep 26 13:34:15 2006 +0200
     3.2 +++ b/src/HOL/Hyperreal/NSA.thy	Tue Sep 26 13:34:16 2006 +0200
     3.3 @@ -675,12 +675,12 @@
     3.4    0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*)
     3.5  fun reorient_proc sg _ (_ $ t $ u) =
     3.6    case u of
     3.7 -      Const("0", _) => NONE
     3.8 -    | Const("1", _) => NONE
     3.9 +      Const("HOL.zero", _) => NONE
    3.10 +    | Const("HOL.one", _) => NONE
    3.11      | Const("Numeral.number_of", _) $ _ => NONE
    3.12      | _ => SOME (case t of
    3.13 -                Const("0", _) => meta_zero_approx_reorient
    3.14 -              | Const("1", _) => meta_one_approx_reorient
    3.15 +                Const("HOL.zero", _) => meta_zero_approx_reorient
    3.16 +              | Const("HOL.one", _) => meta_one_approx_reorient
    3.17                | Const("Numeral.number_of", _) $ _ =>
    3.18                                   meta_number_of_approx_reorient);
    3.19  
     4.1 --- a/src/HOL/Integ/IntDef.thy	Tue Sep 26 13:34:15 2006 +0200
     4.2 +++ b/src/HOL/Integ/IntDef.thy	Tue Sep 26 13:34:16 2006 +0200
     4.3 @@ -897,8 +897,8 @@
     4.4    unfolding zabs_def by auto
     4.5  
     4.6  consts_code
     4.7 -  "0" :: "int"                       ("0")
     4.8 -  "1" :: "int"                       ("1")
     4.9 +  "HOL.zero" :: "int"                ("0")
    4.10 +  "HOL.one" :: "int"                 ("1")
    4.11    "HOL.uminus" :: "int => int"       ("~")
    4.12    "HOL.plus" :: "int => int => int"  ("(_ +/ _)")
    4.13    "HOL.times" :: "int => int => int" ("(_ */ _)")
     5.1 --- a/src/HOL/Integ/cooper_dec.ML	Tue Sep 26 13:34:15 2006 +0200
     5.2 +++ b/src/HOL/Integ/cooper_dec.ML	Tue Sep 26 13:34:16 2006 +0200
     5.3 @@ -76,14 +76,14 @@
     5.4   
     5.5  (*Transform a natural number to a term*) 
     5.6   
     5.7 -fun mk_numeral 0 = Const("0",HOLogic.intT)
     5.8 -   |mk_numeral 1 = Const("1",HOLogic.intT)
     5.9 +fun mk_numeral 0 = Const("HOL.zero",HOLogic.intT)
    5.10 +   |mk_numeral 1 = Const("HOL.one",HOLogic.intT)
    5.11     |mk_numeral n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_binum n); 
    5.12   
    5.13  (*Transform an Term to an natural number*)	  
    5.14  	  
    5.15 -fun dest_numeral (Const("0",Type ("IntDef.int", []))) = 0
    5.16 -   |dest_numeral (Const("1",Type ("IntDef.int", []))) = 1
    5.17 +fun dest_numeral (Const("HOL.zero",Type ("IntDef.int", []))) = 0
    5.18 +   |dest_numeral (Const("HOL.one",Type ("IntDef.int", []))) = 1
    5.19     |dest_numeral (Const ("Numeral.number_of",_) $ n) = 
    5.20         HOLogic.dest_binum n;
    5.21  (*Some terms often used for pattern matching*) 
    5.22 @@ -659,8 +659,8 @@
    5.23      |mk_uni_vars T (Free (v,_)) = Free (v,T) 
    5.24      |mk_uni_vars T tm = tm; 
    5.25   
    5.26 -fun mk_uni_int T (Const ("0",T2)) = if T = T2 then (mk_numeral 0) else (Const ("0",T2)) 
    5.27 -    |mk_uni_int T (Const ("1",T2)) = if T = T2 then (mk_numeral 1) else (Const ("1",T2)) 
    5.28 +fun mk_uni_int T (Const ("HOL.zero",T2)) = if T = T2 then (mk_numeral 0) else (Const ("HOL.zero",T2)) 
    5.29 +    |mk_uni_int T (Const ("HOL.one",T2)) = if T = T2 then (mk_numeral 1) else (Const ("HOL.one",T2)) 
    5.30      |mk_uni_int T (node $ rest) = (mk_uni_int T node) $ (mk_uni_int T rest )  
    5.31      |mk_uni_int T (Abs(AV,AT,p)) = Abs(AV,AT,mk_uni_int T p) 
    5.32      |mk_uni_int T tm = tm; 
     6.1 --- a/src/HOL/Integ/cooper_proof.ML	Tue Sep 26 13:34:15 2006 +0200
     6.2 +++ b/src/HOL/Integ/cooper_proof.ML	Tue Sep 26 13:34:16 2006 +0200
     6.3 @@ -155,7 +155,7 @@
     6.4  
     6.5  (* ------------------------------------------------------------------------- *)
     6.6  (*This function norm_zero_one  replaces the occurences of Numeral1 and Numeral0*)
     6.7 -(*Respectively by their abstract representation Const("1",..) and COnst("0",..)*)
     6.8 +(*Respectively by their abstract representation Const("HOL.one",..) and Const("HOL.zero",..)*)
     6.9  (*this is necessary because the theorems use this representation.*)
    6.10  (* This function should be elminated in next versions...*)
    6.11  (* ------------------------------------------------------------------------- *)
    6.12 @@ -251,7 +251,7 @@
    6.13  (*==================================================*)
    6.14  
    6.15  fun decomp_adjustcoeffeq sg x l fm = case fm of
    6.16 -    (Const("Not",_)$(Const("Orderings.less",_) $(Const("0",_)) $(rt as (Const ("HOL.plus", _)$(Const ("HOL.times",_) $    c $ y ) $z )))) => 
    6.17 +    (Const("Not",_)$(Const("Orderings.less",_) $(Const("HOL.zero",_)) $(rt as (Const ("HOL.plus", _)$(Const ("HOL.times",_) $    c $ y ) $z )))) => 
    6.18       let  
    6.19          val m = l div (dest_numeral c) 
    6.20          val n = if (x = y) then abs (m) else 1
    6.21 @@ -264,7 +264,7 @@
    6.22          val ct = cterm_of sg z
    6.23          val cx = cterm_of sg y
    6.24          val pre = prove_elementar sg "lf" 
    6.25 -            (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),(mk_numeral n)))
    6.26 +            (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),(mk_numeral n)))
    6.27          val th1 = (pre RS (instantiate' [] [SOME ck,SOME cc, SOME cx, SOME ct] (ac_pi_eq)))
    6.28          in ([], fn [] => [th1,(prove_elementar sg "sa" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
    6.29          end
    6.30 @@ -288,21 +288,21 @@
    6.31  	case p of
    6.32  	  "Orderings.less" => 
    6.33  	let val pre = prove_elementar sg "lf" 
    6.34 -	    (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),(mk_numeral k)))
    6.35 +	    (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),(mk_numeral k)))
    6.36              val th1 = (pre RS (instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct] (ac_lt_eq)))
    6.37  	in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
    6.38           end
    6.39  
    6.40             |"op =" =>
    6.41  	     let val pre = prove_elementar sg "lf" 
    6.42 -	    (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("0",HOLogic.intT),(mk_numeral k))))
    6.43 +	    (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("HOL.zero",HOLogic.intT),(mk_numeral k))))
    6.44  	         val th1 = (pre RS(instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct] (ac_eq_eq)))
    6.45  	     in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
    6.46               end
    6.47  
    6.48               |"Divides.op dvd" =>
    6.49  	       let val pre = prove_elementar sg "lf" 
    6.50 -	   (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("0",HOLogic.intT),(mk_numeral k))))
    6.51 +	   (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("HOL.zero",HOLogic.intT),(mk_numeral k))))
    6.52                     val th1 = (pre RS (instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct]) (ac_dvd_eq))
    6.53                 in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
    6.54                          
    6.55 @@ -567,7 +567,7 @@
    6.56        if  (x=y) andalso (c1=zero) andalso (c2=one) 
    6.57  	 then let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ B)
    6.58  	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one  z)))
    6.59 -		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),dlcm))
    6.60 +		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),dlcm))
    6.61  	 in  (instantiate' [] [SOME cfma]([th3,th1,th2] MRS (not_bst_p_ne)))
    6.62  	 end
    6.63           else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
    6.64 @@ -576,8 +576,8 @@
    6.65       if (is_arith_rel at) andalso (x=y)
    6.66  	then let val bst_z = norm_zero_one (linear_neg (linear_add [] z (mk_numeral 1)))
    6.67  	         in let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ bst_z $ B)
    6.68 -	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq (bst_z,Const("HOL.minus",T) $ (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("1",HOLogic.intT))))
    6.69 -		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),dlcm))
    6.70 +	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq (bst_z,Const("HOL.minus",T) $ (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("HOL.one",HOLogic.intT))))
    6.71 +		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),dlcm))
    6.72  	 in  (instantiate' [] [SOME cfma] ([th3,th1,th2] MRS (not_bst_p_eq)))
    6.73  	 end
    6.74         end
    6.75 @@ -590,7 +590,7 @@
    6.76                val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
    6.77  	  in  (instantiate' [] [SOME cfma,  SOME cdlcm]([th1,th2] MRS (not_bst_p_gt)))
    6.78  	    end
    6.79 -	 else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),dlcm))
    6.80 +	 else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),dlcm))
    6.81  	      in (instantiate' [] [SOME cfma, SOME cB,SOME (cterm_of sg (norm_zero_one z))] (th1 RS (not_bst_p_lt)))
    6.82  	      end
    6.83        else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
    6.84 @@ -658,7 +658,7 @@
    6.85        if  (x=y) andalso (c1=zero) andalso (c2=one) 
    6.86  	 then let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ A)
    6.87  	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one  z)))
    6.88 -		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),dlcm))
    6.89 +		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),dlcm))
    6.90  	 in  (instantiate' [] [SOME cfma]([th3,th1,th2] MRS (not_ast_p_ne)))
    6.91  	 end
    6.92           else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
    6.93 @@ -667,8 +667,8 @@
    6.94       if (is_arith_rel at) andalso (x=y)
    6.95  	then let val ast_z = norm_zero_one (linear_sub [] one z )
    6.96  	         val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ ast_z $ A)
    6.97 -	         val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq (ast_z,Const("HOL.plus",T) $ (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("1",HOLogic.intT))))
    6.98 -		 val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),dlcm))
    6.99 +	         val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq (ast_z,Const("HOL.plus",T) $ (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("HOL.one",HOLogic.intT))))
   6.100 +		 val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),dlcm))
   6.101  	 in  (instantiate' [] [SOME cfma] ([th3,th1,th2] MRS (not_ast_p_eq)))
   6.102         end
   6.103           else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
   6.104 @@ -680,7 +680,7 @@
   6.105                val th2 =  prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (zero,dlcm))
   6.106  	  in  (instantiate' [] [SOME cfma]([th2,th1] MRS (not_ast_p_lt)))
   6.107  	    end
   6.108 -	 else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),dlcm))
   6.109 +	 else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),dlcm))
   6.110  	      in (instantiate' [] [SOME cfma, SOME cA,SOME (cterm_of sg (norm_zero_one z))] (th1 RS (not_ast_p_gt)))
   6.111  	      end
   6.112        else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
     7.1 --- a/src/HOL/Integ/int_arith1.ML	Tue Sep 26 13:34:15 2006 +0200
     7.2 +++ b/src/HOL/Integ/int_arith1.ML	Tue Sep 26 13:34:16 2006 +0200
     7.3 @@ -118,12 +118,12 @@
     7.4      0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*)
     7.5    fun reorient_proc sg _ (_ $ t $ u) =
     7.6      case u of
     7.7 -	Const("0", _) => NONE
     7.8 -      | Const("1", _) => NONE
     7.9 +	Const("HOL.zero", _) => NONE
    7.10 +      | Const("HOL.one", _) => NONE
    7.11        | Const("Numeral.number_of", _) $ _ => NONE
    7.12        | _ => SOME (case t of
    7.13 -		  Const("0", _) => meta_zero_reorient
    7.14 -		| Const("1", _) => meta_one_reorient
    7.15 +		  Const("HOL.zero", _) => meta_zero_reorient
    7.16 +		| Const("HOL.one", _) => meta_one_reorient
    7.17  		| Const("Numeral.number_of", _) $ _ => meta_number_of_reorient)
    7.18  
    7.19    val reorient_simproc = 
    7.20 @@ -184,8 +184,8 @@
    7.21  fun mk_numeral T n = HOLogic.number_of_const T $ HOLogic.mk_binum n;
    7.22  
    7.23  (*Decodes a binary INTEGER*)
    7.24 -fun dest_numeral (Const("0", _)) = 0
    7.25 -  | dest_numeral (Const("1", _)) = 1
    7.26 +fun dest_numeral (Const("HOL.zero", _)) = 0
    7.27 +  | dest_numeral (Const("HOL.one", _)) = 1
    7.28    | dest_numeral (Const("Numeral.number_of", _) $ w) =
    7.29       (HOLogic.dest_binum w
    7.30        handle TERM _ => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
     8.1 --- a/src/HOL/Integ/nat_simprocs.ML	Tue Sep 26 13:34:15 2006 +0200
     8.2 +++ b/src/HOL/Integ/nat_simprocs.ML	Tue Sep 26 13:34:16 2006 +0200
     8.3 @@ -26,7 +26,7 @@
     8.4  fun mk_numeral n = HOLogic.number_of_const HOLogic.natT $ HOLogic.mk_binum n;
     8.5  
     8.6  (*Decodes a unary or binary numeral to a NATURAL NUMBER*)
     8.7 -fun dest_numeral (Const ("0", _)) = 0
     8.8 +fun dest_numeral (Const ("HOL.zero", _)) = 0
     8.9    | dest_numeral (Const ("Suc", _) $ t) = 1 + dest_numeral t
    8.10    | dest_numeral (Const("Numeral.number_of", _) $ w) =
    8.11        (IntInf.max (0, HOLogic.dest_binum w)
     9.1 --- a/src/HOL/Integ/presburger.ML	Tue Sep 26 13:34:15 2006 +0200
     9.2 +++ b/src/HOL/Integ/presburger.ML	Tue Sep 26 13:34:16 2006 +0200
     9.3 @@ -166,10 +166,10 @@
     9.4     ("Numeral.Min", iT),
     9.5     ("Numeral.number_of", iT --> iT),
     9.6     ("Numeral.number_of", iT --> nT),
     9.7 -   ("0", nT),
     9.8 -   ("0", iT),
     9.9 -   ("1", nT),
    9.10 -   ("1", iT),
    9.11 +   ("HOL.zero", nT),
    9.12 +   ("HOL.zero", iT),
    9.13 +   ("HOL.one", nT),
    9.14 +   ("HOL.one", iT),
    9.15     ("False", bT),
    9.16     ("True", bT)];
    9.17  
    10.1 --- a/src/HOL/Integ/reflected_cooper.ML	Tue Sep 26 13:34:15 2006 +0200
    10.2 +++ b/src/HOL/Integ/reflected_cooper.ML	Tue Sep 26 13:34:16 2006 +0200
    10.3 @@ -13,8 +13,8 @@
    10.4  	Free(xn,xT) => (case AList.lookup (op =) vs t of 
    10.5  			   NONE   => error "Variable not found in the list!!"
    10.6  			 | SOME n => Var n)
    10.7 -      | Const("0",iT) => Cst 0
    10.8 -      | Const("1",iT) => Cst 1
    10.9 +      | Const("HOL.zero",iT) => Cst 0
   10.10 +      | Const("HOL.one",iT) => Cst 1
   10.11        | Bound i => Var (nat (IntInf.fromInt i))
   10.12        | Const("HOL.uminus",_)$t' => Neg (i_of_term vs t')
   10.13        | Const ("HOL.plus",_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
    11.1 --- a/src/HOL/Lambda/WeakNorm.thy	Tue Sep 26 13:34:15 2006 +0200
    11.2 +++ b/src/HOL/Lambda/WeakNorm.thy	Tue Sep 26 13:34:16 2006 +0200
    11.3 @@ -517,10 +517,10 @@
    11.4  *}
    11.5  
    11.6  ML {*
    11.7 -fun nat_of_int 0 = Norm.id_0
    11.8 +fun nat_of_int 0 = Norm.zero
    11.9    | nat_of_int n = Norm.Suc (nat_of_int (n-1));
   11.10  
   11.11 -fun int_of_nat Norm.id_0 = 0
   11.12 +fun int_of_nat Norm.zero = 0
   11.13    | int_of_nat (Norm.Suc n) = 1 + int_of_nat n;
   11.14  
   11.15  fun dBtype_of_typ (Type ("fun", [T, U])) =
   11.16 @@ -558,7 +558,7 @@
   11.17        let val dBT = dBtype_of_typ T
   11.18        in Norm.rtypingT_Abs (e, dBT, dB_of_term t,
   11.19          dBtype_of_typ (fastype_of1 (T :: Ts, t)),
   11.20 -        typing_of_term (T :: Ts) (Norm.shift e Norm.id_0 dBT) t)
   11.21 +        typing_of_term (T :: Ts) (Norm.shift e Norm.zero dBT) t)
   11.22        end
   11.23    | typing_of_term _ _ _ = error "typing_of_term: bad term";
   11.24  
    12.1 --- a/src/HOL/Library/EfficientNat.thy	Tue Sep 26 13:34:15 2006 +0200
    12.2 +++ b/src/HOL/Library/EfficientNat.thy	Tue Sep 26 13:34:16 2006 +0200
    12.3 @@ -127,8 +127,8 @@
    12.4  types_code
    12.5    nat ("int")
    12.6  attach (term_of) {*
    12.7 -fun term_of_nat 0 = Const ("0", HOLogic.natT)
    12.8 -  | term_of_nat 1 = Const ("1", HOLogic.natT)
    12.9 +fun term_of_nat 0 = Const ("HOL.zero", HOLogic.natT)
   12.10 +  | term_of_nat 1 = Const ("HOL.one", HOLogic.natT)
   12.11    | term_of_nat i = HOLogic.number_of_const HOLogic.natT $
   12.12        HOLogic.mk_binum (IntInf.fromInt i);
   12.13  *}
   12.14 @@ -141,7 +141,7 @@
   12.15    (Haskell target_atom "Integer")
   12.16  
   12.17  consts_code
   12.18 -  0 :: nat ("0")
   12.19 +  "HOL.zero" :: nat ("0")
   12.20    Suc ("(_ + 1)")
   12.21  
   12.22  text {*
    13.1 --- a/src/HOL/Library/ExecutableRat.thy	Tue Sep 26 13:34:15 2006 +0200
    13.2 +++ b/src/HOL/Library/ExecutableRat.thy	Tue Sep 26 13:34:16 2006 +0200
    13.3 @@ -131,8 +131,8 @@
    13.4  consts_code
    13.5    div_zero ("raise/ (Fail/ \"non-defined rational number\")")
    13.6    Fract ("{*of_quotient*}")
    13.7 -  0 :: rat ("{*0::erat*}")
    13.8 -  1 :: rat ("{*1::erat*}")
    13.9 +  HOL.zero :: rat ("{*0::erat*}")
   13.10 +  HOL.one :: rat ("{*1::erat*}")
   13.11    HOL.plus :: "rat \<Rightarrow> rat \<Rightarrow> rat" ("{*op + :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
   13.12    uminus :: "rat \<Rightarrow> rat" ("{*uminus :: erat \<Rightarrow> erat*}")
   13.13    HOL.times :: "rat \<Rightarrow> rat \<Rightarrow> rat" ("{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
    14.1 --- a/src/HOL/Library/comm_ring.ML	Tue Sep 26 13:34:15 2006 +0200
    14.2 +++ b/src/HOL/Library/comm_ring.ML	Tue Sep 26 13:34:16 2006 +0200
    14.3 @@ -17,8 +17,8 @@
    14.4  exception CRing of string;
    14.5  
    14.6  (* Zero and One of the commutative ring *)
    14.7 -fun cring_zero T = Const("0",T);
    14.8 -fun cring_one T = Const("1",T);
    14.9 +fun cring_zero T = Const("HOL.zero",T);
   14.10 +fun cring_one T = Const("HOL.one",T);
   14.11  
   14.12  (* reification functions *)
   14.13  (* add two polynom expressions *)
   14.14 @@ -30,8 +30,8 @@
   14.15  (* Reification of the constructors *)
   14.16  (* Nat*)
   14.17  val succ = Const("Suc",nT --> nT);
   14.18 -val zero = Const("0",nT);
   14.19 -val one = Const("1",nT);
   14.20 +val zero = Const("HOL.zero",nT);
   14.21 +val one = Const("HOL.one",nT);
   14.22  
   14.23  (* Lists *)
   14.24  fun reif_list T [] = Const("List.list.Nil",listT T)
    15.1 --- a/src/HOL/Nat.thy	Tue Sep 26 13:34:15 2006 +0200
    15.2 +++ b/src/HOL/Nat.thy	Tue Sep 26 13:34:16 2006 +0200
    15.3 @@ -112,7 +112,7 @@
    15.4  rep_datatype nat
    15.5    distinct  Suc_not_Zero Zero_not_Suc
    15.6    inject    Suc_Suc_eq
    15.7 -  induction nat_induct
    15.8 +  induction nat_induct [case_names 0 Suc]
    15.9  
   15.10  lemma n_not_Suc_n: "n \<noteq> Suc n"
   15.11    by (induct n) simp_all
   15.12 @@ -1067,6 +1067,8 @@
   15.13  
   15.14  code_instname
   15.15    nat :: eq "IntDef.eq_nat"
   15.16 +  nat :: zero "IntDef.zero_nat"
   15.17 +  nat :: one "IntDef.one_nat"
   15.18    nat :: ord "IntDef.ord_nat"
   15.19    nat :: plus "IntDef.plus_nat"
   15.20    nat :: minus "IntDef.minus_nat"
    16.1 --- a/src/HOL/OrderedGroup.ML	Tue Sep 26 13:34:15 2006 +0200
    16.2 +++ b/src/HOL/OrderedGroup.ML	Tue Sep 26 13:34:16 2006 +0200
    16.3 @@ -8,7 +8,7 @@
    16.4  
    16.5  (*** Term order for abelian groups ***)
    16.6  
    16.7 -fun agrp_ord (Const (a, _)) = find_index (fn a' => a = a') ["0", "HOL.plus", "HOL.uminus", "HOL.minus"]
    16.8 +fun agrp_ord (Const (a, _)) = find_index (fn a' => a = a') ["HOL.zero", "HOL.plus", "HOL.uminus", "HOL.minus"]
    16.9    | agrp_ord _ = ~1;
   16.10  
   16.11  fun termless_agrp (a, b) = (Term.term_lpo agrp_ord (a, b) = LESS);
    17.1 --- a/src/HOL/Prolog/Func.thy	Tue Sep 26 13:34:15 2006 +0200
    17.2 +++ b/src/HOL/Prolog/Func.thy	Tue Sep 26 13:34:16 2006 +0200
    17.3 @@ -23,7 +23,7 @@
    17.4    "and"   :: "tm => tm => tm"       (infixr 999)
    17.5    "eq"    :: "tm => tm => tm"       (infixr 999)
    17.6  
    17.7 -  "0"     :: tm                   ("Z")
    17.8 +  Z       :: tm                     ("Z")
    17.9    S       :: "tm => tm"
   17.10  (*
   17.11          "++", "--",
    18.1 --- a/src/HOL/Prolog/Type.ML	Tue Sep 26 13:34:15 2006 +0200
    18.2 +++ b/src/HOL/Prolog/Type.ML	Tue Sep 26 13:34:16 2006 +0200
    18.3 @@ -11,13 +11,13 @@
    18.4  
    18.5  pgoal "typeof (fix (%x. x)) ?T";
    18.6  
    18.7 -pgoal "typeof (fix (%fact. abs(%n. (app fact (n - 0))))) ?T";
    18.8 +pgoal "typeof (fix (%fact. abs(%n. (app fact (n - Z))))) ?T";
    18.9  
   18.10 -pgoal "typeof (fix (%fact. abs(%n. cond (n eq 0) (S 0) \
   18.11 -				\(n * (app fact (n - (S 0))))))) ?T";
   18.12 +pgoal "typeof (fix (%fact. abs(%n. cond (n eq Z) (S Z) \
   18.13 +  \(n * (app fact (n - (S Z))))))) ?T";
   18.14  
   18.15 -pgoal "typeof (abs(%v. 0)) ?T"; (*correct only solution (?A1 -> nat) *)
   18.16 -Goal "typeof (abs(%v. 0)) ?T";
   18.17 +pgoal "typeof (abs(%v. Z)) ?T"; (*correct only solution (?A1 -> nat) *)
   18.18 +Goal "typeof (abs(%v. Z)) ?T";
   18.19  by (prolog_tac [bad1_typeof,common_typeof]); (* 1st result ok*)
   18.20  back(); (* 2nd result (?A1 -> ?A1) wrong *)
   18.21  
    19.1 --- a/src/HOL/Real/ferrante_rackoff_proof.ML	Tue Sep 26 13:34:15 2006 +0200
    19.2 +++ b/src/HOL/Real/ferrante_rackoff_proof.ML	Tue Sep 26 13:34:16 2006 +0200
    19.3 @@ -287,16 +287,16 @@
    19.4  
    19.5  
    19.6      (* Normalization of arithmetical expressions *)
    19.7 -val rzero = Const("0",rT);
    19.8 -val rone = Const("1",rT);
    19.9 +val rzero = Const("HOL.zero",rT);
   19.10 +val rone = Const("HOL.one",rT);
   19.11  fun mk_real i = 
   19.12      case i of 
   19.13          0 => rzero
   19.14        | 1 => rone
   19.15        | _ => (HOLogic.number_of_const rT)$(HOLogic.mk_binum i); 
   19.16  
   19.17 -fun dest_real (Const("0",_)) = 0
   19.18 -  | dest_real (Const("1",_)) = 1
   19.19 +fun dest_real (Const("HOL.zero",_)) = 0
   19.20 +  | dest_real (Const("HOL.one",_)) = 1
   19.21    | dest_real (Const("Numeral.number_of",_)$b) = HOLogic.dest_binum b;
   19.22  
   19.23          (* Normal form for terms is: 
    20.1 --- a/src/HOL/Tools/Presburger/cooper_dec.ML	Tue Sep 26 13:34:15 2006 +0200
    20.2 +++ b/src/HOL/Tools/Presburger/cooper_dec.ML	Tue Sep 26 13:34:16 2006 +0200
    20.3 @@ -76,14 +76,14 @@
    20.4   
    20.5  (*Transform a natural number to a term*) 
    20.6   
    20.7 -fun mk_numeral 0 = Const("0",HOLogic.intT)
    20.8 -   |mk_numeral 1 = Const("1",HOLogic.intT)
    20.9 +fun mk_numeral 0 = Const("HOL.zero",HOLogic.intT)
   20.10 +   |mk_numeral 1 = Const("HOL.one",HOLogic.intT)
   20.11     |mk_numeral n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_binum n); 
   20.12   
   20.13  (*Transform an Term to an natural number*)	  
   20.14  	  
   20.15 -fun dest_numeral (Const("0",Type ("IntDef.int", []))) = 0
   20.16 -   |dest_numeral (Const("1",Type ("IntDef.int", []))) = 1
   20.17 +fun dest_numeral (Const("HOL.zero",Type ("IntDef.int", []))) = 0
   20.18 +   |dest_numeral (Const("HOL.one",Type ("IntDef.int", []))) = 1
   20.19     |dest_numeral (Const ("Numeral.number_of",_) $ n) = 
   20.20         HOLogic.dest_binum n;
   20.21  (*Some terms often used for pattern matching*) 
   20.22 @@ -659,8 +659,8 @@
   20.23      |mk_uni_vars T (Free (v,_)) = Free (v,T) 
   20.24      |mk_uni_vars T tm = tm; 
   20.25   
   20.26 -fun mk_uni_int T (Const ("0",T2)) = if T = T2 then (mk_numeral 0) else (Const ("0",T2)) 
   20.27 -    |mk_uni_int T (Const ("1",T2)) = if T = T2 then (mk_numeral 1) else (Const ("1",T2)) 
   20.28 +fun mk_uni_int T (Const ("HOL.zero",T2)) = if T = T2 then (mk_numeral 0) else (Const ("HOL.zero",T2)) 
   20.29 +    |mk_uni_int T (Const ("HOL.one",T2)) = if T = T2 then (mk_numeral 1) else (Const ("HOL.one",T2)) 
   20.30      |mk_uni_int T (node $ rest) = (mk_uni_int T node) $ (mk_uni_int T rest )  
   20.31      |mk_uni_int T (Abs(AV,AT,p)) = Abs(AV,AT,mk_uni_int T p) 
   20.32      |mk_uni_int T tm = tm; 
    21.1 --- a/src/HOL/Tools/Presburger/cooper_proof.ML	Tue Sep 26 13:34:15 2006 +0200
    21.2 +++ b/src/HOL/Tools/Presburger/cooper_proof.ML	Tue Sep 26 13:34:16 2006 +0200
    21.3 @@ -155,7 +155,7 @@
    21.4  
    21.5  (* ------------------------------------------------------------------------- *)
    21.6  (*This function norm_zero_one  replaces the occurences of Numeral1 and Numeral0*)
    21.7 -(*Respectively by their abstract representation Const("1",..) and COnst("0",..)*)
    21.8 +(*Respectively by their abstract representation Const("HOL.one",..) and Const("HOL.zero",..)*)
    21.9  (*this is necessary because the theorems use this representation.*)
   21.10  (* This function should be elminated in next versions...*)
   21.11  (* ------------------------------------------------------------------------- *)
   21.12 @@ -251,7 +251,7 @@
   21.13  (*==================================================*)
   21.14  
   21.15  fun decomp_adjustcoeffeq sg x l fm = case fm of
   21.16 -    (Const("Not",_)$(Const("Orderings.less",_) $(Const("0",_)) $(rt as (Const ("HOL.plus", _)$(Const ("HOL.times",_) $    c $ y ) $z )))) => 
   21.17 +    (Const("Not",_)$(Const("Orderings.less",_) $(Const("HOL.zero",_)) $(rt as (Const ("HOL.plus", _)$(Const ("HOL.times",_) $    c $ y ) $z )))) => 
   21.18       let  
   21.19          val m = l div (dest_numeral c) 
   21.20          val n = if (x = y) then abs (m) else 1
   21.21 @@ -264,7 +264,7 @@
   21.22          val ct = cterm_of sg z
   21.23          val cx = cterm_of sg y
   21.24          val pre = prove_elementar sg "lf" 
   21.25 -            (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),(mk_numeral n)))
   21.26 +            (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),(mk_numeral n)))
   21.27          val th1 = (pre RS (instantiate' [] [SOME ck,SOME cc, SOME cx, SOME ct] (ac_pi_eq)))
   21.28          in ([], fn [] => [th1,(prove_elementar sg "sa" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
   21.29          end
   21.30 @@ -288,21 +288,21 @@
   21.31  	case p of
   21.32  	  "Orderings.less" => 
   21.33  	let val pre = prove_elementar sg "lf" 
   21.34 -	    (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),(mk_numeral k)))
   21.35 +	    (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),(mk_numeral k)))
   21.36              val th1 = (pre RS (instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct] (ac_lt_eq)))
   21.37  	in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
   21.38           end
   21.39  
   21.40             |"op =" =>
   21.41  	     let val pre = prove_elementar sg "lf" 
   21.42 -	    (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("0",HOLogic.intT),(mk_numeral k))))
   21.43 +	    (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("HOL.zero",HOLogic.intT),(mk_numeral k))))
   21.44  	         val th1 = (pre RS(instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct] (ac_eq_eq)))
   21.45  	     in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
   21.46               end
   21.47  
   21.48               |"Divides.op dvd" =>
   21.49  	       let val pre = prove_elementar sg "lf" 
   21.50 -	   (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("0",HOLogic.intT),(mk_numeral k))))
   21.51 +	   (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("HOL.zero",HOLogic.intT),(mk_numeral k))))
   21.52                     val th1 = (pre RS (instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct]) (ac_dvd_eq))
   21.53                 in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
   21.54                          
   21.55 @@ -567,7 +567,7 @@
   21.56        if  (x=y) andalso (c1=zero) andalso (c2=one) 
   21.57  	 then let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ B)
   21.58  	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one  z)))
   21.59 -		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),dlcm))
   21.60 +		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),dlcm))
   21.61  	 in  (instantiate' [] [SOME cfma]([th3,th1,th2] MRS (not_bst_p_ne)))
   21.62  	 end
   21.63           else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
   21.64 @@ -576,8 +576,8 @@
   21.65       if (is_arith_rel at) andalso (x=y)
   21.66  	then let val bst_z = norm_zero_one (linear_neg (linear_add [] z (mk_numeral 1)))
   21.67  	         in let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ bst_z $ B)
   21.68 -	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq (bst_z,Const("HOL.minus",T) $ (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("1",HOLogic.intT))))
   21.69 -		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),dlcm))
   21.70 +	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq (bst_z,Const("HOL.minus",T) $ (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("HOL.one",HOLogic.intT))))
   21.71 +		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),dlcm))
   21.72  	 in  (instantiate' [] [SOME cfma] ([th3,th1,th2] MRS (not_bst_p_eq)))
   21.73  	 end
   21.74         end
   21.75 @@ -590,7 +590,7 @@
   21.76                val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
   21.77  	  in  (instantiate' [] [SOME cfma,  SOME cdlcm]([th1,th2] MRS (not_bst_p_gt)))
   21.78  	    end
   21.79 -	 else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),dlcm))
   21.80 +	 else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),dlcm))
   21.81  	      in (instantiate' [] [SOME cfma, SOME cB,SOME (cterm_of sg (norm_zero_one z))] (th1 RS (not_bst_p_lt)))
   21.82  	      end
   21.83        else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
   21.84 @@ -658,7 +658,7 @@
   21.85        if  (x=y) andalso (c1=zero) andalso (c2=one) 
   21.86  	 then let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ A)
   21.87  	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one  z)))
   21.88 -		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),dlcm))
   21.89 +		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),dlcm))
   21.90  	 in  (instantiate' [] [SOME cfma]([th3,th1,th2] MRS (not_ast_p_ne)))
   21.91  	 end
   21.92           else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
   21.93 @@ -667,8 +667,8 @@
   21.94       if (is_arith_rel at) andalso (x=y)
   21.95  	then let val ast_z = norm_zero_one (linear_sub [] one z )
   21.96  	         val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ ast_z $ A)
   21.97 -	         val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq (ast_z,Const("HOL.plus",T) $ (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("1",HOLogic.intT))))
   21.98 -		 val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),dlcm))
   21.99 +	         val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq (ast_z,Const("HOL.plus",T) $ (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("HOL.one",HOLogic.intT))))
  21.100 +		 val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),dlcm))
  21.101  	 in  (instantiate' [] [SOME cfma] ([th3,th1,th2] MRS (not_ast_p_eq)))
  21.102         end
  21.103           else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
  21.104 @@ -680,7 +680,7 @@
  21.105                val th2 =  prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (zero,dlcm))
  21.106  	  in  (instantiate' [] [SOME cfma]([th2,th1] MRS (not_ast_p_lt)))
  21.107  	    end
  21.108 -	 else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),dlcm))
  21.109 +	 else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),dlcm))
  21.110  	      in (instantiate' [] [SOME cfma, SOME cA,SOME (cterm_of sg (norm_zero_one z))] (th1 RS (not_ast_p_gt)))
  21.111  	      end
  21.112        else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
    22.1 --- a/src/HOL/Tools/Presburger/presburger.ML	Tue Sep 26 13:34:15 2006 +0200
    22.2 +++ b/src/HOL/Tools/Presburger/presburger.ML	Tue Sep 26 13:34:16 2006 +0200
    22.3 @@ -166,10 +166,10 @@
    22.4     ("Numeral.Min", iT),
    22.5     ("Numeral.number_of", iT --> iT),
    22.6     ("Numeral.number_of", iT --> nT),
    22.7 -   ("0", nT),
    22.8 -   ("0", iT),
    22.9 -   ("1", nT),
   22.10 -   ("1", iT),
   22.11 +   ("HOL.zero", nT),
   22.12 +   ("HOL.zero", iT),
   22.13 +   ("HOL.one", nT),
   22.14 +   ("HOL.one", iT),
   22.15     ("False", bT),
   22.16     ("True", bT)];
   22.17  
    23.1 --- a/src/HOL/Tools/Presburger/reflected_cooper.ML	Tue Sep 26 13:34:15 2006 +0200
    23.2 +++ b/src/HOL/Tools/Presburger/reflected_cooper.ML	Tue Sep 26 13:34:16 2006 +0200
    23.3 @@ -13,8 +13,8 @@
    23.4  	Free(xn,xT) => (case AList.lookup (op =) vs t of 
    23.5  			   NONE   => error "Variable not found in the list!!"
    23.6  			 | SOME n => Var n)
    23.7 -      | Const("0",iT) => Cst 0
    23.8 -      | Const("1",iT) => Cst 1
    23.9 +      | Const("HOL.zero",iT) => Cst 0
   23.10 +      | Const("HOL.one",iT) => Cst 1
   23.11        | Bound i => Var (nat (IntInf.fromInt i))
   23.12        | Const("HOL.uminus",_)$t' => Neg (i_of_term vs t')
   23.13        | Const ("HOL.plus",_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
    24.1 --- a/src/HOL/arith_data.ML	Tue Sep 26 13:34:15 2006 +0200
    24.2 +++ b/src/HOL/arith_data.ML	Tue Sep 26 13:34:16 2006 +0200
    24.3 @@ -324,8 +324,8 @@
    24.4            demult (t, Rat.mult (m, Rat.inv (Rat.rat_of_intinf den)))
    24.5        end
    24.6          handle TERM _ => (SOME atom, m))
    24.7 -    | demult (Const ("0", _), m) = (NONE, Rat.rat_of_int 0)
    24.8 -    | demult (Const ("1", _), m) = (NONE, m)
    24.9 +    | demult (Const ("HOL.zero", _), m) = (NONE, Rat.rat_of_int 0)
   24.10 +    | demult (Const ("HOL.one", _), m) = (NONE, m)
   24.11      | demult (t as Const ("Numeral.number_of", _) $ n, m) =
   24.12          ((NONE, Rat.mult (m, Rat.rat_of_intinf (HOLogic.dest_binum n)))
   24.13            handle TERM _ => (SOME t,m))
   24.14 @@ -350,9 +350,9 @@
   24.15          if nT T then add_atom all m pi else poly (s, m, poly (t, Rat.neg m, pi))
   24.16      | poly (all as Const ("HOL.uminus", T) $ t, m, pi) =
   24.17          if nT T then add_atom all m pi else poly (t, Rat.neg m, pi)
   24.18 -    | poly (Const ("0", _), _, pi) =
   24.19 +    | poly (Const ("HOL.zero", _), _, pi) =
   24.20          pi
   24.21 -    | poly (Const ("1", _), m, (p, i)) =
   24.22 +    | poly (Const ("HOL.one", _), m, (p, i)) =
   24.23          (p, Rat.add (i, m))
   24.24      | poly (Const ("Suc", _) $ t, m, (p, i)) =
   24.25          poly (t, m, (p, Rat.add (i, m)))
   24.26 @@ -558,7 +558,7 @@
   24.27          val terms1      = map (subst_term [(split_term, t1)]) rev_terms
   24.28          val terms2      = map (subst_term [(split_term, Const ("HOL.uminus",
   24.29                              split_type --> split_type) $ t1)]) rev_terms
   24.30 -        val zero        = Const ("0", split_type)
   24.31 +        val zero        = Const ("HOL.zero", split_type)
   24.32          val zero_leq_t1 = Const ("Orderings.less_eq",
   24.33                              split_type --> split_type --> HOLogic.boolT) $ zero $ t1
   24.34          val t1_lt_zero  = Const ("Orderings.less",
   24.35 @@ -575,7 +575,7 @@
   24.36          (* "d" in the above theorem becomes a new bound variable after NNF   *)
   24.37          (* transformation, therefore some adjustment of indices is necessary *)
   24.38          val rev_terms       = rev terms
   24.39 -        val zero            = Const ("0", split_type)
   24.40 +        val zero            = Const ("HOL.zero", split_type)
   24.41          val d               = Bound 0
   24.42          val terms1          = map (subst_term [(split_term, zero)]) rev_terms
   24.43          val terms2          = map (subst_term [(incr_boundvars 1 split_term, d)])
   24.44 @@ -597,8 +597,8 @@
   24.45      | (Const ("IntDef.nat", _), [t1]) =>
   24.46        let
   24.47          val rev_terms   = rev terms
   24.48 -        val zero_int    = Const ("0", HOLogic.intT)
   24.49 -        val zero_nat    = Const ("0", HOLogic.natT)
   24.50 +        val zero_int    = Const ("HOL.zero", HOLogic.intT)
   24.51 +        val zero_nat    = Const ("HOL.zero", HOLogic.natT)
   24.52          val n           = Bound 0
   24.53          val terms1      = map (subst_term [(incr_boundvars 1 split_term, n)])
   24.54                              (map (incr_boundvars 1) rev_terms)
   24.55 @@ -620,7 +620,7 @@
   24.56      | (Const ("Divides.op mod", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
   24.57        let
   24.58          val rev_terms               = rev terms
   24.59 -        val zero                    = Const ("0", split_type)
   24.60 +        val zero                    = Const ("HOL.zero", split_type)
   24.61          val i                       = Bound 1
   24.62          val j                       = Bound 0
   24.63          val terms1                  = map (subst_term [(split_term, t1)]) rev_terms
   24.64 @@ -652,7 +652,7 @@
   24.65      | (Const ("Divides.op div", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
   24.66        let
   24.67          val rev_terms               = rev terms
   24.68 -        val zero                    = Const ("0", split_type)
   24.69 +        val zero                    = Const ("HOL.zero", split_type)
   24.70          val i                       = Bound 1
   24.71          val j                       = Bound 0
   24.72          val terms1                  = map (subst_term [(split_term, zero)]) rev_terms
   24.73 @@ -688,7 +688,7 @@
   24.74          Type ("fun", [Type ("IntDef.int", []), _])), [t1, t2 as (number_of $ k)]) =>
   24.75        let
   24.76          val rev_terms               = rev terms
   24.77 -        val zero                    = Const ("0", split_type)
   24.78 +        val zero                    = Const ("HOL.zero", split_type)
   24.79          val i                       = Bound 1
   24.80          val j                       = Bound 0
   24.81          val terms1                  = map (subst_term [(split_term, t1)]) rev_terms
   24.82 @@ -740,7 +740,7 @@
   24.83          Type ("fun", [Type ("IntDef.int", []), _])), [t1, t2 as (number_of $ k)]) =>
   24.84        let
   24.85          val rev_terms               = rev terms
   24.86 -        val zero                    = Const ("0", split_type)
   24.87 +        val zero                    = Const ("HOL.zero", split_type)
   24.88          val i                       = Bound 1
   24.89          val j                       = Bound 0
   24.90          val terms1                  = map (subst_term [(split_term, zero)]) rev_terms
    25.1 --- a/src/HOL/ex/Abstract_NAT.thy	Tue Sep 26 13:34:15 2006 +0200
    25.2 +++ b/src/HOL/ex/Abstract_NAT.thy	Tue Sep 26 13:34:16 2006 +0200
    25.3 @@ -31,11 +31,11 @@
    25.4  
    25.5  consts
    25.6    REC :: "'n \<Rightarrow> ('n \<Rightarrow> 'n) \<Rightarrow> 'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('n * 'a) set"
    25.7 -inductive "REC zero succ e r"
    25.8 +inductive "REC zer succ e r"
    25.9    intros
   25.10 -    Rec_zero: "NAT zero succ \<Longrightarrow> (zero, e) \<in> REC zero succ e r"
   25.11 -    Rec_succ: "NAT zero succ \<Longrightarrow> (m, n) \<in> REC zero succ e r \<Longrightarrow>
   25.12 -      (succ m, r m n) \<in> REC zero succ e r"
   25.13 +    Rec_zero: "NAT zer succ \<Longrightarrow> (zer, e) \<in> REC zer succ e r"
   25.14 +    Rec_succ: "NAT zer succ \<Longrightarrow> (m, n) \<in> REC zer succ e r \<Longrightarrow>
   25.15 +      (succ m, r m n) \<in> REC zer succ e r"
   25.16  
   25.17  abbreviation (in NAT)
   25.18    "Rec == REC zero succ"
    26.1 --- a/src/HOL/ex/Codegenerator.thy	Tue Sep 26 13:34:15 2006 +0200
    26.2 +++ b/src/HOL/ex/Codegenerator.thy	Tue Sep 26 13:34:16 2006 +0200
    26.3 @@ -17,8 +17,6 @@
    26.4  subsection {* natural numbers *}
    26.5  
    26.6  definition
    26.7 -  one :: nat
    26.8 -  "one = 1"
    26.9    n :: nat
   26.10    "n = 42"
   26.11  
   26.12 @@ -105,8 +103,10 @@
   26.13  definition
   26.14    "shadow keywords = keywords @ [Codegenerator.keywords 0 0 0 0 0 0]"
   26.15  
   26.16 -code_gen xor
   26.17 -code_gen one
   26.18 +code_gen
   26.19 +  xor
   26.20 +code_gen
   26.21 +  "0::nat" "1::nat"
   26.22  code_gen
   26.23    Pair fst snd Let split swap
   26.24  code_gen "0::int" "1::int"
    27.1 --- a/src/HOL/ex/mesontest2.ML	Tue Sep 26 13:34:15 2006 +0200
    27.2 +++ b/src/HOL/ex/mesontest2.ML	Tue Sep 26 13:34:16 2006 +0200
    27.3 @@ -985,11 +985,11 @@
    27.4    meson_tac 1);
    27.5  
    27.6  val HEN002_0_ax =
    27.7 -  "(\\<forall>X Y. mless_equal(X::'a,Y) --> equal(Divide(X::'a,Y),zero)) &       \
    27.8 -\  (\\<forall>X Y. equal(Divide(X::'a,Y),zero) --> mless_equal(X::'a,Y)) &       \
    27.9 +  "(\\<forall>X Y. mless_equal(X::'a,Y) --> equal(Divide(X::'a,Y),Zero)) &       \
   27.10 +\  (\\<forall>X Y. equal(Divide(X::'a,Y),Zero) --> mless_equal(X::'a,Y)) &       \
   27.11  \  (\\<forall>Y X. mless_equal(Divide(X::'a,Y),X)) & \
   27.12  \  (\\<forall>X Y Z. mless_equal(Divide(Divide(X::'a,Z),Divide(Y::'a,Z)),Divide(Divide(X::'a,Y),Z))) &       \
   27.13 -\  (\\<forall>X. mless_equal(zero::'a,X)) &  \
   27.14 +\  (\\<forall>X. mless_equal(Zero::'a,X)) &  \
   27.15  \  (\\<forall>X Y. mless_equal(X::'a,Y) & mless_equal(Y::'a,X) --> equal(X::'a,Y)) &  \
   27.16  \  (\\<forall>X. mless_equal(X::'a,identity))";
   27.17  
   27.18 @@ -1002,18 +1002,18 @@
   27.19  (*250258 inferences so far.  Searching to depth 16.  406.2 secs*)
   27.20  val HEN003_3 = prove_hard
   27.21   (EQU001_0_ax ^ "&" ^ HEN002_0_ax ^ "&" ^ HEN002_0_eq ^ " &     \
   27.22 -\  (~equal(Divide(a::'a,a),zero)) --> False",
   27.23 +\  (~equal(Divide(a::'a,a),Zero)) --> False",
   27.24    meson_tac 1);
   27.25  
   27.26  
   27.27  (*202177 inferences so far.  Searching to depth 14.  451 secs*)
   27.28  val HEN007_2 = prove_hard
   27.29   (EQU001_0_ax ^ " &  \
   27.30 -\  (\\<forall>X Y. mless_equal(X::'a,Y) --> quotient(X::'a,Y,zero)) &    \
   27.31 -\  (\\<forall>X Y. quotient(X::'a,Y,zero) --> mless_equal(X::'a,Y)) &    \
   27.32 +\  (\\<forall>X Y. mless_equal(X::'a,Y) --> quotient(X::'a,Y,Zero)) &    \
   27.33 +\  (\\<forall>X Y. quotient(X::'a,Y,Zero) --> mless_equal(X::'a,Y)) &    \
   27.34  \  (\\<forall>Y Z X. quotient(X::'a,Y,Z) --> mless_equal(Z::'a,X)) &     \
   27.35  \  (\\<forall>Y X V3 V2 V1 Z V4 V5. quotient(X::'a,Y,V1) & quotient(Y::'a,Z,V2) & quotient(X::'a,Z,V3) & quotient(V3::'a,V2,V4) & quotient(V1::'a,Z,V5) --> mless_equal(V4::'a,V5)) &    \
   27.36 -\  (\\<forall>X. mless_equal(zero::'a,X)) &  \
   27.37 +\  (\\<forall>X. mless_equal(Zero::'a,X)) &  \
   27.38  \  (\\<forall>X Y. mless_equal(X::'a,Y) & mless_equal(Y::'a,X) --> equal(X::'a,Y)) &  \
   27.39  \  (\\<forall>X. mless_equal(X::'a,identity)) &      \
   27.40  \  (\\<forall>X Y. quotient(X::'a,Y,Divide(X::'a,Y))) & \
   27.41 @@ -1025,10 +1025,10 @@
   27.42  \  (\\<forall>X Y Z. equal(X::'a,Y) & mless_equal(X::'a,Z) --> mless_equal(Y::'a,Z)) &        \
   27.43  \  (\\<forall>X Y W. equal(X::'a,Y) --> equal(Divide(X::'a,W),Divide(Y::'a,W))) &   \
   27.44  \  (\\<forall>X W Y. equal(X::'a,Y) --> equal(Divide(W::'a,X),Divide(W::'a,Y))) &   \
   27.45 -\  (\\<forall>X. quotient(X::'a,identity,zero)) &   \
   27.46 -\  (\\<forall>X. quotient(zero::'a,X,zero)) &       \
   27.47 -\  (\\<forall>X. quotient(X::'a,X,zero)) &  \
   27.48 -\  (\\<forall>X. quotient(X::'a,zero,X)) &  \
   27.49 +\  (\\<forall>X. quotient(X::'a,identity,Zero)) &   \
   27.50 +\  (\\<forall>X. quotient(Zero::'a,X,Zero)) &       \
   27.51 +\  (\\<forall>X. quotient(X::'a,X,Zero)) &  \
   27.52 +\  (\\<forall>X. quotient(X::'a,Zero,X)) &  \
   27.53  \  (\\<forall>Y X Z. mless_equal(X::'a,Y) & mless_equal(Y::'a,Z) --> mless_equal(X::'a,Z)) &   \
   27.54  \  (\\<forall>W1 X Z W2 Y. quotient(X::'a,Y,W1) & mless_equal(W1::'a,Z) & quotient(X::'a,Z,W2) --> mless_equal(W2::'a,Y)) &       \
   27.55  \  (mless_equal(x::'a,y)) &  \
   27.56 @@ -1040,10 +1040,10 @@
   27.57  (*60026 inferences so far.  Searching to depth 12.  42.2 secs*)
   27.58  val HEN008_4 = prove_hard
   27.59   (EQU001_0_ax ^ "&" ^ HEN002_0_ax ^ "&" ^ HEN002_0_eq ^ " &     \
   27.60 -\  (\\<forall>X. equal(Divide(X::'a,identity),zero)) &      \
   27.61 -\  (\\<forall>X. equal(Divide(zero::'a,X),zero)) &  \
   27.62 -\  (\\<forall>X. equal(Divide(X::'a,X),zero)) &     \
   27.63 -\  (equal(Divide(a::'a,zero),a)) &  \
   27.64 +\  (\\<forall>X. equal(Divide(X::'a,identity),Zero)) &      \
   27.65 +\  (\\<forall>X. equal(Divide(Zero::'a,X),Zero)) &  \
   27.66 +\  (\\<forall>X. equal(Divide(X::'a,X),Zero)) &     \
   27.67 +\  (equal(Divide(a::'a,Zero),a)) &  \
   27.68  \  (\\<forall>Y X Z. mless_equal(X::'a,Y) & mless_equal(Y::'a,Z) --> mless_equal(X::'a,Z)) &   \
   27.69  \  (\\<forall>X Z Y. mless_equal(Divide(X::'a,Y),Z) --> mless_equal(Divide(X::'a,Z),Y)) & \
   27.70  \  (\\<forall>Y Z X. mless_equal(X::'a,Y) --> mless_equal(Divide(Z::'a,Y),Divide(Z::'a,X))) & \
   27.71 @@ -1055,16 +1055,16 @@
   27.72  (*3160 inferences so far.  Searching to depth 11.  3.5 secs*)
   27.73  val HEN009_5 = prove
   27.74   (EQU001_0_ax ^ " &  \
   27.75 -\  (\\<forall>Y X. equal(Divide(Divide(X::'a,Y),X),zero)) & \
   27.76 -\  (\\<forall>X Y Z. equal(Divide(Divide(Divide(X::'a,Z),Divide(Y::'a,Z)),Divide(Divide(X::'a,Y),Z)),zero)) &       \
   27.77 -\  (\\<forall>X. equal(Divide(zero::'a,X),zero)) &  \
   27.78 -\  (\\<forall>X Y. equal(Divide(X::'a,Y),zero) & equal(Divide(Y::'a,X),zero) --> equal(X::'a,Y)) &  \
   27.79 -\  (\\<forall>X. equal(Divide(X::'a,identity),zero)) &      \
   27.80 +\  (\\<forall>Y X. equal(Divide(Divide(X::'a,Y),X),Zero)) & \
   27.81 +\  (\\<forall>X Y Z. equal(Divide(Divide(Divide(X::'a,Z),Divide(Y::'a,Z)),Divide(Divide(X::'a,Y),Z)),Zero)) &       \
   27.82 +\  (\\<forall>X. equal(Divide(Zero::'a,X),Zero)) &  \
   27.83 +\  (\\<forall>X Y. equal(Divide(X::'a,Y),Zero) & equal(Divide(Y::'a,X),Zero) --> equal(X::'a,Y)) &  \
   27.84 +\  (\\<forall>X. equal(Divide(X::'a,identity),Zero)) &      \
   27.85  \  (\\<forall>A B C. equal(A::'a,B) --> equal(Divide(A::'a,C),Divide(B::'a,C))) &   \
   27.86  \  (\\<forall>D F' E. equal(D::'a,E) --> equal(Divide(F'::'a,D),Divide(F'::'a,E))) &        \
   27.87 -\  (\\<forall>Y X Z. equal(Divide(X::'a,Y),zero) & equal(Divide(Y::'a,Z),zero) --> equal(Divide(X::'a,Z),zero)) &   \
   27.88 -\  (\\<forall>X Z Y. equal(Divide(Divide(X::'a,Y),Z),zero) --> equal(Divide(Divide(X::'a,Z),Y),zero)) & \
   27.89 -\  (\\<forall>Y Z X. equal(Divide(X::'a,Y),zero) --> equal(Divide(Divide(Z::'a,Y),Divide(Z::'a,X)),zero)) & \
   27.90 +\  (\\<forall>Y X Z. equal(Divide(X::'a,Y),Zero) & equal(Divide(Y::'a,Z),Zero) --> equal(Divide(X::'a,Z),Zero)) &   \
   27.91 +\  (\\<forall>X Z Y. equal(Divide(Divide(X::'a,Y),Z),Zero) --> equal(Divide(Divide(X::'a,Z),Y),Zero)) & \
   27.92 +\  (\\<forall>Y Z X. equal(Divide(X::'a,Y),Zero) --> equal(Divide(Divide(Z::'a,Y),Divide(Z::'a,X)),Zero)) & \
   27.93  \  (~equal(Divide(identity::'a,a),Divide(identity::'a,Divide(identity::'a,Divide(identity::'a,a))))) &  \
   27.94  \  (equal(Divide(identity::'a,a),b)) &      \
   27.95  \  (equal(Divide(identity::'a,b),c)) &      \
   27.96 @@ -1735,8 +1735,8 @@
   27.97  \  (mless_THAN(i::'a,n)) &   \
   27.98  \  (mless_THAN(a(j),a(k))) &     \
   27.99  \  (\\<forall>X. mless_THAN(X::'a,j) & mless_THAN(a(X),a(k)) --> mless_THAN(X::'a,i)) &    \
  27.100 -\  (\\<forall>X. mless_THAN(one::'a,i) & mless_THAN(a(X),a(predecessor(i))) --> mless_THAN(X::'a,i) | mless_THAN(n::'a,X)) &   \
  27.101 -\  (\\<forall>X. ~(mless_THAN(one::'a,X) & mless_THAN(X::'a,i) & mless_THAN(a(X),a(predecessor(X))))) &    \
  27.102 +\  (\\<forall>X. mless_THAN(One::'a,i) & mless_THAN(a(X),a(predecessor(i))) --> mless_THAN(X::'a,i) | mless_THAN(n::'a,X)) &   \
  27.103 +\  (\\<forall>X. ~(mless_THAN(One::'a,X) & mless_THAN(X::'a,i) & mless_THAN(a(X),a(predecessor(X))))) &    \
  27.104  \  (mless_THAN(j::'a,i)) --> False",
  27.105    meson_tac 1);
  27.106  
  27.107 @@ -1747,11 +1747,11 @@
  27.108  \  (~mless_THAN(k::'a,l)) &  \
  27.109  \  (~mless_THAN(k::'a,i)) &  \
  27.110  \  (mless_THAN(l::'a,n)) &   \
  27.111 -\  (mless_THAN(one::'a,l)) & \
  27.112 +\  (mless_THAN(One::'a,l)) & \
  27.113  \  (mless_THAN(a(k),a(predecessor(l)))) &        \
  27.114  \  (\\<forall>X. mless_THAN(X::'a,successor(n)) & mless_THAN(a(X),a(k)) --> mless_THAN(X::'a,l)) & \
  27.115 -\  (\\<forall>X. mless_THAN(one::'a,l) & mless_THAN(a(X),a(predecessor(l))) --> mless_THAN(X::'a,l) | mless_THAN(n::'a,X)) &   \
  27.116 -\  (\\<forall>X. ~(mless_THAN(one::'a,X) & mless_THAN(X::'a,l) & mless_THAN(a(X),a(predecessor(X))))) --> False",
  27.117 +\  (\\<forall>X. mless_THAN(One::'a,l) & mless_THAN(a(X),a(predecessor(l))) --> mless_THAN(X::'a,l) | mless_THAN(n::'a,X)) &   \
  27.118 +\  (\\<forall>X. ~(mless_THAN(One::'a,X) & mless_THAN(X::'a,l) & mless_THAN(a(X),a(predecessor(X))))) --> False",
  27.119    meson_tac 1);
  27.120  
  27.121  (*2343 inferences so far.  Searching to depth 8.  3.5 secs*)
  27.122 @@ -1760,11 +1760,11 @@
  27.123  \  (~mless_THAN(n::'a,m)) &  \
  27.124  \  (mless_THAN(i::'a,m)) &   \
  27.125  \  (mless_THAN(i::'a,n)) &   \
  27.126 -\  (~mless_THAN(i::'a,one)) &        \
  27.127 +\  (~mless_THAN(i::'a,One)) &        \
  27.128  \  (mless_THAN(a(i),a(m))) &     \
  27.129  \  (\\<forall>X. mless_THAN(X::'a,successor(n)) & mless_THAN(a(X),a(m)) --> mless_THAN(X::'a,i)) & \
  27.130 -\  (\\<forall>X. mless_THAN(one::'a,i) & mless_THAN(a(X),a(predecessor(i))) --> mless_THAN(X::'a,i) | mless_THAN(n::'a,X)) &   \
  27.131 -\  (\\<forall>X. ~(mless_THAN(one::'a,X) & mless_THAN(X::'a,i) & mless_THAN(a(X),a(predecessor(X))))) --> False",
  27.132 +\  (\\<forall>X. mless_THAN(One::'a,i) & mless_THAN(a(X),a(predecessor(i))) --> mless_THAN(X::'a,i) | mless_THAN(n::'a,X)) &   \
  27.133 +\  (\\<forall>X. ~(mless_THAN(One::'a,X) & mless_THAN(X::'a,i) & mless_THAN(a(X),a(predecessor(X))))) --> False",
  27.134    meson_tac 1);
  27.135  
  27.136  (*86 inferences so far.  Searching to depth 14.  0.1 secs*)
  27.137 @@ -2166,9 +2166,9 @@
  27.138  \  (\\<forall>M O_ N. equal(M::'a,N) --> equal(multiply(O_::'a,M),multiply(O_::'a,N))) &       \
  27.139  \  (\\<forall>P Q. equal(P::'a,Q) --> equal(successor(P),successor(Q))) &   \
  27.140  \  (\\<forall>R S'. equal(R::'a,S') & positive_integer(R) --> positive_integer(S')) &       \
  27.141 -\  (\\<forall>X. equal(multiply(one::'a,X),X)) &    \
  27.142 +\  (\\<forall>X. equal(multiply(One::'a,X),X)) &    \
  27.143  \  (\\<forall>V X. positive_integer(X) --> equal(multiply(successor(V),X),add(X::'a,multiply(V::'a,X)))) &      \
  27.144 -\  (positive_integer(one)) &    \
  27.145 +\  (positive_integer(One)) &    \
  27.146  \  (\\<forall>X. positive_integer(X) --> positive_integer(successor(X))) &      \
  27.147  \  (equal(negate(add(d::'a,e)),negate(e))) &        \
  27.148  \  (positive_integer(k)) &      \
  27.149 @@ -2212,22 +2212,22 @@
  27.150  
  27.151  (*6450 inferences so far.  Searching to depth 14.  4.2 secs*)
  27.152  val SET009_1 = prove
  27.153 - ("(\\<forall>Subset Element Superset. member(Element::'a,Subset) & subset(Subset::'a,Superset) --> member(Element::'a,Superset)) & \
  27.154 -\  (\\<forall>Superset Subset. subset(Subset::'a,Superset) | member(member_of_1_not_of_2(Subset::'a,Superset),Subset)) &       \
  27.155 -\  (\\<forall>Subset Superset. member(member_of_1_not_of_2(Subset::'a,Superset),Superset) --> subset(Subset::'a,Superset)) &    \
  27.156 -\  (\\<forall>Subset Superset. equal_sets(Subset::'a,Superset) --> subset(Subset::'a,Superset)) &       \
  27.157 -\  (\\<forall>Subset Superset. equal_sets(Superset::'a,Subset) --> subset(Subset::'a,Superset)) &       \
  27.158 -\  (\\<forall>Set2 Set1. subset(Set1::'a,Set2) & subset(Set2::'a,Set1) --> equal_sets(Set2::'a,Set1)) &     \
  27.159 + ("(\\<forall>Subset Element Superset. member(Element::'a,Subset) & ssubset(Subset::'a,Superset) --> member(Element::'a,Superset)) & \
  27.160 +\  (\\<forall>Superset Subset. ssubset(Subset::'a,Superset) | member(member_of_1_not_of_2(Subset::'a,Superset),Subset)) &       \
  27.161 +\  (\\<forall>Subset Superset. member(member_of_1_not_of_2(Subset::'a,Superset),Superset) --> ssubset(Subset::'a,Superset)) &    \
  27.162 +\  (\\<forall>Subset Superset. equal_sets(Subset::'a,Superset) --> ssubset(Subset::'a,Superset)) &       \
  27.163 +\  (\\<forall>Subset Superset. equal_sets(Superset::'a,Subset) --> ssubset(Subset::'a,Superset)) &       \
  27.164 +\  (\\<forall>Set2 Set1. ssubset(Set1::'a,Set2) & ssubset(Set2::'a,Set1) --> equal_sets(Set2::'a,Set1)) &     \
  27.165  \  (\\<forall>Set2 Difference Element Set1. difference(Set1::'a,Set2,Difference) & member(Element::'a,Difference) --> member(Element::'a,Set1)) &   \
  27.166  \  (\\<forall>Element A_set Set1 Set2. ~(member(Element::'a,Set1) & member(Element::'a,Set2) & difference(A_set::'a,Set1,Set2))) &  \
  27.167  \  (\\<forall>Set1 Difference Element Set2. member(Element::'a,Set1) & difference(Set1::'a,Set2,Difference) --> member(Element::'a,Difference) | member(Element::'a,Set2)) &   \
  27.168  \  (\\<forall>Set1 Set2 Difference. difference(Set1::'a,Set2,Difference) | member(k(Set1::'a,Set2,Difference),Set1) | member(k(Set1::'a,Set2,Difference),Difference)) &   \
  27.169  \  (\\<forall>Set1 Set2 Difference. member(k(Set1::'a,Set2,Difference),Set2) --> member(k(Set1::'a,Set2,Difference),Difference) | difference(Set1::'a,Set2,Difference)) &  \
  27.170  \  (\\<forall>Set1 Set2 Difference. member(k(Set1::'a,Set2,Difference),Difference) & member(k(Set1::'a,Set2,Difference),Set1) --> member(k(Set1::'a,Set2,Difference),Set2) | difference(Set1::'a,Set2,Difference)) &   \
  27.171 -\  (subset(d::'a,a)) &      \
  27.172 +\  (ssubset(d::'a,a)) &      \
  27.173  \  (difference(b::'a,a,bDa)) &      \
  27.174  \  (difference(b::'a,d,bDd)) &      \
  27.175 -\  (~subset(bDa::'a,bDd)) --> False",
  27.176 +\  (~ssubset(bDa::'a,bDd)) --> False",
  27.177    meson_tac 1);
  27.178  
  27.179  (*34726 inferences so far.  Searching to depth 6.  2420 secs: 40 mins! BIG*)
  27.180 @@ -2299,14 +2299,14 @@
  27.181  \  (\\<forall>Z X. member(Z::'a,sigma(X)) --> member(Z::'a,f16(Z::'a,X))) & \
  27.182  \  (\\<forall>X Z Y. member(Y::'a,X) & member(Z::'a,Y) --> member(Z::'a,sigma(X))) &        \
  27.183  \  (\\<forall>U. little_set(U) --> little_set(sigma(U))) &      \
  27.184 -\  (\\<forall>X U Y. subset(X::'a,Y) & member(U::'a,X) --> member(U::'a,Y)) &       \
  27.185 -\  (\\<forall>Y X. subset(X::'a,Y) | member(f17(X::'a,Y),X)) & \
  27.186 -\  (\\<forall>X Y. member(f17(X::'a,Y),Y) --> subset(X::'a,Y)) &        \
  27.187 -\  (\\<forall>X Y. proper_subset(X::'a,Y) --> subset(X::'a,Y)) &        \
  27.188 +\  (\\<forall>X U Y. ssubset(X::'a,Y) & member(U::'a,X) --> member(U::'a,Y)) &       \
  27.189 +\  (\\<forall>Y X. ssubset(X::'a,Y) | member(f17(X::'a,Y),X)) & \
  27.190 +\  (\\<forall>X Y. member(f17(X::'a,Y),Y) --> ssubset(X::'a,Y)) &        \
  27.191 +\  (\\<forall>X Y. proper_subset(X::'a,Y) --> ssubset(X::'a,Y)) &        \
  27.192  \  (\\<forall>X Y. ~(proper_subset(X::'a,Y) & equal(X::'a,Y))) &        \
  27.193 -\  (\\<forall>X Y. subset(X::'a,Y) --> proper_subset(X::'a,Y) | equal(X::'a,Y)) &  \
  27.194 -\  (\\<forall>Z X. member(Z::'a,powerset(X)) --> subset(Z::'a,X)) &     \
  27.195 -\  (\\<forall>Z X. little_set(Z) & subset(Z::'a,X) --> member(Z::'a,powerset(X))) &     \
  27.196 +\  (\\<forall>X Y. ssubset(X::'a,Y) --> proper_subset(X::'a,Y) | equal(X::'a,Y)) &  \
  27.197 +\  (\\<forall>Z X. member(Z::'a,powerset(X)) --> ssubset(Z::'a,X)) &     \
  27.198 +\  (\\<forall>Z X. little_set(Z) & ssubset(Z::'a,X) --> member(Z::'a,powerset(X))) &     \
  27.199  \  (\\<forall>U. little_set(U) --> little_set(powerset(U))) &   \
  27.200  \  (\\<forall>Z X. relation(Z) & member(X::'a,Z) --> ordered_pair_predicate(X)) &   \
  27.201  \  (\\<forall>Z. relation(Z) | member(f18(Z),Z)) &     \
  27.202 @@ -2354,8 +2354,8 @@
  27.203  \  (\\<forall>Xf X Y. equal(apply_to_two_arguments(Xf::'a,X,Y),apply(Xf::'a,ordered_pair(X::'a,Y)))) &      \
  27.204  \  (\\<forall>X Y Xf. maps(Xf::'a,X,Y) --> function(Xf)) &  \
  27.205  \  (\\<forall>Y Xf X. maps(Xf::'a,X,Y) --> equal(domain_of(Xf),X)) &        \
  27.206 -\  (\\<forall>X Xf Y. maps(Xf::'a,X,Y) --> subset(range_of(Xf),Y)) &        \
  27.207 -\  (\\<forall>X Xf Y. function(Xf) & equal(domain_of(Xf),X) & subset(range_of(Xf),Y) --> maps(Xf::'a,X,Y)) &        \
  27.208 +\  (\\<forall>X Xf Y. maps(Xf::'a,X,Y) --> ssubset(range_of(Xf),Y)) &        \
  27.209 +\  (\\<forall>X Xf Y. function(Xf) & equal(domain_of(Xf),X) & ssubset(range_of(Xf),Y) --> maps(Xf::'a,X,Y)) &        \
  27.210  \  (\\<forall>Xf Xs. closed(Xs::'a,Xf) --> little_set(Xs)) &        \
  27.211  \  (\\<forall>Xs Xf. closed(Xs::'a,Xf) --> little_set(Xf)) &        \
  27.212  \  (\\<forall>Xf Xs. closed(Xs::'a,Xf) --> maps(Xf::'a,cross_product(Xs::'a,Xs),Xs)) &      \
  27.213 @@ -2494,8 +2494,8 @@
  27.214  \  (\\<forall>P15 R15 Q15. equal(P15::'a,Q15) & proper_subset(R15::'a,P15) --> proper_subset(R15::'a,Q15)) &        \
  27.215  \  (\\<forall>S15 T15. equal(S15::'a,T15) & relation(S15) --> relation(T15)) &      \
  27.216  \  (\\<forall>U15 V15. equal(U15::'a,V15) & single_valued_set(U15) --> single_valued_set(V15)) &    \
  27.217 -\  (\\<forall>W15 X15 Y15. equal(W15::'a,X15) & subset(W15::'a,Y15) --> subset(X15::'a,Y15)) &      \
  27.218 -\  (\\<forall>Z15 B16 A16. equal(Z15::'a,A16) & subset(B16::'a,Z15) --> subset(B16::'a,A16)) &      \
  27.219 +\  (\\<forall>W15 X15 Y15. equal(W15::'a,X15) & ssubset(W15::'a,Y15) --> ssubset(X15::'a,Y15)) &      \
  27.220 +\  (\\<forall>Z15 B16 A16. equal(Z15::'a,A16) & ssubset(B16::'a,Z15) --> ssubset(B16::'a,A16)) &      \
  27.221  \  (~little_set(ordered_pair(a::'a,b))) --> False",
  27.222    meson_tac 1);
  27.223  
    28.1 --- a/src/HOL/hologic.ML	Tue Sep 26 13:34:15 2006 +0200
    28.2 +++ b/src/HOL/hologic.ML	Tue Sep 26 13:34:16 2006 +0200
    28.3 @@ -261,9 +261,9 @@
    28.4  
    28.5  val natT = Type ("nat", []);
    28.6  
    28.7 -val zero = Const ("0", natT);
    28.8 +val zero = Const ("HOL.zero", natT);
    28.9  
   28.10 -fun is_zero (Const ("0", _)) = true
   28.11 +fun is_zero (Const ("HOL.zero", _)) = true
   28.12    | is_zero _ = false;
   28.13  
   28.14  fun mk_Suc t = Const ("Suc", natT --> natT) $ t;
   28.15 @@ -274,7 +274,7 @@
   28.16  fun mk_nat 0 = zero
   28.17    | mk_nat n = mk_Suc (mk_nat (n - 1));
   28.18  
   28.19 -fun dest_nat (Const ("0", _)) = 0
   28.20 +fun dest_nat (Const ("HOL.zero", _)) = 0
   28.21    | dest_nat (Const ("Suc", _) $ t) = dest_nat t + 1
   28.22    | dest_nat t = raise TERM ("dest_nat", [t]);
   28.23  
   28.24 @@ -319,21 +319,17 @@
   28.25  fun mk_binum n =
   28.26    let
   28.27      fun mk_bit n = if n = 0 then B0_const else B1_const;
   28.28 -
   28.29      fun bin_of n =
   28.30        if n = 0 then pls_const
   28.31        else if n = ~1 then min_const
   28.32        else
   28.33          let
   28.34 -          (*val (q,r) = IntInf.divMod (n, 2): doesn't work in SML 110.0.7,
   28.35 -            but in newer versions!  FIXME: put this back after new SML released!*)
   28.36 -          val q = IntInf.div (n, 2);
   28.37 -          val r = IntInf.mod (n, 2);
   28.38 +          val (q,r) = IntInf.divMod (n, 2);
   28.39          in bit_const $ bin_of q $ mk_bit r end;
   28.40    in bin_of n end;
   28.41  
   28.42 -fun mk_int 0 = Const ("0", intT)
   28.43 -  | mk_int 1 = Const ("1", intT)
   28.44 +fun mk_int 0 = Const ("HOL.zero", intT)
   28.45 +  | mk_int 1 = Const ("HOL.one", intT)
   28.46    | mk_int i = number_of_const intT $ mk_binum i;
   28.47  
   28.48  
    29.1 --- a/src/HOLCF/Pcpo.thy	Tue Sep 26 13:34:15 2006 +0200
    29.2 +++ b/src/HOLCF/Pcpo.thy	Tue Sep 26 13:34:16 2006 +0200
    29.3 @@ -200,8 +200,8 @@
    29.4    fun reorient_proc sg _ (_ $ t $ u) =
    29.5      case u of
    29.6          Const("Pcpo.UU",_) => NONE
    29.7 -      | Const("0", _) => NONE
    29.8 -      | Const("1", _) => NONE
    29.9 +      | Const("HOL.zero", _) => NONE
   29.10 +      | Const("HOL.one", _) => NONE
   29.11        | Const("Numeral.number_of", _) $ _ => NONE
   29.12        | _ => SOME meta_UU_reorient;
   29.13  in
    30.1 --- a/src/Provers/Arith/abel_cancel.ML	Tue Sep 26 13:34:15 2006 +0200
    30.2 +++ b/src/Provers/Arith/abel_cancel.ML	Tue Sep 26 13:34:16 2006 +0200
    30.3 @@ -28,7 +28,7 @@
    30.4  
    30.5  (* FIXME dependent on abstract syntax *)
    30.6  
    30.7 -fun zero t = Const ("0", t);
    30.8 +fun zero t = Const ("HOL.zero", t);
    30.9  fun minus t = Const ("HOL.uminus", t --> t);
   30.10  
   30.11  fun add_terms pos (Const ("HOL.plus", _) $ x $ y, ts) =