renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
authorhaftmann
Fri Mar 10 15:33:48 2006 +0100 (2006-03-10)
changeset 1923377ca20b0ed77
parent 19232 1f5b5dc3f48a
child 19234 054332e39e0a
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
NEWS
src/HOL/Algebra/CRing.thy
src/HOL/Algebra/abstract/order.ML
src/HOL/Auth/Guard/Extensions.thy
src/HOL/Auth/Guard/Guard.thy
src/HOL/Auth/Guard/GuardK.thy
src/HOL/Complex/CLim.thy
src/HOL/HOL.thy
src/HOL/Import/Generate-HOL/GenHOL4Base.thy
src/HOL/Import/Generate-HOL/GenHOL4Real.thy
src/HOL/Import/Generate-HOLLight/GenHOLLight.thy
src/HOL/Import/HOL/arithmetic.imp
src/HOL/Import/HOL/real.imp
src/HOL/Import/HOL/realax.imp
src/HOL/Import/HOLLight/HOLLight.thy
src/HOL/Import/HOLLight/hollight.imp
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/Library/ExecutableRat.thy
src/HOL/Library/ExecutableSet.thy
src/HOL/Library/comm_ring.ML
src/HOL/OrderedGroup.ML
src/HOL/OrderedGroup.thy
src/HOL/Real/Float.ML
src/HOL/Set.thy
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/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_prop.ML
src/HOL/Tools/refute.ML
src/HOL/Tools/res_clause.ML
src/HOL/arith_data.ML
src/HOL/ex/SVC_Oracle.ML
src/HOL/ex/mesontest2.ML
src/HOL/ex/svc_funcs.ML
src/Provers/Arith/abel_cancel.ML
src/Provers/Arith/cancel_div_mod.ML
src/Pure/Tools/class_package.ML
src/Pure/library.ML
     1.1 --- a/NEWS	Fri Mar 10 12:28:38 2006 +0100
     1.2 +++ b/NEWS	Fri Mar 10 15:33:48 2006 +0100
     1.3 @@ -340,6 +340,33 @@
     1.4  25 like -->); output depends on the "iff" print_mode, the default is
     1.5  "A = B" (with priority 50).
     1.6  
     1.7 +* Renamed some (legacy-named) constants in HOL.thy:
     1.8 +    op +   ~> HOL.plus
     1.9 +    op -   ~> HOL.minus
    1.10 +    uminus ~> HOL.uminus
    1.11 +    op *   ~> HOL.times
    1.12 +
    1.13 +Adaptions may be required in the following cases:
    1.14 +
    1.15 +a) User-defined constants using any of the names "plus", "minus", or "times"
    1.16 +The standard syntax translations for "+", "-" and "*" may go wrong.
    1.17 +INCOMPATIBILITY: use more specific names.
    1.18 +
    1.19 +b) Variables named "plus", "minus", or "times"
    1.20 +INCOMPATIBILITY: use more specific names.
    1.21 +
    1.22 +c) Commutative equations theorems (e. g. "a + b = b + a")
    1.23 +Since the changing of names also changes the order of terms, commutative rewrites
    1.24 +perhaps will be applied when not applied before or the other way round.
    1.25 +Experience shows that thiis is rarely the case (only two adaptions in the whole
    1.26 +Isabelle distribution).
    1.27 +INCOMPATIBILITY: rewrite proof; sometimes already an exchange of a distributive
    1.28 +law may suffice.
    1.29 +
    1.30 +d) ML code directly refering to constant names
    1.31 +This in general only affects hand-written proof tactics, simprocs and so on.
    1.32 +INCOMPATIBILITY: grep your sourcecode and replace names.
    1.33 +
    1.34  * "LEAST x:A. P" expands to "LEAST x. x:A & P" (input only).
    1.35  
    1.36  * In the context of the assumption "~(s = t)" the Simplifier rewrites
     2.1 --- a/src/HOL/Algebra/CRing.thy	Fri Mar 10 12:28:38 2006 +0100
     2.2 +++ b/src/HOL/Algebra/CRing.thy	Fri Mar 10 15:33:48 2006 +0100
     2.3 @@ -20,7 +20,7 @@
     2.4    a_inv :: "[('a, 'm) ring_scheme, 'a ] => 'a" ("\<ominus>\<index> _" [81] 80)
     2.5    "a_inv R == m_inv (| carrier = carrier R, mult = add R, one = zero R |)"
     2.6  
     2.7 -  minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" (infixl "\<ominus>\<index>" 65)
     2.8 +  a_minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" (infixl "\<ominus>\<index>" 65)
     2.9    "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y == x \<oplus> (\<ominus> y)"
    2.10  
    2.11  locale abelian_monoid = struct G +
    2.12 @@ -95,7 +95,7 @@
    2.13  
    2.14  lemma (in abelian_group) minus_closed [intro, simp]:
    2.15    "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<ominus> y \<in> carrier G"
    2.16 -  by (simp add: minus_def)
    2.17 +  by (simp add: a_minus_def)
    2.18  
    2.19  lemma (in abelian_group) a_l_cancel [simp]:
    2.20    "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
    2.21 @@ -431,7 +431,7 @@
    2.22  
    2.23  lemma (in ring) minus_eq:
    2.24    "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y = x \<oplus> \<ominus> y"
    2.25 -  by (simp only: minus_def)
    2.26 +  by (simp only: a_minus_def)
    2.27  
    2.28  lemmas (in ring) ring_simprules =
    2.29    a_closed zero_closed a_inv_closed minus_closed m_closed one_closed
     3.1 --- a/src/HOL/Algebra/abstract/order.ML	Fri Mar 10 12:28:38 2006 +0100
     3.2 +++ b/src/HOL/Algebra/abstract/order.ML	Fri Mar 10 15:33:48 2006 +0100
     3.3 @@ -8,7 +8,7 @@
     3.4  (*** Term order for commutative rings ***)
     3.5  
     3.6  fun ring_ord a =
     3.7 -  find_index_eq a ["0", "op +", "uminus", "op -", "1", "op *"];
     3.8 +  find_index (fn a' => a = a') ["0", "HOL.plus", "HOL.uminus", "HOL.minus", "1", "HOL.times"];
     3.9  
    3.10  fun termless_ring (a, b) = (Term.term_lpo ring_ord (a, b) = LESS);
    3.11  
    3.12 @@ -18,9 +18,9 @@
    3.13  val a = Free ("a", intT);
    3.14  val b = Free ("b", intT);
    3.15  val c = Free ("c", intT);
    3.16 -val plus = Const ("op +", [intT, intT]--->intT);
    3.17 -val mult = Const ("op *", [intT, intT]--->intT);
    3.18 -val uminus = Const ("uminus", intT-->intT);
    3.19 +val plus = Const ("HOL.plus", [intT, intT]--->intT);
    3.20 +val mult = Const ("HOL.times", [intT, intT]--->intT);
    3.21 +val uminus = Const ("HOL.uminus", intT-->intT);
    3.22  val one = Const ("1", intT);
    3.23  val f = Const("f", intT-->intT);
    3.24  
     4.1 --- a/src/HOL/Auth/Guard/Extensions.thy	Fri Mar 10 12:28:38 2006 +0100
     4.2 +++ b/src/HOL/Auth/Guard/Extensions.thy	Fri Mar 10 15:33:48 2006 +0100
     4.3 @@ -27,15 +27,15 @@
     4.4  
     4.5  subsection{*Extensions to Theory @{text List}*}
     4.6  
     4.7 -subsubsection{*"minus l x" erase the first element of "l" equal to "x"*}
     4.8 +subsubsection{*"remove l x" erase the first element of "l" equal to "x"*}
     4.9  
    4.10 -consts minus :: "'a list => 'a => 'a list"
    4.11 +consts remove :: "'a list => 'a => 'a list"
    4.12  
    4.13  primrec
    4.14 -"minus [] y = []"
    4.15 -"minus (x#xs) y = (if x=y then xs else x # minus xs y)"
    4.16 +"remove [] y = []"
    4.17 +"remove (x#xs) y = (if x=y then xs else x # remove xs y)"
    4.18  
    4.19 -lemma set_minus: "set (minus l x) <= set l"
    4.20 +lemma set_remove: "set (remove l x) <= set l"
    4.21  by (induct l, auto)
    4.22  
    4.23  subsection{*Extensions to Theory @{text Message}*}
     5.1 --- a/src/HOL/Auth/Guard/Guard.thy	Fri Mar 10 12:28:38 2006 +0100
     5.2 +++ b/src/HOL/Auth/Guard/Guard.thy	Fri Mar 10 15:33:48 2006 +0100
     5.3 @@ -208,7 +208,7 @@
     5.4  
     5.5  lemmas mem_cnb_minus_substI = mem_cnb_minus [THEN ssubst]
     5.6  
     5.7 -lemma cnb_minus [simp]: "x mem l ==> cnb (minus l x) = cnb l - crypt_nb x"
     5.8 +lemma cnb_minus [simp]: "x mem l ==> cnb (remove l x) = cnb l - crypt_nb x"
     5.9  apply (induct l, auto)
    5.10  by (erule_tac l1=l and x1=x in mem_cnb_minus_substI, simp)
    5.11  
    5.12 @@ -242,7 +242,7 @@
    5.13  subsection{*list corresponding to "decrypt"*}
    5.14  
    5.15  constdefs decrypt' :: "msg list => key => msg => msg list"
    5.16 -"decrypt' l K Y == Y # minus l (Crypt K Y)"
    5.17 +"decrypt' l K Y == Y # remove l (Crypt K Y)"
    5.18  
    5.19  declare decrypt'_def [simp]
    5.20  
    5.21 @@ -278,7 +278,7 @@
    5.22  apply (subgoal_tac "Crypt K Y:parts (set l)")
    5.23  apply (drule parts_cnb, rotate_tac -1, simp)
    5.24  apply (clarify, drule_tac X="Key Ka" and H="insert Y (set l')" in analz_sub)
    5.25 -apply (rule insert_mono, rule set_minus)
    5.26 +apply (rule insert_mono, rule set_remove)
    5.27  apply (simp add: analz_insertD, blast)
    5.28  (* Crypt K Y:parts (set l) *)
    5.29  apply (blast dest: kparts_parts)
    5.30 @@ -288,7 +288,7 @@
    5.31  apply (rule_tac K=K in guard_Crypt, simp add: Guard_def, simp)
    5.32  apply (drule_tac t="set l'" in sym, simp)
    5.33  apply (rule Guard_kparts, simp, simp)
    5.34 -apply (rule_tac B="set l'" in subset_trans, rule set_minus, blast)
    5.35 +apply (rule_tac B="set l'" in subset_trans, rule set_remove, blast)
    5.36  by (rule kparts_set)
    5.37  
    5.38  lemma Guard_invKey_finite: "[| Nonce n:analz G; Guard n Ks G; finite G |]
     6.1 --- a/src/HOL/Auth/Guard/GuardK.thy	Fri Mar 10 12:28:38 2006 +0100
     6.2 +++ b/src/HOL/Auth/Guard/GuardK.thy	Fri Mar 10 15:33:48 2006 +0100
     6.3 @@ -204,7 +204,7 @@
     6.4  
     6.5  lemmas mem_cnb_minus_substI = mem_cnb_minus [THEN ssubst]
     6.6  
     6.7 -lemma cnb_minus [simp]: "x mem l ==> cnb (minus l x) = cnb l - crypt_nb x"
     6.8 +lemma cnb_minus [simp]: "x mem l ==> cnb (remove l x) = cnb l - crypt_nb x"
     6.9  apply (induct l, auto)
    6.10  by (erule_tac l1=l and x1=x in mem_cnb_minus_substI, simp)
    6.11  
    6.12 @@ -238,7 +238,7 @@
    6.13  subsection{*list corresponding to "decrypt"*}
    6.14  
    6.15  constdefs decrypt' :: "msg list => key => msg => msg list"
    6.16 -"decrypt' l K Y == Y # minus l (Crypt K Y)"
    6.17 +"decrypt' l K Y == Y # remove l (Crypt K Y)"
    6.18  
    6.19  declare decrypt'_def [simp]
    6.20  
    6.21 @@ -274,7 +274,7 @@
    6.22  apply (subgoal_tac "Crypt K Y:parts (set l)")
    6.23  apply (drule parts_cnb, rotate_tac -1, simp)
    6.24  apply (clarify, drule_tac X="Key Ka" and H="insert Y (set l')" in analz_sub)
    6.25 -apply (rule insert_mono, rule set_minus)
    6.26 +apply (rule insert_mono, rule set_remove)
    6.27  apply (simp add: analz_insertD, blast)
    6.28  (* Crypt K Y:parts (set l) *)
    6.29  apply (blast dest: kparts_parts)
    6.30 @@ -284,7 +284,7 @@
    6.31  apply (rule_tac K=K in guardK_Crypt, simp add: GuardK_def, simp)
    6.32  apply (drule_tac t="set l'" in sym, simp)
    6.33  apply (rule GuardK_kparts, simp, simp)
    6.34 -apply (rule_tac B="set l'" in subset_trans, rule set_minus, blast)
    6.35 +apply (rule_tac B="set l'" in subset_trans, rule set_remove, blast)
    6.36  by (rule kparts_set)
    6.37  
    6.38  lemma GuardK_invKey_finite: "[| Key n:analz G; GuardK n Ks G; finite G |]
     7.1 --- a/src/HOL/Complex/CLim.thy	Fri Mar 10 12:28:38 2006 +0100
     7.2 +++ b/src/HOL/Complex/CLim.thy	Fri Mar 10 15:33:48 2006 +0100
     7.3 @@ -976,7 +976,7 @@
     7.4  apply (simp add: diff_minus)
     7.5  apply (drule_tac f = g in CDERIV_inverse_fun)
     7.6  apply (drule_tac [2] CDERIV_mult, assumption+)
     7.7 -apply (simp add: divide_inverse right_distrib power_inverse minus_mult_left 
     7.8 +apply (simp add: divide_inverse left_distrib power_inverse minus_mult_left 
     7.9                   mult_ac 
    7.10              del: minus_mult_right [symmetric] minus_mult_left [symmetric]
    7.11                   complexpow_Suc)
     8.1 --- a/src/HOL/HOL.thy	Fri Mar 10 12:28:38 2006 +0100
     8.2 +++ b/src/HOL/HOL.thy	Fri Mar 10 15:33:48 2006 +0100
     8.3 @@ -198,15 +198,20 @@
     8.4  axclass times < type
     8.5  axclass inverse < type
     8.6  
     8.7 +consts
     8.8 +  plus             :: "['a::plus, 'a]  => 'a"       (infixl "+" 65)
     8.9 +  uminus           :: "'a::minus => 'a"             ("- _" [81] 80)
    8.10 +  minus            :: "['a::minus, 'a] => 'a"       (infixl "-" 65)
    8.11 +  abs              :: "'a::minus => 'a"
    8.12 +  times            :: "['a::times, 'a] => 'a"       (infixl "*" 70)
    8.13 +  inverse          :: "'a::inverse => 'a"
    8.14 +  divide           :: "['a::inverse, 'a] => 'a"     (infixl "'/" 70)
    8.15 +
    8.16  global
    8.17  
    8.18  consts
    8.19    "0"           :: "'a::zero"                       ("0")
    8.20    "1"           :: "'a::one"                        ("1")
    8.21 -  "+"           :: "['a::plus, 'a]  => 'a"          (infixl 65)
    8.22 -  -             :: "['a::minus, 'a] => 'a"          (infixl 65)
    8.23 -  uminus        :: "['a::minus] => 'a"              ("- _" [81] 80)
    8.24 -  *             :: "['a::times, 'a] => 'a"          (infixl 70)
    8.25  
    8.26  syntax
    8.27    "_index1"  :: index    ("\<^sub>1")
    8.28 @@ -223,12 +228,6 @@
    8.29    in [tr' "0", tr' "1"] end;
    8.30  *} -- {* show types that are presumably too general *}
    8.31  
    8.32 -
    8.33 -consts
    8.34 -  abs           :: "'a::minus => 'a"
    8.35 -  inverse       :: "'a::inverse => 'a"
    8.36 -  divide        :: "['a::inverse, 'a] => 'a"        (infixl "'/" 70)
    8.37 -
    8.38  syntax (xsymbols)
    8.39    abs :: "'a::minus => 'a"    ("\<bar>_\<bar>")
    8.40  syntax (HTML output)
    8.41 @@ -1408,11 +1407,7 @@
    8.42    "op -->" "HOL.op_implies"
    8.43    "op &" "HOL.op_and"
    8.44    "op |" "HOL.op_or"
    8.45 -  "op +" "HOL.op_add"
    8.46 -  "op -" "HOL.op_minus"
    8.47 -  "op *" "HOL.op_times"
    8.48    Not "HOL.not"
    8.49 -  uminus "HOL.uminus"
    8.50    arbitrary "HOL.arbitrary"
    8.51  
    8.52  code_syntax_const
     9.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Fri Mar 10 12:28:38 2006 +0100
     9.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Fri Mar 10 15:33:48 2006 +0100
     9.3 @@ -182,9 +182,9 @@
     9.4    ">="         > HOL4Compat.nat_ge
     9.5    FUNPOW       > HOL4Compat.FUNPOW
     9.6    "<="         > "op <="          :: "[nat,nat]=>bool"
     9.7 -  "+"          > "op +"           :: "[nat,nat]=>nat"
     9.8 -  "*"          > "op *"           :: "[nat,nat]=>nat"
     9.9 -  "-"          > "op -"           :: "[nat,nat]=>nat"
    9.10 +  "+"          > "HOL.plus"       :: "[nat,nat]=>nat"
    9.11 +  "*"          > "HOL.times"      :: "[nat,nat]=>nat"
    9.12 +  "-"          > "HOL.minus"      :: "[nat,nat]=>nat"
    9.13    MIN          > Orderings.min    :: "[nat,nat]=>nat"
    9.14    MAX          > Orderings.max    :: "[nat,nat]=>nat"
    9.15    DIV          > "Divides.op div" :: "[nat,nat]=>nat"
    10.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Real.thy	Fri Mar 10 12:28:38 2006 +0100
    10.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Real.thy	Fri Mar 10 15:33:48 2006 +0100
    10.3 @@ -21,8 +21,8 @@
    10.4    real_1   > 1           :: real
    10.5    real_neg > uminus      :: "real => real"
    10.6    inv      > HOL.inverse :: "real => real"
    10.7 -  real_add > "op +"      :: "[real,real] => real"
    10.8 -  real_mul > "op *"      :: "[real,real] => real"
    10.9 +  real_add > HOL.plus    :: "[real,real] => real"
   10.10 +  real_mul > HOL.times   :: "[real,real] => real"
   10.11    real_lt  > "op <"      :: "[real,real] => bool";
   10.12  
   10.13  ignore_thms
   10.14 @@ -52,7 +52,7 @@
   10.15    real_gt     > HOL4Compat.real_gt
   10.16    real_ge     > HOL4Compat.real_ge
   10.17    real_lte    > "op <="      :: "[real,real] => bool"
   10.18 -  real_sub    > "op -"       :: "[real,real] => real"
   10.19 +  real_sub    > HOL.minus    :: "[real,real] => real"
   10.20    "/"         > HOL.divide   :: "[real,real] => real"
   10.21    pow         > Nat.power    :: "[real,nat] => real"
   10.22    abs         > HOL.abs      :: "real => real"
    11.1 --- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Fri Mar 10 12:28:38 2006 +0100
    11.2 +++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Fri Mar 10 15:33:48 2006 +0100
    11.3 @@ -76,9 +76,9 @@
    11.4    SUC > Suc
    11.5    PRE > HOLLightCompat.Pred
    11.6    NUMERAL > HOL4Compat.NUMERAL
    11.7 -  "+" > "op +" :: "nat \<Rightarrow> nat \<Rightarrow> nat" 
    11.8 -  "*" > "op *" :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    11.9 -  "-" > "op -" :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   11.10 +  "+" > HOL.plus :: "nat \<Rightarrow> nat \<Rightarrow> nat" 
   11.11 +  "*" > HOL.times :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   11.12 +  "-" > HOL.minus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   11.13    BIT0 > HOLLightCompat.NUMERAL_BIT0
   11.14    BIT1 > HOL4Compat.NUMERAL_BIT1
   11.15    INL > Sum_Type.Inl
    12.1 --- a/src/HOL/Import/HOL/arithmetic.imp	Fri Mar 10 12:28:38 2006 +0100
    12.2 +++ b/src/HOL/Import/HOL/arithmetic.imp	Fri Mar 10 15:33:48 2006 +0100
    12.3 @@ -24,9 +24,9 @@
    12.4    ">=" > "HOL4Compat.nat_ge"
    12.5    ">" > "HOL4Compat.nat_gt"
    12.6    "<=" > "op <=" :: "nat => nat => bool"
    12.7 -  "-" > "op -" :: "nat => nat => nat"
    12.8 -  "+" > "op +" :: "nat => nat => nat"
    12.9 -  "*" > "op *" :: "nat => nat => nat"
   12.10 +  "-" > "HOL.minus" :: "nat => nat => nat"
   12.11 +  "+" > "HOL.plus" :: "nat => nat => nat"
   12.12 +  "*" > "HOL.times" :: "nat => nat => nat"
   12.13  
   12.14  thm_maps
   12.15    "num_case_def" > "HOL4Compat.num_case_def"
    13.1 --- a/src/HOL/Import/HOL/real.imp	Fri Mar 10 12:28:38 2006 +0100
    13.2 +++ b/src/HOL/Import/HOL/real.imp	Fri Mar 10 15:33:48 2006 +0100
    13.3 @@ -10,7 +10,7 @@
    13.4  const_maps
    13.5    "sup" > "HOL4Real.real.sup"
    13.6    "sum" > "HOL4Real.real.sum"
    13.7 -  "real_sub" > "op -" :: "real => real => real"
    13.8 +  "real_sub" > "HOL.minus" :: "real => real => real"
    13.9    "real_of_num" > "RealDef.real" :: "nat => real"
   13.10    "real_lte" > "op <=" :: "real => real => bool"
   13.11    "real_gt" > "HOL4Compat.real_gt"
    14.1 --- a/src/HOL/Import/HOL/realax.imp	Fri Mar 10 12:28:38 2006 +0100
    14.2 +++ b/src/HOL/Import/HOL/realax.imp	Fri Mar 10 15:33:48 2006 +0100
    14.3 @@ -27,10 +27,10 @@
    14.4    "treal_add" > "HOL4Real.realax.treal_add"
    14.5    "treal_1" > "HOL4Real.realax.treal_1"
    14.6    "treal_0" > "HOL4Real.realax.treal_0"
    14.7 -  "real_neg" > "uminus" :: "real => real"
    14.8 -  "real_mul" > "op *" :: "real => real => real"
    14.9 +  "real_neg" > "HOL.uminus" :: "real => real"
   14.10 +  "real_mul" > "HOL.times" :: "real => real => real"
   14.11    "real_lt" > "op <" :: "real => real => bool"
   14.12 -  "real_add" > "op +" :: "real => real => real"
   14.13 +  "real_add" > "HOL.plus" :: "real => real => real"
   14.14    "real_1" > "1" :: "real"
   14.15    "real_0" > "0" :: "real"
   14.16    "inv" > "HOL.inverse" :: "real => real"
    15.1 --- a/src/HOL/Import/HOLLight/HOLLight.thy	Fri Mar 10 12:28:38 2006 +0100
    15.2 +++ b/src/HOL/Import/HOLLight/HOLLight.thy	Fri Mar 10 15:33:48 2006 +0100
    15.3 @@ -1119,37 +1119,37 @@
    15.4     (%x::nat.
    15.5         (All::(nat => bool) => bool)
    15.6          (%xa::nat.
    15.7 -            (op =::nat => nat => bool) ((op +::nat => nat => nat) x xa)
    15.8 -             ((op +::nat => nat => nat) x xa))))
    15.9 +            (op =::nat => nat => bool) ((HOL.plus::nat => nat => nat) x xa)
   15.10 +             ((HOL.plus::nat => nat => nat) x xa))))
   15.11   ((op &::bool => bool => bool)
   15.12 -   ((op =::nat => nat => bool) ((op +::nat => nat => nat) (0::nat) (0::nat))
   15.13 +   ((op =::nat => nat => bool) ((HOL.plus::nat => nat => nat) (0::nat) (0::nat))
   15.14       (0::nat))
   15.15     ((op &::bool => bool => bool)
   15.16       ((All::(nat => bool) => bool)
   15.17         (%x::nat.
   15.18             (op =::nat => nat => bool)
   15.19 -            ((op +::nat => nat => nat) (0::nat)
   15.20 +            ((HOL.plus::nat => nat => nat) (0::nat)
   15.21                ((NUMERAL_BIT0::nat => nat) x))
   15.22              ((NUMERAL_BIT0::nat => nat) x)))
   15.23       ((op &::bool => bool => bool)
   15.24         ((All::(nat => bool) => bool)
   15.25           (%x::nat.
   15.26               (op =::nat => nat => bool)
   15.27 -              ((op +::nat => nat => nat) (0::nat)
   15.28 +              ((HOL.plus::nat => nat => nat) (0::nat)
   15.29                  ((NUMERAL_BIT1::nat => nat) x))
   15.30                ((NUMERAL_BIT1::nat => nat) x)))
   15.31         ((op &::bool => bool => bool)
   15.32           ((All::(nat => bool) => bool)
   15.33             (%x::nat.
   15.34                 (op =::nat => nat => bool)
   15.35 -                ((op +::nat => nat => nat) ((NUMERAL_BIT0::nat => nat) x)
   15.36 +                ((HOL.plus::nat => nat => nat) ((NUMERAL_BIT0::nat => nat) x)
   15.37                    (0::nat))
   15.38                  ((NUMERAL_BIT0::nat => nat) x)))
   15.39           ((op &::bool => bool => bool)
   15.40             ((All::(nat => bool) => bool)
   15.41               (%x::nat.
   15.42                   (op =::nat => nat => bool)
   15.43 -                  ((op +::nat => nat => nat) ((NUMERAL_BIT1::nat => nat) x)
   15.44 +                  ((HOL.plus::nat => nat => nat) ((NUMERAL_BIT1::nat => nat) x)
   15.45                      (0::nat))
   15.46                    ((NUMERAL_BIT1::nat => nat) x)))
   15.47             ((op &::bool => bool => bool)
   15.48 @@ -1158,44 +1158,44 @@
   15.49                     (All::(nat => bool) => bool)
   15.50                      (%xa::nat.
   15.51                          (op =::nat => nat => bool)
   15.52 -                         ((op +::nat => nat => nat)
   15.53 +                         ((HOL.plus::nat => nat => nat)
   15.54                             ((NUMERAL_BIT0::nat => nat) x)
   15.55                             ((NUMERAL_BIT0::nat => nat) xa))
   15.56                           ((NUMERAL_BIT0::nat => nat)
   15.57 -                           ((op +::nat => nat => nat) x xa)))))
   15.58 +                           ((HOL.plus::nat => nat => nat) x xa)))))
   15.59               ((op &::bool => bool => bool)
   15.60                 ((All::(nat => bool) => bool)
   15.61                   (%x::nat.
   15.62                       (All::(nat => bool) => bool)
   15.63                        (%xa::nat.
   15.64                            (op =::nat => nat => bool)
   15.65 -                           ((op +::nat => nat => nat)
   15.66 +                           ((HOL.plus::nat => nat => nat)
   15.67                               ((NUMERAL_BIT0::nat => nat) x)
   15.68                               ((NUMERAL_BIT1::nat => nat) xa))
   15.69                             ((NUMERAL_BIT1::nat => nat)
   15.70 -                             ((op +::nat => nat => nat) x xa)))))
   15.71 +                             ((HOL.plus::nat => nat => nat) x xa)))))
   15.72                 ((op &::bool => bool => bool)
   15.73                   ((All::(nat => bool) => bool)
   15.74                     (%x::nat.
   15.75                         (All::(nat => bool) => bool)
   15.76                          (%xa::nat.
   15.77                              (op =::nat => nat => bool)
   15.78 -                             ((op +::nat => nat => nat)
   15.79 +                             ((HOL.plus::nat => nat => nat)
   15.80                                 ((NUMERAL_BIT1::nat => nat) x)
   15.81                                 ((NUMERAL_BIT0::nat => nat) xa))
   15.82                               ((NUMERAL_BIT1::nat => nat)
   15.83 -                               ((op +::nat => nat => nat) x xa)))))
   15.84 +                               ((HOL.plus::nat => nat => nat) x xa)))))
   15.85                   ((All::(nat => bool) => bool)
   15.86                     (%x::nat.
   15.87                         (All::(nat => bool) => bool)
   15.88                          (%xa::nat.
   15.89                              (op =::nat => nat => bool)
   15.90 -                             ((op +::nat => nat => nat)
   15.91 +                             ((HOL.plus::nat => nat => nat)
   15.92                                 ((NUMERAL_BIT1::nat => nat) x)
   15.93                                 ((NUMERAL_BIT1::nat => nat) xa))
   15.94                               ((NUMERAL_BIT0::nat => nat)
   15.95                                 ((Suc::nat => nat)
   15.96 -                                 ((op +::nat => nat => nat) x
   15.97 +                                 ((HOL.plus::nat => nat => nat) x
   15.98                                     xa))))))))))))))"
   15.99    by (import hollight ARITH_ADD)
  15.100  
  15.101 @@ -1258,7 +1258,7 @@
  15.102                             ((op *::nat => nat => nat)
  15.103                               ((NUMERAL_BIT0::nat => nat) x)
  15.104                               ((NUMERAL_BIT1::nat => nat) xa))
  15.105 -                           ((op +::nat => nat => nat)
  15.106 +                           ((HOL.plus::nat => nat => nat)
  15.107                               ((NUMERAL_BIT0::nat => nat) x)
  15.108                               ((NUMERAL_BIT0::nat => nat)
  15.109                                 ((NUMERAL_BIT0::nat => nat)
  15.110 @@ -1272,7 +1272,7 @@
  15.111                               ((op *::nat => nat => nat)
  15.112                                 ((NUMERAL_BIT1::nat => nat) x)
  15.113                                 ((NUMERAL_BIT0::nat => nat) xa))
  15.114 -                             ((op +::nat => nat => nat)
  15.115 +                             ((HOL.plus::nat => nat => nat)
  15.116                                 ((NUMERAL_BIT0::nat => nat) xa)
  15.117                                 ((NUMERAL_BIT0::nat => nat)
  15.118                                   ((NUMERAL_BIT0::nat => nat)
  15.119 @@ -1285,9 +1285,9 @@
  15.120                               ((op *::nat => nat => nat)
  15.121                                 ((NUMERAL_BIT1::nat => nat) x)
  15.122                                 ((NUMERAL_BIT1::nat => nat) xa))
  15.123 -                             ((op +::nat => nat => nat)
  15.124 +                             ((HOL.plus::nat => nat => nat)
  15.125                                 ((NUMERAL_BIT1::nat => nat) x)
  15.126 -                               ((op +::nat => nat => nat)
  15.127 +                               ((HOL.plus::nat => nat => nat)
  15.128                                   ((NUMERAL_BIT0::nat => nat) xa)
  15.129                                   ((NUMERAL_BIT0::nat => nat)
  15.130                                     ((NUMERAL_BIT0::nat => nat)
  15.131 @@ -7462,7 +7462,7 @@
  15.132        (%i::nat.
  15.133            ($::('A::type, ('M::type, 'N::type) finite_sum) cart
  15.134                => nat => 'A::type)
  15.135 -           u ((op +::nat => nat => nat) i
  15.136 +           u ((HOL.plus::nat => nat => nat) i
  15.137                 ((dimindex::('M::type => bool) => nat)
  15.138                   (hollight.UNIV::'M::type => bool)))))"
  15.139  
  15.140 @@ -7478,14 +7478,14 @@
  15.141        (%i::nat.
  15.142            ($::('A::type, ('M::type, 'N::type) finite_sum) cart
  15.143                => nat => 'A::type)
  15.144 -           u ((op +::nat => nat => nat) i
  15.145 +           u ((HOL.plus::nat => nat => nat) i
  15.146                 ((dimindex::('M::type => bool) => nat)
  15.147                   (hollight.UNIV::'M::type => bool)))))"
  15.148    by (import hollight DEF_sndcart)
  15.149  
  15.150  lemma DIMINDEX_HAS_SIZE_FINITE_SUM: "(HAS_SIZE::(('M::type, 'N::type) finite_sum => bool) => nat => bool)
  15.151   (hollight.UNIV::('M::type, 'N::type) finite_sum => bool)
  15.152 - ((op +::nat => nat => nat)
  15.153 + ((HOL.plus::nat => nat => nat)
  15.154     ((dimindex::('M::type => bool) => nat) (hollight.UNIV::'M::type => bool))
  15.155     ((dimindex::('N::type => bool) => nat)
  15.156       (hollight.UNIV::'N::type => bool)))"
  15.157 @@ -7494,7 +7494,7 @@
  15.158  lemma DIMINDEX_FINITE_SUM: "(op =::nat => nat => bool)
  15.159   ((dimindex::(('M::type, 'N::type) finite_sum => bool) => nat)
  15.160     (hollight.UNIV::('M::type, 'N::type) finite_sum => bool))
  15.161 - ((op +::nat => nat => nat)
  15.162 + ((HOL.plus::nat => nat => nat)
  15.163     ((dimindex::('M::type => bool) => nat) (hollight.UNIV::'M::type => bool))
  15.164     ((dimindex::('N::type => bool) => nat)
  15.165       (hollight.UNIV::'N::type => bool)))"
  15.166 @@ -8025,7 +8025,7 @@
  15.167   (nsum::('q_51017::type => bool) => ('q_51017::type => nat) => nat)
  15.168   ((iterate::(nat => nat => nat)
  15.169              => ('q_51017::type => bool) => ('q_51017::type => nat) => nat)
  15.170 -   (op +::nat => nat => nat))"
  15.171 +   (HOL.plus::nat => nat => nat))"
  15.172  
  15.173  lemma DEF_nsum: "(op =::(('q_51017::type => bool) => ('q_51017::type => nat) => nat)
  15.174         => (('q_51017::type => bool) => ('q_51017::type => nat) => nat)
  15.175 @@ -8033,17 +8033,17 @@
  15.176   (nsum::('q_51017::type => bool) => ('q_51017::type => nat) => nat)
  15.177   ((iterate::(nat => nat => nat)
  15.178              => ('q_51017::type => bool) => ('q_51017::type => nat) => nat)
  15.179 -   (op +::nat => nat => nat))"
  15.180 +   (HOL.plus::nat => nat => nat))"
  15.181    by (import hollight DEF_nsum)
  15.182  
  15.183  lemma NEUTRAL_ADD: "(op =::nat => nat => bool)
  15.184 - ((neutral::(nat => nat => nat) => nat) (op +::nat => nat => nat)) (0::nat)"
  15.185 + ((neutral::(nat => nat => nat) => nat) (HOL.plus::nat => nat => nat)) (0::nat)"
  15.186    by (import hollight NEUTRAL_ADD)
  15.187  
  15.188  lemma NEUTRAL_MUL: "neutral op * = NUMERAL_BIT1 0"
  15.189    by (import hollight NEUTRAL_MUL)
  15.190  
  15.191 -lemma MONOIDAL_ADD: "(monoidal::(nat => nat => nat) => bool) (op +::nat => nat => nat)"
  15.192 +lemma MONOIDAL_ADD: "(monoidal::(nat => nat => nat) => bool) (HOL.plus::nat => nat => nat)"
  15.193    by (import hollight MONOIDAL_ADD)
  15.194  
  15.195  lemma MONOIDAL_MUL: "(monoidal::(nat => nat => nat) => bool) (op *::nat => nat => nat)"
  15.196 @@ -8068,7 +8068,7 @@
  15.197    by (import hollight NSUM_DIFF)
  15.198  
  15.199  lemma NSUM_SUPPORT: "ALL (x::'q_51214::type => nat) xa::'q_51214::type => bool.
  15.200 -   FINITE (support op + x xa) --> nsum (support op + x xa) x = nsum xa x"
  15.201 +   FINITE (support HOL.plus x xa) --> nsum (support HOL.plus x xa) x = nsum xa x"
  15.202    by (import hollight NSUM_SUPPORT)
  15.203  
  15.204  lemma NSUM_ADD: "ALL (f::'q_51260::type => nat) (g::'q_51260::type => nat)
    16.1 --- a/src/HOL/Import/HOLLight/hollight.imp	Fri Mar 10 12:28:38 2006 +0100
    16.2 +++ b/src/HOL/Import/HOLLight/hollight.imp	Fri Mar 10 15:33:48 2006 +0100
    16.3 @@ -238,10 +238,10 @@
    16.4    "<=" > "HOLLight.hollight.<="
    16.5    "<" > "HOLLight.hollight.<"
    16.6    "/\\" > "op &"
    16.7 -  "-" > "op -" :: "nat => nat => nat"
    16.8 +  "-" > "HOL.minus" :: "nat => nat => nat"
    16.9    "," > "Pair"
   16.10 -  "+" > "op +" :: "nat => nat => nat"
   16.11 -  "*" > "op *" :: "nat => nat => nat"
   16.12 +  "+" > "HOL.plus" :: "nat => nat => nat"
   16.13 +  "*" > "HOL.times" :: "nat => nat => nat"
   16.14    "$" > "HOLLight.hollight.$"
   16.15    "!" > "All"
   16.16  
    17.1 --- a/src/HOL/Integ/IntDef.thy	Fri Mar 10 12:28:38 2006 +0100
    17.2 +++ b/src/HOL/Integ/IntDef.thy	Fri Mar 10 15:33:48 2006 +0100
    17.3 @@ -886,14 +886,14 @@
    17.4    by (simp add: nat_aux_def)
    17.5  
    17.6  consts_code
    17.7 -  "0" :: "int"                  ("0")
    17.8 -  "1" :: "int"                  ("1")
    17.9 -  "uminus" :: "int => int"      ("~")
   17.10 -  "op +" :: "int => int => int" ("(_ +/ _)")
   17.11 -  "op *" :: "int => int => int" ("(_ */ _)")
   17.12 -  "op <" :: "int => int => bool" ("(_ </ _)")
   17.13 -  "op <=" :: "int => int => bool" ("(_ <=/ _)")
   17.14 -  "neg"                         ("(_ < 0)")
   17.15 +  "0" :: "int"                       ("0")
   17.16 +  "1" :: "int"                       ("1")
   17.17 +  "HOL.uminus" :: "int => int"       ("~")
   17.18 +  "HOL.plus" :: "int => int => int"  ("(_ +/ _)")
   17.19 +  "HOL.times" :: "int => int => int" ("(_ */ _)")
   17.20 +  "op <" :: "int => int => bool"     ("(_ </ _)")
   17.21 +  "op <=" :: "int => int => bool"    ("(_ <=/ _)")
   17.22 +  "neg"                              ("(_ < 0)")
   17.23  
   17.24  code_syntax_tyco int
   17.25    ml (target_atom "IntInf.int")
    18.1 --- a/src/HOL/Integ/cooper_dec.ML	Fri Mar 10 12:28:38 2006 +0100
    18.2 +++ b/src/HOL/Integ/cooper_dec.ML	Fri Mar 10 15:33:48 2006 +0100
    18.3 @@ -116,8 +116,8 @@
    18.4   
    18.5  fun linear_cmul n tm =  if n = 0 then zero else let fun times n k = n*k in  
    18.6    ( case tm of  
    18.7 -     (Const("op +",T)  $  (Const ("op *",T1 ) $c1 $  x1) $ rest) => 
    18.8 -       Const("op +",T) $ ((Const("op *",T1) $ (numeral1 (times n) c1) $ x1)) $ (linear_cmul n rest) 
    18.9 +     (Const("HOL.plus",T)  $  (Const ("HOL.times",T1 ) $c1 $  x1) $ rest) => 
   18.10 +       Const("HOL.plus",T) $ ((Const("HOL.times",T1) $ (numeral1 (times n) c1) $ x1)) $ (linear_cmul n rest) 
   18.11      |_ =>  numeral1 (times n) tm) 
   18.12      end ; 
   18.13   
   18.14 @@ -139,23 +139,23 @@
   18.15  fun linear_add vars tm1 tm2 = 
   18.16    let fun addwith x y = x + y in
   18.17   (case (tm1,tm2) of 
   18.18 -	((Const ("op +",T1) $ ( Const("op *",T2) $ c1 $  x1) $ rest1),(Const 
   18.19 -	("op +",T3)$( Const("op *",T4) $ c2 $  x2) $ rest2)) => 
   18.20 +	((Const ("HOL.plus",T1) $ ( Const("HOL.times",T2) $ c1 $  x1) $ rest1),(Const 
   18.21 +	("HOL.plus",T3)$( Const("HOL.times",T4) $ c2 $  x2) $ rest2)) => 
   18.22           if x1 = x2 then 
   18.23                let val c = (numeral2 (addwith) c1 c2) 
   18.24  	      in 
   18.25                if c = zero then (linear_add vars rest1  rest2)  
   18.26 -	      else (Const("op +",T1) $ (Const("op *",T2) $ c $ x1) $ (linear_add vars  rest1 rest2)) 
   18.27 +	      else (Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c $ x1) $ (linear_add vars  rest1 rest2)) 
   18.28                end 
   18.29  	   else 
   18.30 -		if earlierv vars x1 x2 then (Const("op +",T1) $  
   18.31 -		(Const("op *",T2)$ c1 $ x1) $ (linear_add vars rest1 tm2)) 
   18.32 -    	       else (Const("op +",T1) $ (Const("op *",T2) $ c2 $ x2) $ (linear_add vars tm1 rest2)) 
   18.33 -   	|((Const("op +",T1) $ (Const("op *",T2) $ c1 $ x1) $ rest1) ,_) => 
   18.34 -    	  (Const("op +",T1)$ (Const("op *",T2) $ c1 $ x1) $ (linear_add vars 
   18.35 +		if earlierv vars x1 x2 then (Const("HOL.plus",T1) $  
   18.36 +		(Const("HOL.times",T2)$ c1 $ x1) $ (linear_add vars rest1 tm2)) 
   18.37 +    	       else (Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c2 $ x2) $ (linear_add vars tm1 rest2)) 
   18.38 +   	|((Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c1 $ x1) $ rest1) ,_) => 
   18.39 +    	  (Const("HOL.plus",T1)$ (Const("HOL.times",T2) $ c1 $ x1) $ (linear_add vars 
   18.40  	  rest1 tm2)) 
   18.41 -   	|(_, (Const("op +",T1) $(Const("op *",T2) $ c2 $ x2) $ rest2)) => 
   18.42 -      	  (Const("op +",T1) $ (Const("op *",T2) $ c2 $ x2) $ (linear_add vars tm1 
   18.43 +   	|(_, (Const("HOL.plus",T1) $(Const("HOL.times",T2) $ c2 $ x2) $ rest2)) => 
   18.44 +      	  (Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c2 $ x2) $ (linear_add vars tm1 
   18.45  	  rest2)) 
   18.46     	| (_,_) => numeral2 (addwith) tm1 tm2) 
   18.47  	 
   18.48 @@ -180,13 +180,13 @@
   18.49   Free(x,T)*) 
   18.50    
   18.51  fun lint vars tm = if is_numeral tm then tm else case tm of 
   18.52 -   (Free (x,T)) =>  (HOLogic.mk_binop "op +" ((HOLogic.mk_binop "op *" ((mk_numeral 1),Free (x,T))), zero)) 
   18.53 -  |(Bound i) =>  (Const("op +",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ 
   18.54 -  (Const("op *",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ (mk_numeral 1) $ (Bound i)) $ zero) 
   18.55 -  |(Const("uminus",_) $ t ) => (linear_neg (lint vars t)) 
   18.56 -  |(Const("op +",_) $ s $ t) => (linear_add vars (lint vars s) (lint vars t)) 
   18.57 -  |(Const("op -",_) $ s $ t) => (linear_sub vars (lint vars s) (lint vars t)) 
   18.58 -  |(Const ("op *",_) $ s $ t) => 
   18.59 +   (Free (x,T)) =>  (HOLogic.mk_binop "HOL.plus" ((HOLogic.mk_binop "HOL.times" ((mk_numeral 1),Free (x,T))), zero)) 
   18.60 +  |(Bound i) =>  (Const("HOL.plus",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ 
   18.61 +  (Const("HOL.times",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ (mk_numeral 1) $ (Bound i)) $ zero) 
   18.62 +  |(Const("HOL.uminus",_) $ t ) => (linear_neg (lint vars t)) 
   18.63 +  |(Const("HOL.plus",_) $ s $ t) => (linear_add vars (lint vars s) (lint vars t)) 
   18.64 +  |(Const("HOL.minus",_) $ s $ t) => (linear_sub vars (lint vars s) (lint vars t)) 
   18.65 +  |(Const ("HOL.times",_) $ s $ t) => 
   18.66          let val s' = lint vars s  
   18.67              val t' = lint vars t  
   18.68          in 
   18.69 @@ -212,14 +212,14 @@
   18.70        end 
   18.71      else (warning "Nonlinear term --- Non numeral leftside at dvd"
   18.72        ;raise COOPER)
   18.73 -  |linform vars  (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ s $ t ) = (mkatom vars "op =" (Const ("op -",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s) ) 
   18.74 -  |linform vars  (Const("op <",_)$ s $t ) = (mkatom vars "op <" (Const ("op -",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s))
   18.75 -  |linform vars  (Const("op >",_) $ s $ t ) = (mkatom vars "op <" (Const ("op -",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ s $ t)) 
   18.76 +  |linform vars  (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ s $ t ) = (mkatom vars "op =" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s) ) 
   18.77 +  |linform vars  (Const("op <",_)$ s $t ) = (mkatom vars "op <" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s))
   18.78 +  |linform vars  (Const("op >",_) $ s $ t ) = (mkatom vars "op <" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ s $ t)) 
   18.79    |linform vars  (Const("op <=",_)$ s $ t ) = 
   18.80 -        (mkatom vars "op <" (Const ("op -",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ (Const("op +",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $t $(mk_numeral 1)) $ s)) 
   18.81 +        (mkatom vars "op <" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $t $(mk_numeral 1)) $ s)) 
   18.82    |linform vars  (Const("op >=",_)$ s $ t ) = 
   18.83 -        (mkatom vars "op <" (Const ("op -",HOLogic.intT --> HOLogic.intT --> 
   18.84 -	HOLogic.intT) $ (Const("op +",HOLogic.intT --> HOLogic.intT --> 
   18.85 +        (mkatom vars "op <" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> 
   18.86 +	HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT --> 
   18.87  	HOLogic.intT) $s $(mk_numeral 1)) $ t)) 
   18.88   
   18.89     |linform vars  fm =  fm; 
   18.90 @@ -246,7 +246,7 @@
   18.91  fun lcm_num a b = (abs a*b) div (gcd (abs a) (abs b)); 
   18.92   
   18.93  fun formlcm x fm = case fm of 
   18.94 -    (Const (p,_)$ _ $(Const ("op +", _)$(Const ("op *",_)$ c $ y ) $z ) ) =>  if 
   18.95 +    (Const (p,_)$ _ $(Const ("HOL.plus", _)$(Const ("HOL.times",_)$ c $ y ) $z ) ) =>  if 
   18.96      (is_arith_rel fm) andalso (x = y) then  (abs(dest_numeral c)) else 1 
   18.97    | ( Const ("Not", _) $p) => formlcm x p 
   18.98    | ( Const ("op &",_) $ p $ q) => lcm_num (formlcm x p) (formlcm x q) 
   18.99 @@ -259,13 +259,13 @@
  18.100   
  18.101  fun adjustcoeff x l fm = 
  18.102       case fm of  
  18.103 -      (Const(p,_) $d $( Const ("op +", _)$(Const ("op *",_) $ 
  18.104 +      (Const(p,_) $d $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $ 
  18.105        c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then  
  18.106          let val m = l div (dest_numeral c) 
  18.107              val n = (if p = "op <" then abs(m) else m) 
  18.108 -            val xtm = HOLogic.mk_binop "op *" ((mk_numeral (m div n)), x) 
  18.109 +            val xtm = HOLogic.mk_binop "HOL.times" ((mk_numeral (m div n)), x) 
  18.110  	in
  18.111 -        (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "op +" ( xtm ,( linear_cmul n z) )))) 
  18.112 +        (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) )))) 
  18.113  	end 
  18.114  	else fm 
  18.115    |( Const ("Not", _) $ p) => HOLogic.Not $ (adjustcoeff x l p) 
  18.116 @@ -282,8 +282,8 @@
  18.117        val fm' = adjustcoeff x l fm in
  18.118        if l = 1 then fm' 
  18.119  	 else 
  18.120 -     let val xp = (HOLogic.mk_binop "op +"  
  18.121 -     		((HOLogic.mk_binop "op *" ((mk_numeral 1), x )), zero))
  18.122 +     let val xp = (HOLogic.mk_binop "HOL.plus"  
  18.123 +     		((HOLogic.mk_binop "HOL.times" ((mk_numeral 1), x )), zero))
  18.124  	in 
  18.125        HOLogic.conj $(HOLogic.mk_binrel "Divides.op dvd" ((mk_numeral l) , xp )) $ (adjustcoeff x l fm) 
  18.126        end 
  18.127 @@ -294,12 +294,12 @@
  18.128  (*
  18.129  fun adjustcoeffeq x l fm = 
  18.130      case fm of  
  18.131 -      (Const(p,_) $d $( Const ("op +", _)$(Const ("op *",_) $ 
  18.132 +      (Const(p,_) $d $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $ 
  18.133        c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then  
  18.134          let val m = l div (dest_numeral c) 
  18.135              val n = (if p = "op <" then abs(m) else m)  
  18.136 -            val xtm = (HOLogic.mk_binop "op *" ((mk_numeral ((m div n)*l) ), x))
  18.137 -            in (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "op +" ( xtm ,( linear_cmul n z) )))) 
  18.138 +            val xtm = (HOLogic.mk_binop "HOL.times" ((mk_numeral ((m div n)*l) ), x))
  18.139 +            in (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) )))) 
  18.140  	    end 
  18.141  	else fm 
  18.142    |( Const ("Not", _) $ p) => HOLogic.Not $ (adjustcoeffeq x l p) 
  18.143 @@ -315,11 +315,11 @@
  18.144  (* ------------------------------------------------------------------------- *) 
  18.145   
  18.146  fun minusinf x fm = case fm of  
  18.147 -    (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) => 
  18.148 +    (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) => 
  18.149    	 if (is_arith_rel fm) andalso (x=y) andalso (c2 = one) andalso (c1 =zero) then HOLogic.false_const  
  18.150  	 				 else fm 
  18.151   
  18.152 -  |(Const("op <",_) $ c $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z 
  18.153 +  |(Const("op <",_) $ c $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z 
  18.154    )) => if (x = y) 
  18.155  	then if (pm1 = one) andalso (c = zero) then HOLogic.false_const 
  18.156  	     else if (dest_numeral pm1 = ~1) andalso (c = zero) then HOLogic.true_const 
  18.157 @@ -336,11 +336,11 @@
  18.158  (* ------------------------------------------------------------------------- *)
  18.159  
  18.160  fun plusinf x fm = case fm of
  18.161 -    (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
  18.162 +    (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
  18.163    	 if (is_arith_rel fm) andalso (x=y) andalso (c2 = one) andalso (c1 =zero) then HOLogic.false_const
  18.164  	 				 else fm
  18.165  
  18.166 -  |(Const("op <",_) $ c $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z
  18.167 +  |(Const("op <",_) $ c $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z
  18.168    )) => if (x = y) 
  18.169  	then if (pm1 = one) andalso (c = zero) then HOLogic.true_const 
  18.170  	     else if (dest_numeral pm1 = ~1) andalso (c = zero) then HOLogic.false_const
  18.171 @@ -356,7 +356,7 @@
  18.172  (* The LCM of all the divisors that involve x.                               *) 
  18.173  (* ------------------------------------------------------------------------- *) 
  18.174   
  18.175 -fun divlcm x (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z ) ) =  
  18.176 +fun divlcm x (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z ) ) =  
  18.177          if x = y then abs(dest_numeral d) else 1 
  18.178    |divlcm x ( Const ("Not", _) $ p) = divlcm x p 
  18.179    |divlcm x ( Const ("op &",_) $ p $ q) = lcm_num (divlcm x p) (divlcm x q) 
  18.180 @@ -370,15 +370,15 @@
  18.181  fun bset x fm = case fm of 
  18.182     (Const ("Not", _) $ p) => if (is_arith_rel p) then  
  18.183            (case p of  
  18.184 -	      (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $c2 $y) $a ) )  
  18.185 +	      (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $c2 $y) $a ) )  
  18.186  	             => if (is_arith_rel p) andalso (x=	y) andalso (c2 = one) andalso (c1 = zero)  
  18.187  	                then [linear_neg a] 
  18.188  			else  bset x p 
  18.189     	  |_ =>[]) 
  18.190  			 
  18.191  			else bset x p 
  18.192 -  |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +",_) $ (Const ("op *",_) $c2 $ x) $ a)) =>  if (c1 =zero) andalso (c2 = one) then [linear_neg(linear_add [] a (mk_numeral 1))]  else [] 
  18.193 -  |(Const ("op <",_) $ c1$ (Const ("op +",_) $(Const ("op *",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg a] else [] 
  18.194 +  |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) =>  if (c1 =zero) andalso (c2 = one) then [linear_neg(linear_add [] a (mk_numeral 1))]  else [] 
  18.195 +  |(Const ("op <",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg a] else [] 
  18.196    |(Const ("op &",_) $ p $ q) => (bset x p) union (bset x q) 
  18.197    |(Const ("op |",_) $ p $ q) => (bset x p) union (bset x q) 
  18.198    |_ => []; 
  18.199 @@ -390,15 +390,15 @@
  18.200  fun aset x fm = case fm of
  18.201     (Const ("Not", _) $ p) => if (is_arith_rel p) then
  18.202            (case p of
  18.203 -	      (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $c2 $y) $a ) )
  18.204 +	      (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $c2 $y) $a ) )
  18.205  	             => if (x=	y) andalso (c2 = one) andalso (c1 = zero)
  18.206  	                then [linear_neg a]
  18.207  			else  []
  18.208     	  |_ =>[])
  18.209  
  18.210  			else aset x p
  18.211 -  |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +",_) $ (Const ("op *",_) $c2 $ x) $ a)) =>  if (c1 =zero) andalso (c2 = one) then [linear_sub [] (mk_numeral 1) a]  else []
  18.212 -  |(Const ("op <",_) $ c1$ (Const ("op +",_) $(Const ("op *",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = (mk_numeral (~1))) then [a] else []
  18.213 +  |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) =>  if (c1 =zero) andalso (c2 = one) then [linear_sub [] (mk_numeral 1) a]  else []
  18.214 +  |(Const ("op <",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = (mk_numeral (~1))) then [a] else []
  18.215    |(Const ("op &",_) $ p $ q) => (aset x p) union (aset x q)
  18.216    |(Const ("op |",_) $ p $ q) => (aset x p) union (aset x q)
  18.217    |_ => [];
  18.218 @@ -409,7 +409,7 @@
  18.219  (* ------------------------------------------------------------------------- *) 
  18.220   
  18.221  fun linrep vars x t fm = case fm of  
  18.222 -   ((Const(p,_)$ d $ (Const("op +",_)$(Const("op *",_)$ c $ y) $ z))) => 
  18.223 +   ((Const(p,_)$ d $ (Const("HOL.plus",_)$(Const("HOL.times",_)$ c $ y) $ z))) => 
  18.224        if (x = y) andalso (is_arith_rel fm)  
  18.225        then  
  18.226          let val ct = linear_cmul (dest_numeral c) t  
  18.227 @@ -435,8 +435,8 @@
  18.228     val dn = dest_numeral d
  18.229     fun coeffs_of x = case x of 
  18.230       Const(p,_) $ tl $ tr => 
  18.231 -       if p = "op +" then (coeffs_of tl) union (coeffs_of tr)
  18.232 -          else if p = "op *" 
  18.233 +       if p = "HOL.plus" then (coeffs_of tl) union (coeffs_of tr)
  18.234 +          else if p = "HOL.times" 
  18.235  	        then if (is_numeral tr) 
  18.236  		 then [(dest_numeral tr) * (dest_numeral tl)] 
  18.237  		 else [dest_numeral tl]
    19.1 --- a/src/HOL/Integ/cooper_proof.ML	Fri Mar 10 12:28:38 2006 +0100
    19.2 +++ b/src/HOL/Integ/cooper_proof.ML	Fri Mar 10 15:33:48 2006 +0100
    19.3 @@ -165,11 +165,11 @@
    19.4  (* ------------------------------------------------------------------------- *)
    19.5  
    19.6  fun norm_zero_one fm = case fm of
    19.7 -  (Const ("op *",_) $ c $ t) => 
    19.8 +  (Const ("HOL.times",_) $ c $ t) => 
    19.9      if c = one then (norm_zero_one t)
   19.10      else if (dest_numeral c = ~1) 
   19.11 -         then (Const("uminus",HOLogic.intT --> HOLogic.intT) $ (norm_zero_one t))
   19.12 -         else (HOLogic.mk_binop "op *" (norm_zero_one c,norm_zero_one t))
   19.13 +         then (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $ (norm_zero_one t))
   19.14 +         else (HOLogic.mk_binop "HOL.times" (norm_zero_one c,norm_zero_one t))
   19.15    |(node $ rest) => ((norm_zero_one node)$(norm_zero_one rest))
   19.16    |(Abs(x,T,p)) => (Abs(x,T,(norm_zero_one p)))
   19.17    |_ => fm;
   19.18 @@ -255,13 +255,13 @@
   19.19  (*==================================================*)
   19.20  
   19.21  fun decomp_adjustcoeffeq sg x l fm = case fm of
   19.22 -    (Const("Not",_)$(Const("op <",_) $(Const("0",_)) $(rt as (Const ("op +", _)$(Const ("op *",_) $    c $ y ) $z )))) => 
   19.23 +    (Const("Not",_)$(Const("op <",_) $(Const("0",_)) $(rt as (Const ("HOL.plus", _)$(Const ("HOL.times",_) $    c $ y ) $z )))) => 
   19.24       let  
   19.25          val m = l div (dest_numeral c) 
   19.26          val n = if (x = y) then abs (m) else 1
   19.27 -        val xtm = (HOLogic.mk_binop "op *" ((mk_numeral ((m div n)*l) ), x)) 
   19.28 +        val xtm = (HOLogic.mk_binop "HOL.times" ((mk_numeral ((m div n)*l) ), x)) 
   19.29          val rs = if (x = y) 
   19.30 -                 then (HOLogic.mk_binrel "op <" (zero,linear_sub [] (mk_numeral n) (HOLogic.mk_binop "op +" ( xtm ,( linear_cmul n z) )))) 
   19.31 +                 then (HOLogic.mk_binrel "op <" (zero,linear_sub [] (mk_numeral n) (HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) )))) 
   19.32                   else HOLogic.mk_binrel "op <" (zero,linear_sub [] one rt )
   19.33          val ck = cterm_of sg (mk_numeral n)
   19.34          val cc = cterm_of sg c
   19.35 @@ -273,14 +273,14 @@
   19.36          in ([], fn [] => [th1,(prove_elementar sg "sa" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
   19.37          end
   19.38  
   19.39 -  |(Const(p,_) $a $( Const ("op +", _)$(Const ("op *",_) $ 
   19.40 +  |(Const(p,_) $a $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $ 
   19.41        c $ y ) $t )) => 
   19.42     if (is_arith_rel fm) andalso (x = y) 
   19.43     then  
   19.44          let val m = l div (dest_numeral c) 
   19.45             val k = (if p = "op <" then abs(m) else m)  
   19.46 -           val xtm = (HOLogic.mk_binop "op *" ((mk_numeral ((m div k)*l) ), x))
   19.47 -           val rs = (HOLogic.mk_binrel p ((linear_cmul k a),(HOLogic.mk_binop "op +" ( xtm ,( linear_cmul k t) )))) 
   19.48 +           val xtm = (HOLogic.mk_binop "HOL.times" ((mk_numeral ((m div k)*l) ), x))
   19.49 +           val rs = (HOLogic.mk_binrel p ((linear_cmul k a),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul k t) )))) 
   19.50  
   19.51             val ck = cterm_of sg (mk_numeral k)
   19.52             val cc = cterm_of sg c
   19.53 @@ -335,28 +335,28 @@
   19.54     val cfalse = cterm_of sg HOLogic.false_const
   19.55     val fm = norm_zero_one fm1
   19.56    in  case fm1 of 
   19.57 -      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
   19.58 +      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) => 
   19.59           if (x=y) andalso (c1= zero) andalso (c2= one) then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_minf))
   19.60             else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
   19.61  
   19.62 -      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
   19.63 +      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
   19.64    	   if (is_arith_rel fm) andalso (x=y) andalso (c1= zero) andalso (c2= one) 
   19.65  	   then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_minf))
   19.66  	 	 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf)) 
   19.67  
   19.68 -      |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
   19.69 +      |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
   19.70             if (y=x) andalso (c1 = zero) then 
   19.71              if (pm1 = one) then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_minf)) else
   19.72  	     (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_minf))
   19.73  	    else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
   19.74    
   19.75 -      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
   19.76 +      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
   19.77           if y=x then  let val cz = cterm_of sg (norm_zero_one z)
   19.78  			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
   19.79  	 	      in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_minf)))
   19.80  		      end
   19.81  		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
   19.82 -      |(Const("Divides.op dvd",_)$ d $ (db as (Const ("op +",_) $ (Const ("op *",_) $
   19.83 +      |(Const("Divides.op dvd",_)$ d $ (db as (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $
   19.84        c $ y ) $ z))) => 
   19.85           if y=x then  let val cz = cterm_of sg (norm_zero_one z)
   19.86  			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
   19.87 @@ -373,22 +373,22 @@
   19.88     let
   19.89     val fm = norm_zero_one fm1
   19.90      in  case fm1 of 
   19.91 -      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
   19.92 +      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) => 
   19.93           if  (x=y) andalso (c1=zero) andalso (c2=one) 
   19.94  	   then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (neq_eq_minf))
   19.95             else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
   19.96  
   19.97 -      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
   19.98 +      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
   19.99    	   if (is_arith_rel fm) andalso (x=y) andalso ((c1=zero) orelse (c1 = norm_zero_one zero)) andalso ((c2=one) orelse (c1 = norm_zero_one one))
  19.100  	     then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (eq_eq_minf))
  19.101  	     else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf)) 
  19.102  
  19.103 -      |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
  19.104 +      |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
  19.105             if (y=x) andalso (c1 =zero) then 
  19.106              if pm1 = one then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (le_eq_minf)) else
  19.107  	     (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (len_eq_minf))
  19.108  	    else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
  19.109 -      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
  19.110 +      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
  19.111           if y=x then  let val cd = cterm_of sg (norm_zero_one d)
  19.112  	 		  val cz = cterm_of sg (norm_zero_one z)
  19.113  	 	      in(instantiate' [] [SOME cd,  SOME cz] (not_dvd_eq_minf)) 
  19.114 @@ -396,7 +396,7 @@
  19.115  
  19.116  		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
  19.117  		
  19.118 -      |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
  19.119 +      |(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
  19.120           if y=x then  let val cd = cterm_of sg (norm_zero_one d)
  19.121  	 		  val cz = cterm_of sg (norm_zero_one z)
  19.122  	 	      in(instantiate' [] [SOME cd, SOME cz ] (dvd_eq_minf))
  19.123 @@ -431,30 +431,30 @@
  19.124    val cfalse = cterm_of sg HOLogic.false_const
  19.125    val fm = norm_zero_one fm1
  19.126   in  case fm1 of 
  19.127 -      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
  19.128 +      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) => 
  19.129           if ((x=y) andalso (c1= zero) andalso (c2= one))
  19.130  	 then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_pinf))
  19.131           else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
  19.132  
  19.133 -      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
  19.134 +      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
  19.135    	if ((is_arith_rel fm) andalso (x = y) andalso (c1 = zero)  andalso (c2 = one)) 
  19.136  	then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_pinf))
  19.137  	else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
  19.138  
  19.139 -      |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
  19.140 +      |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
  19.141          if ((y=x) andalso (c1 = zero)) then 
  19.142            if (pm1 = one) 
  19.143  	  then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_pinf)) 
  19.144  	  else (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_pinf))
  19.145  	else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
  19.146    
  19.147 -      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
  19.148 +      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
  19.149           if y=x then  let val cz = cterm_of sg (norm_zero_one z)
  19.150  			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
  19.151  	 	      in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_pinf)))
  19.152  		      end
  19.153  		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
  19.154 -      |(Const("Divides.op dvd",_)$ d $ (db as (Const ("op +",_) $ (Const ("op *",_) $
  19.155 +      |(Const("Divides.op dvd",_)$ d $ (db as (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $
  19.156        c $ y ) $ z))) => 
  19.157           if y=x then  let val cz = cterm_of sg (norm_zero_one z)
  19.158  			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
  19.159 @@ -472,22 +472,22 @@
  19.160    let
  19.161  					val fm = norm_zero_one fm1
  19.162      in  case fm1 of 
  19.163 -      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
  19.164 +      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) => 
  19.165           if  (x=y) andalso (c1=zero) andalso (c2=one) 
  19.166  	   then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (neq_eq_pinf))
  19.167             else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
  19.168  
  19.169 -      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
  19.170 +      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
  19.171    	   if (is_arith_rel fm) andalso (x=y) andalso ((c1=zero) orelse (c1 = norm_zero_one zero)) andalso ((c2=one) orelse (c1 = norm_zero_one one))
  19.172  	     then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (eq_eq_pinf))
  19.173  	     else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf)) 
  19.174  
  19.175 -      |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
  19.176 +      |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
  19.177             if (y=x) andalso (c1 =zero) then 
  19.178              if pm1 = one then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (le_eq_pinf)) else
  19.179  	     (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (len_eq_pinf))
  19.180  	    else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
  19.181 -      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
  19.182 +      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
  19.183           if y=x then  let val cd = cterm_of sg (norm_zero_one d)
  19.184  	 		  val cz = cterm_of sg (norm_zero_one z)
  19.185  	 	      in(instantiate' [] [SOME cd,  SOME cz] (not_dvd_eq_pinf)) 
  19.186 @@ -495,7 +495,7 @@
  19.187  
  19.188  		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
  19.189  		
  19.190 -      |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
  19.191 +      |(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
  19.192           if y=x then  let val cd = cterm_of sg (norm_zero_one d)
  19.193  	 		  val cz = cterm_of sg (norm_zero_one z)
  19.194  	 	      in(instantiate' [] [SOME cd, SOME cz ] (dvd_eq_pinf))
  19.195 @@ -567,31 +567,31 @@
  19.196      val cat = cterm_of sg (norm_zero_one at)
  19.197    in
  19.198    case at of 
  19.199 -   (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
  19.200 +   (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) => 
  19.201        if  (x=y) andalso (c1=zero) andalso (c2=one) 
  19.202  	 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)
  19.203 -	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one  z)))
  19.204 +	          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)))
  19.205  		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
  19.206  	 in  (instantiate' [] [SOME cfma]([th3,th1,th2] MRS (not_bst_p_ne)))
  19.207  	 end
  19.208           else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
  19.209  
  19.210 -   |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", T) $(Const ("op *",_) $ c2 $ y) $z)) =>
  19.211 +   |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", T) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
  19.212       if (is_arith_rel at) andalso (x=y)
  19.213  	then let val bst_z = norm_zero_one (linear_neg (linear_add [] z (mk_numeral 1)))
  19.214  	         in let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ bst_z $ B)
  19.215 -	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq (bst_z,Const("op -",T) $ (Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("1",HOLogic.intT))))
  19.216 +	          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))))
  19.217  		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
  19.218  	 in  (instantiate' [] [SOME cfma] ([th3,th1,th2] MRS (not_bst_p_eq)))
  19.219  	 end
  19.220         end
  19.221           else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
  19.222  
  19.223 -   |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
  19.224 +   |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
  19.225          if (y=x) andalso (c1 =zero) then 
  19.226          if pm1 = one then 
  19.227  	  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)
  19.228 -              val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
  19.229 +              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)))
  19.230  	  in  (instantiate' [] [SOME cfma,  SOME cdlcm]([th1,th2] MRS (not_bst_p_gt)))
  19.231  	    end
  19.232  	 else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
  19.233 @@ -599,7 +599,7 @@
  19.234  	      end
  19.235        else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
  19.236  
  19.237 -   |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
  19.238 +   |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
  19.239        if y=x then  
  19.240             let val cz = cterm_of sg (norm_zero_one z)
  19.241  	       val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
  19.242 @@ -607,7 +607,7 @@
  19.243  	     end
  19.244        else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
  19.245  
  19.246 -   |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
  19.247 +   |(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
  19.248         if y=x then  
  19.249  	 let val cz = cterm_of sg (norm_zero_one z)
  19.250  	     val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
  19.251 @@ -658,26 +658,26 @@
  19.252      val cat = cterm_of sg (norm_zero_one at)
  19.253    in
  19.254    case at of 
  19.255 -   (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
  19.256 +   (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) => 
  19.257        if  (x=y) andalso (c1=zero) andalso (c2=one) 
  19.258  	 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)
  19.259 -	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one  z)))
  19.260 +	          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)))
  19.261  		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
  19.262  	 in  (instantiate' [] [SOME cfma]([th3,th1,th2] MRS (not_ast_p_ne)))
  19.263  	 end
  19.264           else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
  19.265  
  19.266 -   |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", T) $(Const ("op *",_) $ c2 $ y) $z)) =>
  19.267 +   |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", T) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
  19.268       if (is_arith_rel at) andalso (x=y)
  19.269  	then let val ast_z = norm_zero_one (linear_sub [] one z )
  19.270  	         val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ ast_z $ A)
  19.271 -	         val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq (ast_z,Const("op +",T) $ (Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("1",HOLogic.intT))))
  19.272 +	         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))))
  19.273  		 val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
  19.274  	 in  (instantiate' [] [SOME cfma] ([th3,th1,th2] MRS (not_ast_p_eq)))
  19.275         end
  19.276           else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
  19.277  
  19.278 -   |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
  19.279 +   |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
  19.280          if (y=x) andalso (c1 =zero) then 
  19.281          if pm1 = (mk_numeral ~1) then 
  19.282  	  let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one z) $ A)
  19.283 @@ -689,7 +689,7 @@
  19.284  	      end
  19.285        else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
  19.286  
  19.287 -   |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
  19.288 +   |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
  19.289        if y=x then  
  19.290             let val cz = cterm_of sg (norm_zero_one z)
  19.291  	       val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
  19.292 @@ -697,7 +697,7 @@
  19.293  	     end
  19.294        else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
  19.295  
  19.296 -   |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
  19.297 +   |(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
  19.298         if y=x then  
  19.299  	 let val cz = cterm_of sg (norm_zero_one z)
  19.300  	     val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
    20.1 --- a/src/HOL/Integ/int_arith1.ML	Fri Mar 10 12:28:38 2006 +0100
    20.2 +++ b/src/HOL/Integ/int_arith1.ML	Fri Mar 10 15:33:48 2006 +0100
    20.3 @@ -197,11 +197,11 @@
    20.4           handle TERM _ => find_first_numeral (t::past) terms)
    20.5    | find_first_numeral past [] = raise TERM("find_first_numeral", []);
    20.6  
    20.7 -val mk_plus = HOLogic.mk_binop "op +";
    20.8 +val mk_plus = HOLogic.mk_binop "HOL.plus";
    20.9  
   20.10  fun mk_minus t = 
   20.11    let val T = Term.fastype_of t
   20.12 -  in Const ("uminus", T --> T) $ t
   20.13 +  in Const ("HOL.uminus", T --> T) $ t
   20.14    end;
   20.15  
   20.16  (*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
   20.17 @@ -213,22 +213,22 @@
   20.18  fun long_mk_sum T []        = mk_numeral T 0
   20.19    | long_mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
   20.20  
   20.21 -val dest_plus = HOLogic.dest_bin "op +" Term.dummyT;
   20.22 +val dest_plus = HOLogic.dest_bin "HOL.plus" Term.dummyT;
   20.23  
   20.24  (*decompose additions AND subtractions as a sum*)
   20.25 -fun dest_summing (pos, Const ("op +", _) $ t $ u, ts) =
   20.26 +fun dest_summing (pos, Const ("HOL.plus", _) $ t $ u, ts) =
   20.27          dest_summing (pos, t, dest_summing (pos, u, ts))
   20.28 -  | dest_summing (pos, Const ("op -", _) $ t $ u, ts) =
   20.29 +  | dest_summing (pos, Const ("HOL.minus", _) $ t $ u, ts) =
   20.30          dest_summing (pos, t, dest_summing (not pos, u, ts))
   20.31    | dest_summing (pos, t, ts) =
   20.32          if pos then t::ts else mk_minus t :: ts;
   20.33  
   20.34  fun dest_sum t = dest_summing (true, t, []);
   20.35  
   20.36 -val mk_diff = HOLogic.mk_binop "op -";
   20.37 -val dest_diff = HOLogic.dest_bin "op -" Term.dummyT;
   20.38 +val mk_diff = HOLogic.mk_binop "HOL.minus";
   20.39 +val dest_diff = HOLogic.dest_bin "HOL.minus" Term.dummyT;
   20.40  
   20.41 -val mk_times = HOLogic.mk_binop "op *";
   20.42 +val mk_times = HOLogic.mk_binop "HOL.times";
   20.43  
   20.44  fun mk_prod T = 
   20.45    let val one = mk_numeral T 1
   20.46 @@ -241,7 +241,7 @@
   20.47  fun long_mk_prod T []        = mk_numeral T 1
   20.48    | long_mk_prod T (t :: ts) = mk_times (t, mk_prod T ts);
   20.49  
   20.50 -val dest_times = HOLogic.dest_bin "op *" Term.dummyT;
   20.51 +val dest_times = HOLogic.dest_bin "HOL.times" Term.dummyT;
   20.52  
   20.53  fun dest_prod t =
   20.54        let val (t,u) = dest_times t
   20.55 @@ -252,7 +252,7 @@
   20.56  fun mk_coeff (k, t) = mk_times (mk_numeral (Term.fastype_of t) k, t);
   20.57  
   20.58  (*Express t as a product of (possibly) a numeral with other sorted terms*)
   20.59 -fun dest_coeff sign (Const ("uminus", _) $ t) = dest_coeff (~sign) t
   20.60 +fun dest_coeff sign (Const ("HOL.uminus", _) $ t) = dest_coeff (~sign) t
   20.61    | dest_coeff sign t =
   20.62      let val ts = sort Term.term_ord (dest_prod t)
   20.63          val (n, ts') = find_first_numeral [] ts
    21.1 --- a/src/HOL/Integ/nat_simprocs.ML	Fri Mar 10 12:28:38 2006 +0100
    21.2 +++ b/src/HOL/Integ/nat_simprocs.ML	Fri Mar 10 15:33:48 2006 +0100
    21.3 @@ -39,7 +39,7 @@
    21.4    | find_first_numeral past [] = raise TERM("find_first_numeral", []);
    21.5  
    21.6  val zero = mk_numeral 0;
    21.7 -val mk_plus = HOLogic.mk_binop "op +";
    21.8 +val mk_plus = HOLogic.mk_binop "HOL.plus";
    21.9  
   21.10  (*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
   21.11  fun mk_sum []        = zero
   21.12 @@ -50,7 +50,7 @@
   21.13  fun long_mk_sum []        = HOLogic.zero
   21.14    | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
   21.15  
   21.16 -val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT;
   21.17 +val dest_plus = HOLogic.dest_bin "HOL.plus" HOLogic.natT;
   21.18  
   21.19  (*extract the outer Sucs from a term and convert them to a binary numeral*)
   21.20  fun dest_Sucs (k, Const ("Suc", _) $ t) = dest_Sucs (k+1, t)
   21.21 @@ -85,14 +85,14 @@
   21.22  (*** CancelNumerals simprocs ***)
   21.23  
   21.24  val one = mk_numeral 1;
   21.25 -val mk_times = HOLogic.mk_binop "op *";
   21.26 +val mk_times = HOLogic.mk_binop "HOL.times";
   21.27  
   21.28  fun mk_prod [] = one
   21.29    | mk_prod [t] = t
   21.30    | mk_prod (t :: ts) = if t = one then mk_prod ts
   21.31                          else mk_times (t, mk_prod ts);
   21.32  
   21.33 -val dest_times = HOLogic.dest_bin "op *" HOLogic.natT;
   21.34 +val dest_times = HOLogic.dest_bin "HOL.times" HOLogic.natT;
   21.35  
   21.36  fun dest_prod t =
   21.37        let val (t,u) = dest_times t
   21.38 @@ -213,8 +213,8 @@
   21.39  structure DiffCancelNumerals = CancelNumeralsFun
   21.40   (open CancelNumeralsCommon
   21.41    val prove_conv = Bin_Simprocs.prove_conv
   21.42 -  val mk_bal   = HOLogic.mk_binop "op -"
   21.43 -  val dest_bal = HOLogic.dest_bin "op -" HOLogic.natT
   21.44 +  val mk_bal   = HOLogic.mk_binop "HOL.minus"
   21.45 +  val dest_bal = HOLogic.dest_bin "HOL.minus" HOLogic.natT
   21.46    val bal_add1 = nat_diff_add_eq1 RS trans
   21.47    val bal_add2 = nat_diff_add_eq2 RS trans
   21.48  );
    22.1 --- a/src/HOL/Integ/presburger.ML	Fri Mar 10 12:28:38 2006 +0100
    22.2 +++ b/src/HOL/Integ/presburger.ML	Fri Mar 10 15:33:48 2006 +0100
    22.3 @@ -139,11 +139,11 @@
    22.4     ("Divides.op dvd", iT --> iT --> bT),
    22.5     ("Divides.op div", iT --> iT --> iT),
    22.6     ("Divides.op mod", iT --> iT --> iT),
    22.7 -   ("op +", iT --> iT --> iT),
    22.8 -   ("op -", iT --> iT --> iT),
    22.9 -   ("op *", iT --> iT --> iT), 
   22.10 +   ("HOL.plus", iT --> iT --> iT),
   22.11 +   ("HOL.minus", iT --> iT --> iT),
   22.12 +   ("HOL.times", iT --> iT --> iT), 
   22.13     ("HOL.abs", iT --> iT),
   22.14 -   ("uminus", iT --> iT),
   22.15 +   ("HOL.uminus", iT --> iT),
   22.16     ("HOL.max", iT --> iT --> iT),
   22.17     ("HOL.min", iT --> iT --> iT),
   22.18  
   22.19 @@ -153,9 +153,9 @@
   22.20     ("Divides.op dvd", nT --> nT --> bT),
   22.21     ("Divides.op div", nT --> nT --> nT),
   22.22     ("Divides.op mod", nT --> nT --> nT),
   22.23 -   ("op +", nT --> nT --> nT),
   22.24 -   ("op -", nT --> nT --> nT),
   22.25 -   ("op *", nT --> nT --> nT), 
   22.26 +   ("HOL.plus", nT --> nT --> nT),
   22.27 +   ("HOL.minus", nT --> nT --> nT),
   22.28 +   ("HOL.times", nT --> nT --> nT), 
   22.29     ("Suc", nT --> nT),
   22.30     ("HOL.max", nT --> nT --> nT),
   22.31     ("HOL.min", nT --> nT --> nT),
    23.1 --- a/src/HOL/Integ/reflected_cooper.ML	Fri Mar 10 12:28:38 2006 +0100
    23.2 +++ b/src/HOL/Integ/reflected_cooper.ML	Fri Mar 10 15:33:48 2006 +0100
    23.3 @@ -16,10 +16,10 @@
    23.4        | Const("0",iT) => Cst 0
    23.5        | Const("1",iT) => Cst 1
    23.6        | Bound i => Var (nat (IntInf.fromInt i))
    23.7 -      | Const("uminus",_)$t' => Neg (i_of_term vs t')
    23.8 -      | Const ("op +",_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
    23.9 -      | Const ("op -",_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
   23.10 -      | Const ("op *",_)$t1$t2 => Mult (i_of_term vs t1,i_of_term vs t2)
   23.11 +      | Const("HOL.uminus",_)$t' => Neg (i_of_term vs t')
   23.12 +      | Const ("HOL.plus",_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
   23.13 +      | Const ("HOL.minus",_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
   23.14 +      | Const ("HOL.times",_)$t1$t2 => Mult (i_of_term vs t1,i_of_term vs t2)
   23.15        | Const ("Numeral.number_of",_)$t' => Cst (HOLogic.dest_binum t')
   23.16        | _ => error "i_of_term: unknown term";
   23.17  	
   23.18 @@ -77,12 +77,12 @@
   23.19      case t of 
   23.20  	Cst i => CooperDec.mk_numeral i
   23.21        | Var n => valOf (myassoc2 vs n)
   23.22 -      | Neg t' => Const("uminus",iT --> iT)$(term_of_i vs t')
   23.23 -      | Add(t1,t2) => Const("op +",[iT,iT] ---> iT)$
   23.24 +      | Neg t' => Const("HOL.uminus",iT --> iT)$(term_of_i vs t')
   23.25 +      | Add(t1,t2) => Const("HOL.plus",[iT,iT] ---> iT)$
   23.26  			   (term_of_i vs t1)$(term_of_i vs t2)
   23.27 -      | Sub(t1,t2) => Const("op -",[iT,iT] ---> iT)$
   23.28 +      | Sub(t1,t2) => Const("HOL.minus",[iT,iT] ---> iT)$
   23.29  			   (term_of_i vs t1)$(term_of_i vs t2)
   23.30 -      | Mult(t1,t2) => Const("op *",[iT,iT] ---> iT)$
   23.31 +      | Mult(t1,t2) => Const("HOL.times",[iT,iT] ---> iT)$
   23.32  			   (term_of_i vs t1)$(term_of_i vs t2);
   23.33  
   23.34  fun term_of_qf vs t = 
    24.1 --- a/src/HOL/Library/ExecutableRat.thy	Fri Mar 10 12:28:38 2006 +0100
    24.2 +++ b/src/HOL/Library/ExecutableRat.thy	Fri Mar 10 15:33:48 2006 +0100
    24.3 @@ -15,13 +15,13 @@
    24.4  
    24.5  datatype erat = Rat bool int int
    24.6  
    24.7 -instance erat :: zero by intro_classes
    24.8 -instance erat :: one by intro_classes
    24.9 -instance erat :: plus by intro_classes
   24.10 -instance erat :: minus by intro_classes
   24.11 -instance erat :: times by intro_classes
   24.12 -instance erat :: inverse by intro_classes
   24.13 -instance erat :: ord by intro_classes
   24.14 +instance erat :: zero ..
   24.15 +instance erat :: one ..
   24.16 +instance erat :: plus ..
   24.17 +instance erat :: minus ..
   24.18 +instance erat :: times ..
   24.19 +instance erat :: inverse ..
   24.20 +instance erat :: ord ..
   24.21  
   24.22  consts
   24.23    norm :: "erat \<Rightarrow> erat"
   24.24 @@ -85,12 +85,6 @@
   24.25    ml (target_atom "{*erat*}")
   24.26    haskell (target_atom "{*erat*}")
   24.27  
   24.28 -code_alias
   24.29 -  (* an intermediate solution until name resolving of ad-hoc overloaded
   24.30 -     constants is refined *)
   24.31 -  "HOL.inverse" "Rational.inverse"
   24.32 -  "HOL.divide" "Rational.divide"
   24.33 -
   24.34  code_syntax_const
   24.35    Fract
   24.36      ml ("{*of_quotient*}")
   24.37 @@ -103,7 +97,7 @@
   24.38      haskell ("{*1::erat*}")
   24.39    "op + :: rat \<Rightarrow> rat \<Rightarrow> rat"
   24.40      ml ("{*op + :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
   24.41 -    haskell ("{*op + :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
   24.42 +    haskell ("{*HOL.plus :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
   24.43    "uminus :: rat \<Rightarrow> rat"
   24.44      ml ("{*uminus :: erat \<Rightarrow> erat*}")
   24.45      haskell ("{*uminus :: erat \<Rightarrow> erat*}")
    25.1 --- a/src/HOL/Library/ExecutableSet.thy	Fri Mar 10 12:28:38 2006 +0100
    25.2 +++ b/src/HOL/Library/ExecutableSet.thy	Fri Mar 10 15:33:48 2006 +0100
    25.3 @@ -40,7 +40,7 @@
    25.4    "insert"  ("(_ ins _)")
    25.5    "op Un"   ("(_ union _)")
    25.6    "op Int"  ("(_ inter _)")
    25.7 -  "op -" :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("(_ \\\\ _)")
    25.8 +  "HOL.minus" :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("(_ \\\\ _)")
    25.9    "image"   ("\<module>image")
   25.10  attach {*
   25.11  fun image f S = distinct (map f S);
    26.1 --- a/src/HOL/Library/comm_ring.ML	Fri Mar 10 12:28:38 2006 +0100
    26.2 +++ b/src/HOL/Library/comm_ring.ML	Fri Mar 10 15:33:48 2006 +0100
    26.3 @@ -77,13 +77,13 @@
    26.4  (* reification of polynom expressions *)
    26.5  fun reif_polex T vs t =
    26.6      case t of
    26.7 -        Const("op +",_)$a$b => (polex_add T)
    26.8 +        Const("HOL.plus",_)$a$b => (polex_add T)
    26.9                                     $ (reif_polex T vs a)$(reif_polex T vs b)
   26.10 -      | Const("op -",_)$a$b => (polex_sub T)
   26.11 +      | Const("HOL.minus",_)$a$b => (polex_sub T)
   26.12                                     $ (reif_polex T vs a)$(reif_polex T vs b)
   26.13 -      | Const("op *",_)$a$b =>  (polex_mul T)
   26.14 +      | Const("HOL.times",_)$a$b =>  (polex_mul T)
   26.15                                      $ (reif_polex T vs a)$ (reif_polex T vs b)
   26.16 -      | Const("uminus",_)$a => (polex_neg T)
   26.17 +      | Const("HOL.uminus",_)$a => (polex_neg T)
   26.18                                     $ (reif_polex T vs a)
   26.19        | (Const("Nat.power",_)$a$n) => (polex_pow T) $ (reif_polex T vs a) $ n
   26.20  
    27.1 --- a/src/HOL/OrderedGroup.ML	Fri Mar 10 12:28:38 2006 +0100
    27.2 +++ b/src/HOL/OrderedGroup.ML	Fri Mar 10 15:33:48 2006 +0100
    27.3 @@ -8,7 +8,7 @@
    27.4  
    27.5  (*** Term order for abelian groups ***)
    27.6  
    27.7 -fun agrp_ord a = find_index_eq a ["0", "op +", "uminus", "op -"];
    27.8 +fun agrp_ord a = find_index (fn a' => a = a') ["0", "HOL.plus", "HOL.uminus", "HOL.minus"];
    27.9  
   27.10  fun termless_agrp (a, b) = (Term.term_lpo agrp_ord (a, b) = LESS);
   27.11  
   27.12 @@ -16,9 +16,9 @@
   27.13    val ac1 = mk_meta_eq (thm "add_assoc");
   27.14    val ac2 = mk_meta_eq (thm "add_commute");
   27.15    val ac3 = mk_meta_eq (thm "add_left_commute");
   27.16 -  fun solve_add_ac thy _ (_ $ (Const ("op +",_) $ _ $ _) $ _) =
   27.17 +  fun solve_add_ac thy _ (_ $ (Const ("HOL.plus",_) $ _ $ _) $ _) =
   27.18          SOME ac1
   27.19 -    | solve_add_ac thy _ (_ $ x $ (Const ("op +",_) $ y $ z)) =
   27.20 +    | solve_add_ac thy _ (_ $ x $ (Const ("HOL.plus",_) $ y $ z)) =
   27.21          if termless_agrp (y, x) then SOME ac3 else NONE
   27.22      | solve_add_ac thy _ (_ $ x $ y) =
   27.23          if termless_agrp (y, x) then SOME ac2 else NONE
    28.1 --- a/src/HOL/OrderedGroup.thy	Fri Mar 10 12:28:38 2006 +0100
    28.2 +++ b/src/HOL/OrderedGroup.thy	Fri Mar 10 15:33:48 2006 +0100
    28.3 @@ -899,8 +899,7 @@
    28.4  lemma abs_triangle_ineq: "abs(a+b) \<le> abs a + abs(b::'a::lordered_ab_group_abs)"
    28.5  proof -
    28.6    have g:"abs a + abs b = join (a+b) (join (-a-b) (join (-a+b) (a + (-b))))" (is "_=join ?m ?n")
    28.7 -    apply (simp add: abs_lattice add_meet_join_distribs join_aci)
    28.8 -    by (simp only: diff_minus)
    28.9 +    by (simp add: abs_lattice add_meet_join_distribs join_aci diff_minus)
   28.10    have a:"a+b <= join ?m ?n" by (simp add: meet_join_le)
   28.11    have b:"-a-b <= ?n" by (simp add: meet_join_le) 
   28.12    have c:"?n <= join ?m ?n" by (simp add: meet_join_le)
    29.1 --- a/src/HOL/Real/Float.ML	Fri Mar 10 12:28:38 2006 +0100
    29.2 +++ b/src/HOL/Real/Float.ML	Fri Mar 10 15:33:48 2006 +0100
    29.3 @@ -330,10 +330,10 @@
    29.4  		
    29.5  val float_const = Const ("Float.float", HOLogic.mk_prodT (HOLogic.intT, HOLogic.intT) --> HOLogic.realT)
    29.6  
    29.7 -val float_add_const = Const ("op +", HOLogic.realT --> HOLogic.realT --> HOLogic.realT)
    29.8 -val float_diff_const = Const ("op -", HOLogic.realT --> HOLogic.realT --> HOLogic.realT)
    29.9 -val float_mult_const = Const ("op *", HOLogic.realT --> HOLogic.realT --> HOLogic.realT)
   29.10 -val float_uminus_const = Const ("uminus", HOLogic.realT --> HOLogic.realT)
   29.11 +val float_add_const = Const ("HOL.plus", HOLogic.realT --> HOLogic.realT --> HOLogic.realT)
   29.12 +val float_diff_const = Const ("HOL.minus", HOLogic.realT --> HOLogic.realT --> HOLogic.realT)
   29.13 +val float_mult_const = Const ("HOL.times", HOLogic.realT --> HOLogic.realT --> HOLogic.realT)
   29.14 +val float_uminus_const = Const ("HOL.uminus", HOLogic.realT --> HOLogic.realT)
   29.15  val float_abs_const = Const ("HOL.abs", HOLogic.realT --> HOLogic.realT)
   29.16  val float_le_const = Const ("op <=", HOLogic.realT --> HOLogic.realT --> HOLogic.boolT)
   29.17  val float_pprt_const = Const ("OrderedGroup.pprt", HOLogic.realT --> HOLogic.realT)
    30.1 --- a/src/HOL/Set.thy	Fri Mar 10 12:28:38 2006 +0100
    30.2 +++ b/src/HOL/Set.thy	Fri Mar 10 15:33:48 2006 +0100
    30.3 @@ -958,7 +958,7 @@
    30.4    outer-level constant, which in this case is just "op :"; we instead need
    30.5    to use term-nets to associate patterns with rules.  Also, if a rule fails to
    30.6    apply, then the formula should be kept.
    30.7 -  [("uminus", Compl_iff RS iffD1), ("op -", [Diff_iff RS iffD1]),
    30.8 +  [("HOL.uminus", Compl_iff RS iffD1), ("HOL.minus", [Diff_iff RS iffD1]),
    30.9     ("op Int", [IntD1,IntD2]),
   30.10     ("Collect", [CollectD]), ("Inter", [InterD]), ("INTER", [INT_D])]
   30.11   *)
    31.1 --- a/src/HOL/Tools/Presburger/cooper_dec.ML	Fri Mar 10 12:28:38 2006 +0100
    31.2 +++ b/src/HOL/Tools/Presburger/cooper_dec.ML	Fri Mar 10 15:33:48 2006 +0100
    31.3 @@ -116,8 +116,8 @@
    31.4   
    31.5  fun linear_cmul n tm =  if n = 0 then zero else let fun times n k = n*k in  
    31.6    ( case tm of  
    31.7 -     (Const("op +",T)  $  (Const ("op *",T1 ) $c1 $  x1) $ rest) => 
    31.8 -       Const("op +",T) $ ((Const("op *",T1) $ (numeral1 (times n) c1) $ x1)) $ (linear_cmul n rest) 
    31.9 +     (Const("HOL.plus",T)  $  (Const ("HOL.times",T1 ) $c1 $  x1) $ rest) => 
   31.10 +       Const("HOL.plus",T) $ ((Const("HOL.times",T1) $ (numeral1 (times n) c1) $ x1)) $ (linear_cmul n rest) 
   31.11      |_ =>  numeral1 (times n) tm) 
   31.12      end ; 
   31.13   
   31.14 @@ -139,23 +139,23 @@
   31.15  fun linear_add vars tm1 tm2 = 
   31.16    let fun addwith x y = x + y in
   31.17   (case (tm1,tm2) of 
   31.18 -	((Const ("op +",T1) $ ( Const("op *",T2) $ c1 $  x1) $ rest1),(Const 
   31.19 -	("op +",T3)$( Const("op *",T4) $ c2 $  x2) $ rest2)) => 
   31.20 +	((Const ("HOL.plus",T1) $ ( Const("HOL.times",T2) $ c1 $  x1) $ rest1),(Const 
   31.21 +	("HOL.plus",T3)$( Const("HOL.times",T4) $ c2 $  x2) $ rest2)) => 
   31.22           if x1 = x2 then 
   31.23                let val c = (numeral2 (addwith) c1 c2) 
   31.24  	      in 
   31.25                if c = zero then (linear_add vars rest1  rest2)  
   31.26 -	      else (Const("op +",T1) $ (Const("op *",T2) $ c $ x1) $ (linear_add vars  rest1 rest2)) 
   31.27 +	      else (Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c $ x1) $ (linear_add vars  rest1 rest2)) 
   31.28                end 
   31.29  	   else 
   31.30 -		if earlierv vars x1 x2 then (Const("op +",T1) $  
   31.31 -		(Const("op *",T2)$ c1 $ x1) $ (linear_add vars rest1 tm2)) 
   31.32 -    	       else (Const("op +",T1) $ (Const("op *",T2) $ c2 $ x2) $ (linear_add vars tm1 rest2)) 
   31.33 -   	|((Const("op +",T1) $ (Const("op *",T2) $ c1 $ x1) $ rest1) ,_) => 
   31.34 -    	  (Const("op +",T1)$ (Const("op *",T2) $ c1 $ x1) $ (linear_add vars 
   31.35 +		if earlierv vars x1 x2 then (Const("HOL.plus",T1) $  
   31.36 +		(Const("HOL.times",T2)$ c1 $ x1) $ (linear_add vars rest1 tm2)) 
   31.37 +    	       else (Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c2 $ x2) $ (linear_add vars tm1 rest2)) 
   31.38 +   	|((Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c1 $ x1) $ rest1) ,_) => 
   31.39 +    	  (Const("HOL.plus",T1)$ (Const("HOL.times",T2) $ c1 $ x1) $ (linear_add vars 
   31.40  	  rest1 tm2)) 
   31.41 -   	|(_, (Const("op +",T1) $(Const("op *",T2) $ c2 $ x2) $ rest2)) => 
   31.42 -      	  (Const("op +",T1) $ (Const("op *",T2) $ c2 $ x2) $ (linear_add vars tm1 
   31.43 +   	|(_, (Const("HOL.plus",T1) $(Const("HOL.times",T2) $ c2 $ x2) $ rest2)) => 
   31.44 +      	  (Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c2 $ x2) $ (linear_add vars tm1 
   31.45  	  rest2)) 
   31.46     	| (_,_) => numeral2 (addwith) tm1 tm2) 
   31.47  	 
   31.48 @@ -180,13 +180,13 @@
   31.49   Free(x,T)*) 
   31.50    
   31.51  fun lint vars tm = if is_numeral tm then tm else case tm of 
   31.52 -   (Free (x,T)) =>  (HOLogic.mk_binop "op +" ((HOLogic.mk_binop "op *" ((mk_numeral 1),Free (x,T))), zero)) 
   31.53 -  |(Bound i) =>  (Const("op +",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ 
   31.54 -  (Const("op *",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ (mk_numeral 1) $ (Bound i)) $ zero) 
   31.55 -  |(Const("uminus",_) $ t ) => (linear_neg (lint vars t)) 
   31.56 -  |(Const("op +",_) $ s $ t) => (linear_add vars (lint vars s) (lint vars t)) 
   31.57 -  |(Const("op -",_) $ s $ t) => (linear_sub vars (lint vars s) (lint vars t)) 
   31.58 -  |(Const ("op *",_) $ s $ t) => 
   31.59 +   (Free (x,T)) =>  (HOLogic.mk_binop "HOL.plus" ((HOLogic.mk_binop "HOL.times" ((mk_numeral 1),Free (x,T))), zero)) 
   31.60 +  |(Bound i) =>  (Const("HOL.plus",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ 
   31.61 +  (Const("HOL.times",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ (mk_numeral 1) $ (Bound i)) $ zero) 
   31.62 +  |(Const("HOL.uminus",_) $ t ) => (linear_neg (lint vars t)) 
   31.63 +  |(Const("HOL.plus",_) $ s $ t) => (linear_add vars (lint vars s) (lint vars t)) 
   31.64 +  |(Const("HOL.minus",_) $ s $ t) => (linear_sub vars (lint vars s) (lint vars t)) 
   31.65 +  |(Const ("HOL.times",_) $ s $ t) => 
   31.66          let val s' = lint vars s  
   31.67              val t' = lint vars t  
   31.68          in 
   31.69 @@ -212,14 +212,14 @@
   31.70        end 
   31.71      else (warning "Nonlinear term --- Non numeral leftside at dvd"
   31.72        ;raise COOPER)
   31.73 -  |linform vars  (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ s $ t ) = (mkatom vars "op =" (Const ("op -",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s) ) 
   31.74 -  |linform vars  (Const("op <",_)$ s $t ) = (mkatom vars "op <" (Const ("op -",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s))
   31.75 -  |linform vars  (Const("op >",_) $ s $ t ) = (mkatom vars "op <" (Const ("op -",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ s $ t)) 
   31.76 +  |linform vars  (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ s $ t ) = (mkatom vars "op =" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s) ) 
   31.77 +  |linform vars  (Const("op <",_)$ s $t ) = (mkatom vars "op <" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s))
   31.78 +  |linform vars  (Const("op >",_) $ s $ t ) = (mkatom vars "op <" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ s $ t)) 
   31.79    |linform vars  (Const("op <=",_)$ s $ t ) = 
   31.80 -        (mkatom vars "op <" (Const ("op -",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ (Const("op +",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $t $(mk_numeral 1)) $ s)) 
   31.81 +        (mkatom vars "op <" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $t $(mk_numeral 1)) $ s)) 
   31.82    |linform vars  (Const("op >=",_)$ s $ t ) = 
   31.83 -        (mkatom vars "op <" (Const ("op -",HOLogic.intT --> HOLogic.intT --> 
   31.84 -	HOLogic.intT) $ (Const("op +",HOLogic.intT --> HOLogic.intT --> 
   31.85 +        (mkatom vars "op <" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> 
   31.86 +	HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT --> 
   31.87  	HOLogic.intT) $s $(mk_numeral 1)) $ t)) 
   31.88   
   31.89     |linform vars  fm =  fm; 
   31.90 @@ -246,7 +246,7 @@
   31.91  fun lcm_num a b = (abs a*b) div (gcd (abs a) (abs b)); 
   31.92   
   31.93  fun formlcm x fm = case fm of 
   31.94 -    (Const (p,_)$ _ $(Const ("op +", _)$(Const ("op *",_)$ c $ y ) $z ) ) =>  if 
   31.95 +    (Const (p,_)$ _ $(Const ("HOL.plus", _)$(Const ("HOL.times",_)$ c $ y ) $z ) ) =>  if 
   31.96      (is_arith_rel fm) andalso (x = y) then  (abs(dest_numeral c)) else 1 
   31.97    | ( Const ("Not", _) $p) => formlcm x p 
   31.98    | ( Const ("op &",_) $ p $ q) => lcm_num (formlcm x p) (formlcm x q) 
   31.99 @@ -259,13 +259,13 @@
  31.100   
  31.101  fun adjustcoeff x l fm = 
  31.102       case fm of  
  31.103 -      (Const(p,_) $d $( Const ("op +", _)$(Const ("op *",_) $ 
  31.104 +      (Const(p,_) $d $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $ 
  31.105        c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then  
  31.106          let val m = l div (dest_numeral c) 
  31.107              val n = (if p = "op <" then abs(m) else m) 
  31.108 -            val xtm = HOLogic.mk_binop "op *" ((mk_numeral (m div n)), x) 
  31.109 +            val xtm = HOLogic.mk_binop "HOL.times" ((mk_numeral (m div n)), x) 
  31.110  	in
  31.111 -        (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "op +" ( xtm ,( linear_cmul n z) )))) 
  31.112 +        (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) )))) 
  31.113  	end 
  31.114  	else fm 
  31.115    |( Const ("Not", _) $ p) => HOLogic.Not $ (adjustcoeff x l p) 
  31.116 @@ -282,8 +282,8 @@
  31.117        val fm' = adjustcoeff x l fm in
  31.118        if l = 1 then fm' 
  31.119  	 else 
  31.120 -     let val xp = (HOLogic.mk_binop "op +"  
  31.121 -     		((HOLogic.mk_binop "op *" ((mk_numeral 1), x )), zero))
  31.122 +     let val xp = (HOLogic.mk_binop "HOL.plus"  
  31.123 +     		((HOLogic.mk_binop "HOL.times" ((mk_numeral 1), x )), zero))
  31.124  	in 
  31.125        HOLogic.conj $(HOLogic.mk_binrel "Divides.op dvd" ((mk_numeral l) , xp )) $ (adjustcoeff x l fm) 
  31.126        end 
  31.127 @@ -294,12 +294,12 @@
  31.128  (*
  31.129  fun adjustcoeffeq x l fm = 
  31.130      case fm of  
  31.131 -      (Const(p,_) $d $( Const ("op +", _)$(Const ("op *",_) $ 
  31.132 +      (Const(p,_) $d $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $ 
  31.133        c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then  
  31.134          let val m = l div (dest_numeral c) 
  31.135              val n = (if p = "op <" then abs(m) else m)  
  31.136 -            val xtm = (HOLogic.mk_binop "op *" ((mk_numeral ((m div n)*l) ), x))
  31.137 -            in (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "op +" ( xtm ,( linear_cmul n z) )))) 
  31.138 +            val xtm = (HOLogic.mk_binop "HOL.times" ((mk_numeral ((m div n)*l) ), x))
  31.139 +            in (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) )))) 
  31.140  	    end 
  31.141  	else fm 
  31.142    |( Const ("Not", _) $ p) => HOLogic.Not $ (adjustcoeffeq x l p) 
  31.143 @@ -315,11 +315,11 @@
  31.144  (* ------------------------------------------------------------------------- *) 
  31.145   
  31.146  fun minusinf x fm = case fm of  
  31.147 -    (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) => 
  31.148 +    (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) => 
  31.149    	 if (is_arith_rel fm) andalso (x=y) andalso (c2 = one) andalso (c1 =zero) then HOLogic.false_const  
  31.150  	 				 else fm 
  31.151   
  31.152 -  |(Const("op <",_) $ c $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z 
  31.153 +  |(Const("op <",_) $ c $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z 
  31.154    )) => if (x = y) 
  31.155  	then if (pm1 = one) andalso (c = zero) then HOLogic.false_const 
  31.156  	     else if (dest_numeral pm1 = ~1) andalso (c = zero) then HOLogic.true_const 
  31.157 @@ -336,11 +336,11 @@
  31.158  (* ------------------------------------------------------------------------- *)
  31.159  
  31.160  fun plusinf x fm = case fm of
  31.161 -    (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
  31.162 +    (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
  31.163    	 if (is_arith_rel fm) andalso (x=y) andalso (c2 = one) andalso (c1 =zero) then HOLogic.false_const
  31.164  	 				 else fm
  31.165  
  31.166 -  |(Const("op <",_) $ c $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z
  31.167 +  |(Const("op <",_) $ c $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z
  31.168    )) => if (x = y) 
  31.169  	then if (pm1 = one) andalso (c = zero) then HOLogic.true_const 
  31.170  	     else if (dest_numeral pm1 = ~1) andalso (c = zero) then HOLogic.false_const
  31.171 @@ -356,7 +356,7 @@
  31.172  (* The LCM of all the divisors that involve x.                               *) 
  31.173  (* ------------------------------------------------------------------------- *) 
  31.174   
  31.175 -fun divlcm x (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z ) ) =  
  31.176 +fun divlcm x (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z ) ) =  
  31.177          if x = y then abs(dest_numeral d) else 1 
  31.178    |divlcm x ( Const ("Not", _) $ p) = divlcm x p 
  31.179    |divlcm x ( Const ("op &",_) $ p $ q) = lcm_num (divlcm x p) (divlcm x q) 
  31.180 @@ -370,15 +370,15 @@
  31.181  fun bset x fm = case fm of 
  31.182     (Const ("Not", _) $ p) => if (is_arith_rel p) then  
  31.183            (case p of  
  31.184 -	      (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $c2 $y) $a ) )  
  31.185 +	      (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $c2 $y) $a ) )  
  31.186  	             => if (is_arith_rel p) andalso (x=	y) andalso (c2 = one) andalso (c1 = zero)  
  31.187  	                then [linear_neg a] 
  31.188  			else  bset x p 
  31.189     	  |_ =>[]) 
  31.190  			 
  31.191  			else bset x p 
  31.192 -  |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +",_) $ (Const ("op *",_) $c2 $ x) $ a)) =>  if (c1 =zero) andalso (c2 = one) then [linear_neg(linear_add [] a (mk_numeral 1))]  else [] 
  31.193 -  |(Const ("op <",_) $ c1$ (Const ("op +",_) $(Const ("op *",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg a] else [] 
  31.194 +  |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) =>  if (c1 =zero) andalso (c2 = one) then [linear_neg(linear_add [] a (mk_numeral 1))]  else [] 
  31.195 +  |(Const ("op <",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg a] else [] 
  31.196    |(Const ("op &",_) $ p $ q) => (bset x p) union (bset x q) 
  31.197    |(Const ("op |",_) $ p $ q) => (bset x p) union (bset x q) 
  31.198    |_ => []; 
  31.199 @@ -390,15 +390,15 @@
  31.200  fun aset x fm = case fm of
  31.201     (Const ("Not", _) $ p) => if (is_arith_rel p) then
  31.202            (case p of
  31.203 -	      (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $c2 $y) $a ) )
  31.204 +	      (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $c2 $y) $a ) )
  31.205  	             => if (x=	y) andalso (c2 = one) andalso (c1 = zero)
  31.206  	                then [linear_neg a]
  31.207  			else  []
  31.208     	  |_ =>[])
  31.209  
  31.210  			else aset x p
  31.211 -  |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +",_) $ (Const ("op *",_) $c2 $ x) $ a)) =>  if (c1 =zero) andalso (c2 = one) then [linear_sub [] (mk_numeral 1) a]  else []
  31.212 -  |(Const ("op <",_) $ c1$ (Const ("op +",_) $(Const ("op *",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = (mk_numeral (~1))) then [a] else []
  31.213 +  |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) =>  if (c1 =zero) andalso (c2 = one) then [linear_sub [] (mk_numeral 1) a]  else []
  31.214 +  |(Const ("op <",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = (mk_numeral (~1))) then [a] else []
  31.215    |(Const ("op &",_) $ p $ q) => (aset x p) union (aset x q)
  31.216    |(Const ("op |",_) $ p $ q) => (aset x p) union (aset x q)
  31.217    |_ => [];
  31.218 @@ -409,7 +409,7 @@
  31.219  (* ------------------------------------------------------------------------- *) 
  31.220   
  31.221  fun linrep vars x t fm = case fm of  
  31.222 -   ((Const(p,_)$ d $ (Const("op +",_)$(Const("op *",_)$ c $ y) $ z))) => 
  31.223 +   ((Const(p,_)$ d $ (Const("HOL.plus",_)$(Const("HOL.times",_)$ c $ y) $ z))) => 
  31.224        if (x = y) andalso (is_arith_rel fm)  
  31.225        then  
  31.226          let val ct = linear_cmul (dest_numeral c) t  
  31.227 @@ -435,8 +435,8 @@
  31.228     val dn = dest_numeral d
  31.229     fun coeffs_of x = case x of 
  31.230       Const(p,_) $ tl $ tr => 
  31.231 -       if p = "op +" then (coeffs_of tl) union (coeffs_of tr)
  31.232 -          else if p = "op *" 
  31.233 +       if p = "HOL.plus" then (coeffs_of tl) union (coeffs_of tr)
  31.234 +          else if p = "HOL.times" 
  31.235  	        then if (is_numeral tr) 
  31.236  		 then [(dest_numeral tr) * (dest_numeral tl)] 
  31.237  		 else [dest_numeral tl]
    32.1 --- a/src/HOL/Tools/Presburger/cooper_proof.ML	Fri Mar 10 12:28:38 2006 +0100
    32.2 +++ b/src/HOL/Tools/Presburger/cooper_proof.ML	Fri Mar 10 15:33:48 2006 +0100
    32.3 @@ -165,11 +165,11 @@
    32.4  (* ------------------------------------------------------------------------- *)
    32.5  
    32.6  fun norm_zero_one fm = case fm of
    32.7 -  (Const ("op *",_) $ c $ t) => 
    32.8 +  (Const ("HOL.times",_) $ c $ t) => 
    32.9      if c = one then (norm_zero_one t)
   32.10      else if (dest_numeral c = ~1) 
   32.11 -         then (Const("uminus",HOLogic.intT --> HOLogic.intT) $ (norm_zero_one t))
   32.12 -         else (HOLogic.mk_binop "op *" (norm_zero_one c,norm_zero_one t))
   32.13 +         then (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $ (norm_zero_one t))
   32.14 +         else (HOLogic.mk_binop "HOL.times" (norm_zero_one c,norm_zero_one t))
   32.15    |(node $ rest) => ((norm_zero_one node)$(norm_zero_one rest))
   32.16    |(Abs(x,T,p)) => (Abs(x,T,(norm_zero_one p)))
   32.17    |_ => fm;
   32.18 @@ -255,13 +255,13 @@
   32.19  (*==================================================*)
   32.20  
   32.21  fun decomp_adjustcoeffeq sg x l fm = case fm of
   32.22 -    (Const("Not",_)$(Const("op <",_) $(Const("0",_)) $(rt as (Const ("op +", _)$(Const ("op *",_) $    c $ y ) $z )))) => 
   32.23 +    (Const("Not",_)$(Const("op <",_) $(Const("0",_)) $(rt as (Const ("HOL.plus", _)$(Const ("HOL.times",_) $    c $ y ) $z )))) => 
   32.24       let  
   32.25          val m = l div (dest_numeral c) 
   32.26          val n = if (x = y) then abs (m) else 1
   32.27 -        val xtm = (HOLogic.mk_binop "op *" ((mk_numeral ((m div n)*l) ), x)) 
   32.28 +        val xtm = (HOLogic.mk_binop "HOL.times" ((mk_numeral ((m div n)*l) ), x)) 
   32.29          val rs = if (x = y) 
   32.30 -                 then (HOLogic.mk_binrel "op <" (zero,linear_sub [] (mk_numeral n) (HOLogic.mk_binop "op +" ( xtm ,( linear_cmul n z) )))) 
   32.31 +                 then (HOLogic.mk_binrel "op <" (zero,linear_sub [] (mk_numeral n) (HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) )))) 
   32.32                   else HOLogic.mk_binrel "op <" (zero,linear_sub [] one rt )
   32.33          val ck = cterm_of sg (mk_numeral n)
   32.34          val cc = cterm_of sg c
   32.35 @@ -273,14 +273,14 @@
   32.36          in ([], fn [] => [th1,(prove_elementar sg "sa" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
   32.37          end
   32.38  
   32.39 -  |(Const(p,_) $a $( Const ("op +", _)$(Const ("op *",_) $ 
   32.40 +  |(Const(p,_) $a $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $ 
   32.41        c $ y ) $t )) => 
   32.42     if (is_arith_rel fm) andalso (x = y) 
   32.43     then  
   32.44          let val m = l div (dest_numeral c) 
   32.45             val k = (if p = "op <" then abs(m) else m)  
   32.46 -           val xtm = (HOLogic.mk_binop "op *" ((mk_numeral ((m div k)*l) ), x))
   32.47 -           val rs = (HOLogic.mk_binrel p ((linear_cmul k a),(HOLogic.mk_binop "op +" ( xtm ,( linear_cmul k t) )))) 
   32.48 +           val xtm = (HOLogic.mk_binop "HOL.times" ((mk_numeral ((m div k)*l) ), x))
   32.49 +           val rs = (HOLogic.mk_binrel p ((linear_cmul k a),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul k t) )))) 
   32.50  
   32.51             val ck = cterm_of sg (mk_numeral k)
   32.52             val cc = cterm_of sg c
   32.53 @@ -335,28 +335,28 @@
   32.54     val cfalse = cterm_of sg HOLogic.false_const
   32.55     val fm = norm_zero_one fm1
   32.56    in  case fm1 of 
   32.57 -      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
   32.58 +      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) => 
   32.59           if (x=y) andalso (c1= zero) andalso (c2= one) then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_minf))
   32.60             else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
   32.61  
   32.62 -      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
   32.63 +      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
   32.64    	   if (is_arith_rel fm) andalso (x=y) andalso (c1= zero) andalso (c2= one) 
   32.65  	   then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_minf))
   32.66  	 	 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf)) 
   32.67  
   32.68 -      |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
   32.69 +      |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
   32.70             if (y=x) andalso (c1 = zero) then 
   32.71              if (pm1 = one) then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_minf)) else
   32.72  	     (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_minf))
   32.73  	    else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
   32.74    
   32.75 -      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
   32.76 +      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
   32.77           if y=x then  let val cz = cterm_of sg (norm_zero_one z)
   32.78  			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
   32.79  	 	      in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_minf)))
   32.80  		      end
   32.81  		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
   32.82 -      |(Const("Divides.op dvd",_)$ d $ (db as (Const ("op +",_) $ (Const ("op *",_) $
   32.83 +      |(Const("Divides.op dvd",_)$ d $ (db as (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $
   32.84        c $ y ) $ z))) => 
   32.85           if y=x then  let val cz = cterm_of sg (norm_zero_one z)
   32.86  			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
   32.87 @@ -373,22 +373,22 @@
   32.88     let
   32.89     val fm = norm_zero_one fm1
   32.90      in  case fm1 of 
   32.91 -      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
   32.92 +      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) => 
   32.93           if  (x=y) andalso (c1=zero) andalso (c2=one) 
   32.94  	   then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (neq_eq_minf))
   32.95             else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
   32.96  
   32.97 -      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
   32.98 +      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
   32.99    	   if (is_arith_rel fm) andalso (x=y) andalso ((c1=zero) orelse (c1 = norm_zero_one zero)) andalso ((c2=one) orelse (c1 = norm_zero_one one))
  32.100  	     then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (eq_eq_minf))
  32.101  	     else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf)) 
  32.102  
  32.103 -      |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
  32.104 +      |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
  32.105             if (y=x) andalso (c1 =zero) then 
  32.106              if pm1 = one then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (le_eq_minf)) else
  32.107  	     (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (len_eq_minf))
  32.108  	    else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
  32.109 -      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
  32.110 +      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
  32.111           if y=x then  let val cd = cterm_of sg (norm_zero_one d)
  32.112  	 		  val cz = cterm_of sg (norm_zero_one z)
  32.113  	 	      in(instantiate' [] [SOME cd,  SOME cz] (not_dvd_eq_minf)) 
  32.114 @@ -396,7 +396,7 @@
  32.115  
  32.116  		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
  32.117  		
  32.118 -      |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
  32.119 +      |(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
  32.120           if y=x then  let val cd = cterm_of sg (norm_zero_one d)
  32.121  	 		  val cz = cterm_of sg (norm_zero_one z)
  32.122  	 	      in(instantiate' [] [SOME cd, SOME cz ] (dvd_eq_minf))
  32.123 @@ -431,30 +431,30 @@
  32.124    val cfalse = cterm_of sg HOLogic.false_const
  32.125    val fm = norm_zero_one fm1
  32.126   in  case fm1 of 
  32.127 -      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
  32.128 +      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) => 
  32.129           if ((x=y) andalso (c1= zero) andalso (c2= one))
  32.130  	 then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_pinf))
  32.131           else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
  32.132  
  32.133 -      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
  32.134 +      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
  32.135    	if ((is_arith_rel fm) andalso (x = y) andalso (c1 = zero)  andalso (c2 = one)) 
  32.136  	then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_pinf))
  32.137  	else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
  32.138  
  32.139 -      |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
  32.140 +      |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
  32.141          if ((y=x) andalso (c1 = zero)) then 
  32.142            if (pm1 = one) 
  32.143  	  then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_pinf)) 
  32.144  	  else (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_pinf))
  32.145  	else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
  32.146    
  32.147 -      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
  32.148 +      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
  32.149           if y=x then  let val cz = cterm_of sg (norm_zero_one z)
  32.150  			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
  32.151  	 	      in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_pinf)))
  32.152  		      end
  32.153  		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
  32.154 -      |(Const("Divides.op dvd",_)$ d $ (db as (Const ("op +",_) $ (Const ("op *",_) $
  32.155 +      |(Const("Divides.op dvd",_)$ d $ (db as (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $
  32.156        c $ y ) $ z))) => 
  32.157           if y=x then  let val cz = cterm_of sg (norm_zero_one z)
  32.158  			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
  32.159 @@ -472,22 +472,22 @@
  32.160    let
  32.161  					val fm = norm_zero_one fm1
  32.162      in  case fm1 of 
  32.163 -      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
  32.164 +      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) => 
  32.165           if  (x=y) andalso (c1=zero) andalso (c2=one) 
  32.166  	   then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (neq_eq_pinf))
  32.167             else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
  32.168  
  32.169 -      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
  32.170 +      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
  32.171    	   if (is_arith_rel fm) andalso (x=y) andalso ((c1=zero) orelse (c1 = norm_zero_one zero)) andalso ((c2=one) orelse (c1 = norm_zero_one one))
  32.172  	     then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (eq_eq_pinf))
  32.173  	     else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf)) 
  32.174  
  32.175 -      |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
  32.176 +      |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
  32.177             if (y=x) andalso (c1 =zero) then 
  32.178              if pm1 = one then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (le_eq_pinf)) else
  32.179  	     (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (len_eq_pinf))
  32.180  	    else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
  32.181 -      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
  32.182 +      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
  32.183           if y=x then  let val cd = cterm_of sg (norm_zero_one d)
  32.184  	 		  val cz = cterm_of sg (norm_zero_one z)
  32.185  	 	      in(instantiate' [] [SOME cd,  SOME cz] (not_dvd_eq_pinf)) 
  32.186 @@ -495,7 +495,7 @@
  32.187  
  32.188  		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
  32.189  		
  32.190 -      |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
  32.191 +      |(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
  32.192           if y=x then  let val cd = cterm_of sg (norm_zero_one d)
  32.193  	 		  val cz = cterm_of sg (norm_zero_one z)
  32.194  	 	      in(instantiate' [] [SOME cd, SOME cz ] (dvd_eq_pinf))
  32.195 @@ -567,31 +567,31 @@
  32.196      val cat = cterm_of sg (norm_zero_one at)
  32.197    in
  32.198    case at of 
  32.199 -   (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
  32.200 +   (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) => 
  32.201        if  (x=y) andalso (c1=zero) andalso (c2=one) 
  32.202  	 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)
  32.203 -	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one  z)))
  32.204 +	          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)))
  32.205  		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
  32.206  	 in  (instantiate' [] [SOME cfma]([th3,th1,th2] MRS (not_bst_p_ne)))
  32.207  	 end
  32.208           else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
  32.209  
  32.210 -   |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", T) $(Const ("op *",_) $ c2 $ y) $z)) =>
  32.211 +   |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", T) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
  32.212       if (is_arith_rel at) andalso (x=y)
  32.213  	then let val bst_z = norm_zero_one (linear_neg (linear_add [] z (mk_numeral 1)))
  32.214  	         in let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ bst_z $ B)
  32.215 -	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq (bst_z,Const("op -",T) $ (Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("1",HOLogic.intT))))
  32.216 +	          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))))
  32.217  		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
  32.218  	 in  (instantiate' [] [SOME cfma] ([th3,th1,th2] MRS (not_bst_p_eq)))
  32.219  	 end
  32.220         end
  32.221           else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
  32.222  
  32.223 -   |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
  32.224 +   |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
  32.225          if (y=x) andalso (c1 =zero) then 
  32.226          if pm1 = one then 
  32.227  	  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)
  32.228 -              val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
  32.229 +              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)))
  32.230  	  in  (instantiate' [] [SOME cfma,  SOME cdlcm]([th1,th2] MRS (not_bst_p_gt)))
  32.231  	    end
  32.232  	 else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
  32.233 @@ -599,7 +599,7 @@
  32.234  	      end
  32.235        else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
  32.236  
  32.237 -   |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
  32.238 +   |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
  32.239        if y=x then  
  32.240             let val cz = cterm_of sg (norm_zero_one z)
  32.241  	       val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
  32.242 @@ -607,7 +607,7 @@
  32.243  	     end
  32.244        else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
  32.245  
  32.246 -   |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
  32.247 +   |(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
  32.248         if y=x then  
  32.249  	 let val cz = cterm_of sg (norm_zero_one z)
  32.250  	     val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
  32.251 @@ -658,26 +658,26 @@
  32.252      val cat = cterm_of sg (norm_zero_one at)
  32.253    in
  32.254    case at of 
  32.255 -   (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
  32.256 +   (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) => 
  32.257        if  (x=y) andalso (c1=zero) andalso (c2=one) 
  32.258  	 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)
  32.259 -	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one  z)))
  32.260 +	          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)))
  32.261  		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
  32.262  	 in  (instantiate' [] [SOME cfma]([th3,th1,th2] MRS (not_ast_p_ne)))
  32.263  	 end
  32.264           else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
  32.265  
  32.266 -   |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", T) $(Const ("op *",_) $ c2 $ y) $z)) =>
  32.267 +   |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", T) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
  32.268       if (is_arith_rel at) andalso (x=y)
  32.269  	then let val ast_z = norm_zero_one (linear_sub [] one z )
  32.270  	         val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ ast_z $ A)
  32.271 -	         val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq (ast_z,Const("op +",T) $ (Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("1",HOLogic.intT))))
  32.272 +	         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))))
  32.273  		 val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
  32.274  	 in  (instantiate' [] [SOME cfma] ([th3,th1,th2] MRS (not_ast_p_eq)))
  32.275         end
  32.276           else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
  32.277  
  32.278 -   |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
  32.279 +   |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
  32.280          if (y=x) andalso (c1 =zero) then 
  32.281          if pm1 = (mk_numeral ~1) then 
  32.282  	  let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one z) $ A)
  32.283 @@ -689,7 +689,7 @@
  32.284  	      end
  32.285        else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
  32.286  
  32.287 -   |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
  32.288 +   |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
  32.289        if y=x then  
  32.290             let val cz = cterm_of sg (norm_zero_one z)
  32.291  	       val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
  32.292 @@ -697,7 +697,7 @@
  32.293  	     end
  32.294        else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
  32.295  
  32.296 -   |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
  32.297 +   |(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
  32.298         if y=x then  
  32.299  	 let val cz = cterm_of sg (norm_zero_one z)
  32.300  	     val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
    33.1 --- a/src/HOL/Tools/Presburger/presburger.ML	Fri Mar 10 12:28:38 2006 +0100
    33.2 +++ b/src/HOL/Tools/Presburger/presburger.ML	Fri Mar 10 15:33:48 2006 +0100
    33.3 @@ -139,11 +139,11 @@
    33.4     ("Divides.op dvd", iT --> iT --> bT),
    33.5     ("Divides.op div", iT --> iT --> iT),
    33.6     ("Divides.op mod", iT --> iT --> iT),
    33.7 -   ("op +", iT --> iT --> iT),
    33.8 -   ("op -", iT --> iT --> iT),
    33.9 -   ("op *", iT --> iT --> iT), 
   33.10 +   ("HOL.plus", iT --> iT --> iT),
   33.11 +   ("HOL.minus", iT --> iT --> iT),
   33.12 +   ("HOL.times", iT --> iT --> iT), 
   33.13     ("HOL.abs", iT --> iT),
   33.14 -   ("uminus", iT --> iT),
   33.15 +   ("HOL.uminus", iT --> iT),
   33.16     ("HOL.max", iT --> iT --> iT),
   33.17     ("HOL.min", iT --> iT --> iT),
   33.18  
   33.19 @@ -153,9 +153,9 @@
   33.20     ("Divides.op dvd", nT --> nT --> bT),
   33.21     ("Divides.op div", nT --> nT --> nT),
   33.22     ("Divides.op mod", nT --> nT --> nT),
   33.23 -   ("op +", nT --> nT --> nT),
   33.24 -   ("op -", nT --> nT --> nT),
   33.25 -   ("op *", nT --> nT --> nT), 
   33.26 +   ("HOL.plus", nT --> nT --> nT),
   33.27 +   ("HOL.minus", nT --> nT --> nT),
   33.28 +   ("HOL.times", nT --> nT --> nT), 
   33.29     ("Suc", nT --> nT),
   33.30     ("HOL.max", nT --> nT --> nT),
   33.31     ("HOL.min", nT --> nT --> nT),
    34.1 --- a/src/HOL/Tools/Presburger/reflected_cooper.ML	Fri Mar 10 12:28:38 2006 +0100
    34.2 +++ b/src/HOL/Tools/Presburger/reflected_cooper.ML	Fri Mar 10 15:33:48 2006 +0100
    34.3 @@ -16,10 +16,10 @@
    34.4        | Const("0",iT) => Cst 0
    34.5        | Const("1",iT) => Cst 1
    34.6        | Bound i => Var (nat (IntInf.fromInt i))
    34.7 -      | Const("uminus",_)$t' => Neg (i_of_term vs t')
    34.8 -      | Const ("op +",_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
    34.9 -      | Const ("op -",_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
   34.10 -      | Const ("op *",_)$t1$t2 => Mult (i_of_term vs t1,i_of_term vs t2)
   34.11 +      | Const("HOL.uminus",_)$t' => Neg (i_of_term vs t')
   34.12 +      | Const ("HOL.plus",_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
   34.13 +      | Const ("HOL.minus",_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
   34.14 +      | Const ("HOL.times",_)$t1$t2 => Mult (i_of_term vs t1,i_of_term vs t2)
   34.15        | Const ("Numeral.number_of",_)$t' => Cst (HOLogic.dest_binum t')
   34.16        | _ => error "i_of_term: unknown term";
   34.17  	
   34.18 @@ -77,12 +77,12 @@
   34.19      case t of 
   34.20  	Cst i => CooperDec.mk_numeral i
   34.21        | Var n => valOf (myassoc2 vs n)
   34.22 -      | Neg t' => Const("uminus",iT --> iT)$(term_of_i vs t')
   34.23 -      | Add(t1,t2) => Const("op +",[iT,iT] ---> iT)$
   34.24 +      | Neg t' => Const("HOL.uminus",iT --> iT)$(term_of_i vs t')
   34.25 +      | Add(t1,t2) => Const("HOL.plus",[iT,iT] ---> iT)$
   34.26  			   (term_of_i vs t1)$(term_of_i vs t2)
   34.27 -      | Sub(t1,t2) => Const("op -",[iT,iT] ---> iT)$
   34.28 +      | Sub(t1,t2) => Const("HOL.minus",[iT,iT] ---> iT)$
   34.29  			   (term_of_i vs t1)$(term_of_i vs t2)
   34.30 -      | Mult(t1,t2) => Const("op *",[iT,iT] ---> iT)$
   34.31 +      | Mult(t1,t2) => Const("HOL.times",[iT,iT] ---> iT)$
   34.32  			   (term_of_i vs t1)$(term_of_i vs t2);
   34.33  
   34.34  fun term_of_qf vs t = 
    35.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Fri Mar 10 12:28:38 2006 +0100
    35.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Fri Mar 10 15:33:48 2006 +0100
    35.3 @@ -404,7 +404,7 @@
    35.4      val def_names = map (fn s => s ^ "_def") (DatatypeProp.indexify_names
    35.5        (map (fn T => name_of_typ T ^ "_size") recTs));
    35.6  
    35.7 -    fun plus (t1, t2) = Const ("op +", [HOLogic.natT, HOLogic.natT] ---> HOLogic.natT) $ t1 $ t2;
    35.8 +    fun plus (t1, t2) = Const ("HOL.plus", [HOLogic.natT, HOLogic.natT] ---> HOLogic.natT) $ t1 $ t2;
    35.9  
   35.10      fun make_sizefun (_, cargs) =
   35.11        let
    36.1 --- a/src/HOL/Tools/datatype_prop.ML	Fri Mar 10 12:28:38 2006 +0100
    36.2 +++ b/src/HOL/Tools/datatype_prop.ML	Fri Mar 10 15:33:48 2006 +0100
    36.3 @@ -366,7 +366,7 @@
    36.4      val size_consts = map (fn (s, T) =>
    36.5        Const (s, T --> HOLogic.natT)) (size_names ~~ recTs);
    36.6  
    36.7 -    fun plus (t1, t2) = Const ("op +", [HOLogic.natT, HOLogic.natT] ---> HOLogic.natT) $ t1 $ t2;
    36.8 +    fun plus (t1, t2) = Const ("HOL.plus", [HOLogic.natT, HOLogic.natT] ---> HOLogic.natT) $ t1 $ t2;
    36.9  
   36.10      fun make_size_eqn size_const T (cname, cargs) =
   36.11        let
    37.1 --- a/src/HOL/Tools/refute.ML	Fri Mar 10 12:28:38 2006 +0100
    37.2 +++ b/src/HOL/Tools/refute.ML	Fri Mar 10 15:33:48 2006 +0100
    37.3 @@ -622,9 +622,9 @@
    37.4  			| Const ("Finite_Set.card", T)    => collect_type_axioms (axs, T)
    37.5  			| Const ("Finite_Set.Finites", T) => collect_type_axioms (axs, T)
    37.6  			| Const ("op <", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => collect_type_axioms (axs, T)
    37.7 -			| Const ("op +", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T)
    37.8 -			| Const ("op -", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T)
    37.9 -			| Const ("op *", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T)
   37.10 +			| Const ("HOL.plus", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T)
   37.11 +			| Const ("HOL.minus", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T)
   37.12 +			| Const ("HOL.times", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T)
   37.13  			| Const ("List.op @", T)          => collect_type_axioms (axs, T)
   37.14  			| Const ("Lfp.lfp", T)            => collect_type_axioms (axs, T)
   37.15  			| Const ("Gfp.gfp", T)            => collect_type_axioms (axs, T)
   37.16 @@ -2162,13 +2162,13 @@
   37.17  
   37.18  	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
   37.19  
   37.20 -	(* only an optimization: 'op +' could in principle be interpreted with    *)
   37.21 +	(* only an optimization: 'HOL.plus' could in principle be interpreted with*)
   37.22  	(* interpreters available already (using its definition), but the code    *)
   37.23  	(* below is more efficient                                                *)
   37.24  
   37.25  	fun Nat_plus_interpreter thy model args t =
   37.26  		case t of
   37.27 -		  Const ("op +", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
   37.28 +		  Const ("HOL.plus", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
   37.29  			let
   37.30  				val (i_nat, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type ("nat", [])))
   37.31  				val size_nat      = size_of_type i_nat
   37.32 @@ -2196,7 +2196,7 @@
   37.33  
   37.34  	fun Nat_minus_interpreter thy model args t =
   37.35  		case t of
   37.36 -		  Const ("op -", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
   37.37 +		  Const ("HOL.minus", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
   37.38  			let
   37.39  				val (i_nat, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type ("nat", [])))
   37.40  				val size_nat      = size_of_type i_nat
   37.41 @@ -2215,13 +2215,13 @@
   37.42  
   37.43  	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
   37.44  
   37.45 -	(* only an optimization: 'op *' could in principle be interpreted with    *)
   37.46 -	(* interpreters available already (using its definition), but the code    *)
   37.47 -	(* below is more efficient                                                *)
   37.48 +	(* only an optimization: 'HOL.times' could in principle be interpreted with *)
   37.49 +	(* interpreters available already (using its definition), but the code      *)
   37.50 +	(* below is more efficient                                                  *)
   37.51  
   37.52  	fun Nat_mult_interpreter thy model args t =
   37.53  		case t of
   37.54 -		  Const ("op *", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
   37.55 +		  Const ("HOL.times", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
   37.56  			let
   37.57  				val (i_nat, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type ("nat", [])))
   37.58  				val size_nat      = size_of_type i_nat
    38.1 --- a/src/HOL/Tools/res_clause.ML	Fri Mar 10 12:28:38 2006 +0100
    38.2 +++ b/src/HOL/Tools/res_clause.ML	Fri Mar 10 15:33:48 2006 +0100
    38.3 @@ -94,9 +94,9 @@
    38.4  		   ("op <", "less"),
    38.5  		   ("op &", "and"),
    38.6  		   ("op |", "or"),
    38.7 -		   ("op +", "plus"),
    38.8 -		   ("op -", "minus"),
    38.9 -		   ("op *", "times"),
   38.10 +		   ("HOL.plus", "plus"),
   38.11 +		   ("HOL.minus", "minus"),
   38.12 +		   ("HOL.times", "times"),
   38.13  		   ("Divides.op div", "div"),
   38.14  		   ("HOL.divide", "divide"),
   38.15  		   ("op -->", "implies"),
    39.1 --- a/src/HOL/arith_data.ML	Fri Mar 10 12:28:38 2006 +0100
    39.2 +++ b/src/HOL/arith_data.ML	Fri Mar 10 15:33:48 2006 +0100
    39.3 @@ -17,7 +17,7 @@
    39.4  (* mk_sum, mk_norm_sum *)
    39.5  
    39.6  val one = HOLogic.mk_nat 1;
    39.7 -val mk_plus = HOLogic.mk_binop "op +";
    39.8 +val mk_plus = HOLogic.mk_binop "HOL.plus";
    39.9  
   39.10  fun mk_sum [] = HOLogic.zero
   39.11    | mk_sum [t] = t
   39.12 @@ -32,7 +32,7 @@
   39.13  
   39.14  (* dest_sum *)
   39.15  
   39.16 -val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT;
   39.17 +val dest_plus = HOLogic.dest_bin "HOL.plus" HOLogic.natT;
   39.18  
   39.19  fun dest_sum tm =
   39.20    if HOLogic.is_zero tm then []
   39.21 @@ -137,8 +137,8 @@
   39.22  structure DiffCancelSums = CancelSumsFun
   39.23  (struct
   39.24    open Sum;
   39.25 -  val mk_bal = HOLogic.mk_binop "op -";
   39.26 -  val dest_bal = HOLogic.dest_bin "op -" HOLogic.natT;
   39.27 +  val mk_bal = HOLogic.mk_binop "HOL.minus";
   39.28 +  val dest_bal = HOLogic.dest_bin "HOL.minus" HOLogic.natT;
   39.29    val uncancel_tac = gen_uncancel_tac diff_cancel;
   39.30  end);
   39.31  
   39.32 @@ -267,14 +267,14 @@
   39.33  
   39.34  fun demult inj_consts =
   39.35  let
   39.36 -fun demult((mC as Const("op *",_)) $ s $ t,m) = ((case s of
   39.37 +fun demult((mC as Const("HOL.times",_)) $ s $ t,m) = ((case s of
   39.38          Const("Numeral.number_of",_)$n
   39.39          => demult(t,Rat.mult(m,Rat.rat_of_intinf(HOLogic.dest_binum n)))
   39.40 -      | Const("uminus",_)$(Const("Numeral.number_of",_)$n)
   39.41 +      | Const("HOL.uminus",_)$(Const("Numeral.number_of",_)$n)
   39.42          => demult(t,Rat.mult(m,Rat.rat_of_intinf(~(HOLogic.dest_binum n))))
   39.43        | Const("Suc",_) $ _
   39.44          => demult(t,Rat.mult(m,Rat.rat_of_int(number_of_Sucs s)))
   39.45 -      | Const("op *",_) $ s1 $ s2 => demult(mC $ s1 $ (mC $ s2 $ t),m)
   39.46 +      | Const("HOL.times",_) $ s1 $ s2 => demult(mC $ s1 $ (mC $ s2 $ t),m)
   39.47        | Const("HOL.divide",_) $ numt $ (Const("Numeral.number_of",_)$dent) =>
   39.48            let val den = HOLogic.dest_binum dent
   39.49            in if den = 0 then raise Zero
   39.50 @@ -291,7 +291,7 @@
   39.51    | demult(t as Const("Numeral.number_of",_)$n,m) =
   39.52        ((NONE,Rat.mult(m,Rat.rat_of_intinf(HOLogic.dest_binum n)))
   39.53         handle TERM _ => (SOME t,m))
   39.54 -  | demult(Const("uminus",_)$t, m) = demult(t,Rat.mult(m,Rat.rat_of_int(~1)))
   39.55 +  | demult(Const("HOL.uminus",_)$t, m) = demult(t,Rat.mult(m,Rat.rat_of_int(~1)))
   39.56    | demult(t as Const f $ x, m) =
   39.57        (if f mem inj_consts then SOME x else SOME t,m)
   39.58    | demult(atom,m) = (SOME atom,m)
   39.59 @@ -303,15 +303,15 @@
   39.60  fun decomp2 inj_consts (rel,lhs,rhs) =
   39.61  let
   39.62  (* Turn term into list of summand * multiplicity plus a constant *)
   39.63 -fun poly(Const("op +",_) $ s $ t, m, pi) = poly(s,m,poly(t,m,pi))
   39.64 -  | poly(all as Const("op -",T) $ s $ t, m, pi) =
   39.65 +fun poly(Const("HOL.plus",_) $ s $ t, m, pi) = poly(s,m,poly(t,m,pi))
   39.66 +  | poly(all as Const("HOL.minus",T) $ s $ t, m, pi) =
   39.67        if nT T then add_atom(all,m,pi) else poly(s,m,poly(t,Rat.neg m,pi))
   39.68 -  | poly(all as Const("uminus",T) $ t, m, pi) =
   39.69 +  | poly(all as Const("HOL.uminus",T) $ t, m, pi) =
   39.70        if nT T then add_atom(all,m,pi) else poly(t,Rat.neg m,pi)
   39.71    | poly(Const("0",_), _, pi) = pi
   39.72    | poly(Const("1",_), m, (p,i)) = (p,Rat.add(i,m))
   39.73    | poly(Const("Suc",_)$t, m, (p,i)) = poly(t, m, (p,Rat.add(i,m)))
   39.74 -  | poly(t as Const("op *",_) $ _ $ _, m, pi as (p,i)) =
   39.75 +  | poly(t as Const("HOL.times",_) $ _ $ _, m, pi as (p,i)) =
   39.76        (case demult inj_consts (t,m) of
   39.77           (NONE,m') => (p,Rat.add(i,m))
   39.78         | (SOME u,m') => add_atom(u,m',pi))
    40.1 --- a/src/HOL/ex/SVC_Oracle.ML	Fri Mar 10 12:28:38 2006 +0100
    40.2 +++ b/src/HOL/ex/SVC_Oracle.ML	Fri Mar 10 15:33:48 2006 +0100
    40.3 @@ -46,21 +46,21 @@
    40.4        | lit (t as Const("Numeral.number_of", _) $ w) = t
    40.5        | lit t = replace t
    40.6      (*abstraction of a real/rational expression*)
    40.7 -    fun rat ((c as Const("op +", _)) $ x $ y) = c $ (rat x) $ (rat y)
    40.8 -      | rat ((c as Const("op -", _)) $ x $ y) = c $ (rat x) $ (rat y)
    40.9 -      | rat ((c as Const("op /", _)) $ x $ y) = c $ (rat x) $ (rat y)
   40.10 -      | rat ((c as Const("op *", _)) $ x $ y) = c $ (rat x) $ (rat y)
   40.11 -      | rat ((c as Const("uminus", _)) $ x) = c $ (rat x)
   40.12 +    fun rat ((c as Const("HOL.plus", _)) $ x $ y) = c $ (rat x) $ (rat y)
   40.13 +      | rat ((c as Const("HOL.minus", _)) $ x $ y) = c $ (rat x) $ (rat y)
   40.14 +      | rat ((c as Const("HOL.divide", _)) $ x $ y) = c $ (rat x) $ (rat y)
   40.15 +      | rat ((c as Const("HOL.times", _)) $ x $ y) = c $ (rat x) $ (rat y)
   40.16 +      | rat ((c as Const("HOL.uminus", _)) $ x) = c $ (rat x)
   40.17        | rat t = lit t
   40.18      (*abstraction of an integer expression: no div, mod*)
   40.19 -    fun int ((c as Const("op +", _)) $ x $ y) = c $ (int x) $ (int y)
   40.20 -      | int ((c as Const("op -", _)) $ x $ y) = c $ (int x) $ (int y)
   40.21 -      | int ((c as Const("op *", _)) $ x $ y) = c $ (int x) $ (int y)
   40.22 -      | int ((c as Const("uminus", _)) $ x) = c $ (int x)
   40.23 +    fun int ((c as Const("HOL.plus", _)) $ x $ y) = c $ (int x) $ (int y)
   40.24 +      | int ((c as Const("HOL.minus", _)) $ x $ y) = c $ (int x) $ (int y)
   40.25 +      | int ((c as Const("HOL.times", _)) $ x $ y) = c $ (int x) $ (int y)
   40.26 +      | int ((c as Const("HOL.uminus", _)) $ x) = c $ (int x)
   40.27        | int t = lit t
   40.28      (*abstraction of a natural number expression: no minus*)
   40.29 -    fun nat ((c as Const("op +", _)) $ x $ y) = c $ (nat x) $ (nat y)
   40.30 -      | nat ((c as Const("op *", _)) $ x $ y) = c $ (nat x) $ (nat y)
   40.31 +    fun nat ((c as Const("HOL.plus", _)) $ x $ y) = c $ (nat x) $ (nat y)
   40.32 +      | nat ((c as Const("HOL.times", _)) $ x $ y) = c $ (nat x) $ (nat y)
   40.33        | nat ((c as Const("Suc", _)) $ x) = c $ (nat x)
   40.34        | nat t = lit t
   40.35      (*abstraction of a relation: =, <, <=*)
    41.1 --- a/src/HOL/ex/mesontest2.ML	Fri Mar 10 12:28:38 2006 +0100
    41.2 +++ b/src/HOL/ex/mesontest2.ML	Fri Mar 10 15:33:48 2006 +0100
    41.3 @@ -547,9 +547,9 @@
    41.4  \  (has(p4::'a,goto(out))) &        \
    41.5  \  (follows(p5::'a,p4)) &   \
    41.6  \  (follows(p6::'a,p3)) &   \
    41.7 -\  (has(p6::'a,assign(register_k::'a,times(num2::'a,register_k)))) &   \
    41.8 +\  (has(p6::'a,assign(register_k::'a,mtimes(num2::'a,register_k)))) &   \
    41.9  \  (follows(p7::'a,p6)) &   \
   41.10 -\  (has(p7::'a,assign(register_j::'a,plus(register_j::'a,num1)))) &    \
   41.11 +\  (has(p7::'a,assign(register_j::'a,mplus(register_j::'a,num1)))) &    \
   41.12  \  (follows(p8::'a,p7)) &   \
   41.13  \  (has(p8::'a,goto(loop))) &       \
   41.14  \  (~succeeds(p3::'a,p3)) --> False",
   41.15 @@ -570,9 +570,9 @@
   41.16  \  (has(p4::'a,goto(out))) &        \
   41.17  \  (follows(p5::'a,p4)) &   \
   41.18  \  (follows(p6::'a,p3)) &   \
   41.19 -\  (has(p6::'a,assign(register_k::'a,times(num2::'a,register_k)))) &   \
   41.20 +\  (has(p6::'a,assign(register_k::'a,mtimes(num2::'a,register_k)))) &   \
   41.21  \  (follows(p7::'a,p6)) &   \
   41.22 -\  (has(p7::'a,assign(register_j::'a,plus(register_j::'a,num1)))) &    \
   41.23 +\  (has(p7::'a,assign(register_j::'a,mplus(register_j::'a,num1)))) &    \
   41.24  \  (follows(p8::'a,p7)) &   \
   41.25  \  (has(p8::'a,goto(loop))) &       \
   41.26  \  (fails(p3::'a,p3)) --> False",
   41.27 @@ -768,7 +768,6 @@
   41.28  \  (\\<forall>X V1 V2 V3 V4 Y V5. equal(X::'a,Y) --> equal(continuous(V1::'a,V2,V3,V4,X,V5),continuous(V1::'a,V2,V3,V4,Y,V5))) &    \
   41.29  \  (\\<forall>X V1 V2 V3 V4 V5 Y. equal(X::'a,Y) --> equal(continuous(V1::'a,V2,V3,V4,V5,X),continuous(V1::'a,V2,V3,V4,V5,Y)))";
   41.30  
   41.31 -
   41.32  (*4272 inferences so far.  Searching to depth 10.  29.4 secs*)
   41.33  val GEO017_2 = prove_hard
   41.34   (EQU001_0_ax ^ "&" ^ GEO002_ax_eq ^ "  &    \
   41.35 @@ -1224,26 +1223,26 @@
   41.36  
   41.37  (*73 inferences so far.  Searching to depth 10.  0.2 secs*)
   41.38  val MSC003_1 = prove
   41.39 - ("(\\<forall>Number_of_small_parts Small_part Big_part Number_of_mid_parts Mid_part. has_parts(Big_part::'a,Number_of_mid_parts,Mid_part) --> in'(object_in(Big_part::'a,Mid_part,Small_part,Number_of_mid_parts,Number_of_small_parts),Mid_part) | has_parts(Big_part::'a,times(Number_of_mid_parts::'a,Number_of_small_parts),Small_part)) &        \
   41.40 -\  (\\<forall>Big_part Mid_part Number_of_mid_parts Number_of_small_parts Small_part. has_parts(Big_part::'a,Number_of_mid_parts,Mid_part) & has_parts(object_in(Big_part::'a,Mid_part,Small_part,Number_of_mid_parts,Number_of_small_parts),Number_of_small_parts,Small_part) --> has_parts(Big_part::'a,times(Number_of_mid_parts::'a,Number_of_small_parts),Small_part)) &   \
   41.41 + ("(\\<forall>Number_of_small_parts Small_part Big_part Number_of_mid_parts Mid_part. has_parts(Big_part::'a,Number_of_mid_parts,Mid_part) --> in'(object_in(Big_part::'a,Mid_part,Small_part,Number_of_mid_parts,Number_of_small_parts),Mid_part) | has_parts(Big_part::'a,mtimes(Number_of_mid_parts::'a,Number_of_small_parts),Small_part)) &        \
   41.42 +\  (\\<forall>Big_part Mid_part Number_of_mid_parts Number_of_small_parts Small_part. has_parts(Big_part::'a,Number_of_mid_parts,Mid_part) & has_parts(object_in(Big_part::'a,Mid_part,Small_part,Number_of_mid_parts,Number_of_small_parts),Number_of_small_parts,Small_part) --> has_parts(Big_part::'a,mtimes(Number_of_mid_parts::'a,Number_of_small_parts),Small_part)) &   \
   41.43  \  (in'(john::'a,boy)) &    \
   41.44  \  (\\<forall>X. in'(X::'a,boy) --> in'(X::'a,human)) & \
   41.45  \  (\\<forall>X. in'(X::'a,hand) --> has_parts(X::'a,num5,fingers)) &      \
   41.46  \  (\\<forall>X. in'(X::'a,human) --> has_parts(X::'a,num2,arm)) & \
   41.47  \  (\\<forall>X. in'(X::'a,arm) --> has_parts(X::'a,num1,hand)) &  \
   41.48 -\  (~has_parts(john::'a,times(num2::'a,num1),hand)) --> False",
   41.49 +\  (~has_parts(john::'a,mtimes(num2::'a,num1),hand)) --> False",
   41.50    meson_tac 1);
   41.51  
   41.52  (*1486 inferences so far.  Searching to depth 20.  1.2 secs*)
   41.53  val MSC004_1 = prove
   41.54 - ("(\\<forall>Number_of_small_parts Small_part Big_part Number_of_mid_parts Mid_part. has_parts(Big_part::'a,Number_of_mid_parts,Mid_part) --> in'(object_in(Big_part::'a,Mid_part,Small_part,Number_of_mid_parts,Number_of_small_parts),Mid_part) | has_parts(Big_part::'a,times(Number_of_mid_parts::'a,Number_of_small_parts),Small_part)) &        \
   41.55 -\  (\\<forall>Big_part Mid_part Number_of_mid_parts Number_of_small_parts Small_part. has_parts(Big_part::'a,Number_of_mid_parts,Mid_part) & has_parts(object_in(Big_part::'a,Mid_part,Small_part,Number_of_mid_parts,Number_of_small_parts),Number_of_small_parts,Small_part) --> has_parts(Big_part::'a,times(Number_of_mid_parts::'a,Number_of_small_parts),Small_part)) &   \
   41.56 + ("(\\<forall>Number_of_small_parts Small_part Big_part Number_of_mid_parts Mid_part. has_parts(Big_part::'a,Number_of_mid_parts,Mid_part) --> in'(object_in(Big_part::'a,Mid_part,Small_part,Number_of_mid_parts,Number_of_small_parts),Mid_part) | has_parts(Big_part::'a,mtimes(Number_of_mid_parts::'a,Number_of_small_parts),Small_part)) &        \
   41.57 +\  (\\<forall>Big_part Mid_part Number_of_mid_parts Number_of_small_parts Small_part. has_parts(Big_part::'a,Number_of_mid_parts,Mid_part) & has_parts(object_in(Big_part::'a,Mid_part,Small_part,Number_of_mid_parts,Number_of_small_parts),Number_of_small_parts,Small_part) --> has_parts(Big_part::'a,mtimes(Number_of_mid_parts::'a,Number_of_small_parts),Small_part)) &   \
   41.58  \  (in'(john::'a,boy)) &    \
   41.59  \  (\\<forall>X. in'(X::'a,boy) --> in'(X::'a,human)) & \
   41.60  \  (\\<forall>X. in'(X::'a,hand) --> has_parts(X::'a,num5,fingers)) &      \
   41.61  \  (\\<forall>X. in'(X::'a,human) --> has_parts(X::'a,num2,arm)) & \
   41.62  \  (\\<forall>X. in'(X::'a,arm) --> has_parts(X::'a,num1,hand)) &  \
   41.63 -\  (~has_parts(john::'a,times(times(num2::'a,num1),num5),fingers)) --> False",
   41.64 +\  (~has_parts(john::'a,mtimes(mtimes(num2::'a,num1),num5),fingers)) --> False",
   41.65    meson_tac 1);
   41.66  
   41.67  (*100 inferences so far.  Searching to depth 12.  0.1 secs*)
    42.1 --- a/src/HOL/ex/svc_funcs.ML	Fri Mar 10 12:28:38 2006 +0100
    42.2 +++ b/src/HOL/ex/svc_funcs.ML	Fri Mar 10 15:33:48 2006 +0100
    42.3 @@ -154,16 +154,16 @@
    42.4        | lit (Const("0", _)) = 0
    42.5        | lit (Const("1", _)) = 1
    42.6      (*translation of a literal expression [no variables]*)
    42.7 -    fun litExp (Const("op +", T) $ x $ y) =
    42.8 +    fun litExp (Const("HOL.plus", T) $ x $ y) =
    42.9            if is_numeric_op T then (litExp x) + (litExp y)
   42.10            else fail t
   42.11 -      | litExp (Const("op -", T) $ x $ y) =
   42.12 +      | litExp (Const("HOL.minus", T) $ x $ y) =
   42.13            if is_numeric_op T then (litExp x) - (litExp y)
   42.14            else fail t
   42.15 -      | litExp (Const("op *", T) $ x $ y) =
   42.16 +      | litExp (Const("HOL.times", T) $ x $ y) =
   42.17            if is_numeric_op T then (litExp x) * (litExp y)
   42.18            else fail t
   42.19 -      | litExp (Const("uminus", T) $ x)   =
   42.20 +      | litExp (Const("HOL.uminus", T) $ x)   =
   42.21            if is_numeric_op T then ~(litExp x)
   42.22            else fail t
   42.23        | litExp t = lit t
   42.24 @@ -171,21 +171,21 @@
   42.25      (*translation of a real/rational expression*)
   42.26      fun suc t = Interp("+", [Int 1, t])
   42.27      fun tm (Const("Suc", T) $ x) = suc (tm x)
   42.28 -      | tm (Const("op +", T) $ x $ y) =
   42.29 +      | tm (Const("HOL.plus", T) $ x $ y) =
   42.30            if is_numeric_op T then Interp("+", [tm x, tm y])
   42.31            else fail t
   42.32 -      | tm (Const("op -", T) $ x $ y) =
   42.33 +      | tm (Const("HOL.minus", T) $ x $ y) =
   42.34            if is_numeric_op T then
   42.35                Interp("+", [tm x, Interp("*", [Int ~1, tm y])])
   42.36            else fail t
   42.37 -      | tm (Const("op *", T) $ x $ y) =
   42.38 +      | tm (Const("HOL.times", T) $ x $ y) =
   42.39            if is_numeric_op T then Interp("*", [tm x, tm y])
   42.40            else fail t
   42.41        | tm (Const("RealDef.rinv", T) $ x) =
   42.42            if domain_type T = HOLogic.realT then
   42.43                Rat(1, litExp x)
   42.44            else fail t
   42.45 -      | tm (Const("uminus", T) $ x) =
   42.46 +      | tm (Const("HOL.uminus", T) $ x) =
   42.47            if is_numeric_op T then Interp("*", [Int ~1, tm x])
   42.48            else fail t
   42.49        | tm t = Int (lit t)
    43.1 --- a/src/Provers/Arith/abel_cancel.ML	Fri Mar 10 12:28:38 2006 +0100
    43.2 +++ b/src/Provers/Arith/abel_cancel.ML	Fri Mar 10 15:33:48 2006 +0100
    43.3 @@ -31,28 +31,28 @@
    43.4  open Data;
    43.5  
    43.6   fun zero t = Const ("0", t);
    43.7 - fun minus t = Const ("uminus", t --> t);
    43.8 + fun minus t = Const ("HOL.uminus", t --> t);
    43.9  
   43.10 - fun add_terms pos (Const ("op +", _) $ x $ y, ts) =
   43.11 + fun add_terms pos (Const ("HOL.plus", _) $ x $ y, ts) =
   43.12           add_terms pos (x, add_terms pos (y, ts))
   43.13 -   | add_terms pos (Const ("op -", _) $ x $ y, ts) =
   43.14 +   | add_terms pos (Const ("HOL.minus", _) $ x $ y, ts) =
   43.15           add_terms pos (x, add_terms (not pos) (y, ts))
   43.16 -   | add_terms pos (Const ("uminus", _) $ x, ts) =
   43.17 +   | add_terms pos (Const ("HOL.uminus", _) $ x, ts) =
   43.18           add_terms (not pos) (x, ts)
   43.19     | add_terms pos (x, ts) = (pos,x) :: ts;
   43.20  
   43.21   fun terms fml = add_terms true (fml, []);
   43.22  
   43.23 -fun zero1 pt (u as (c as Const("op +",_)) $ x $ y) =
   43.24 +fun zero1 pt (u as (c as Const("HOL.plus",_)) $ x $ y) =
   43.25        (case zero1 pt x of NONE => (case zero1 pt y of NONE => NONE
   43.26                                     | SOME z => SOME(c $ x $ z))
   43.27         | SOME z => SOME(c $ z $ y))
   43.28 -  | zero1 (pos,t) (u as (c as Const("op -",_)) $ x $ y) =
   43.29 +  | zero1 (pos,t) (u as (c as Const("HOL.minus",_)) $ x $ y) =
   43.30        (case zero1 (pos,t) x of
   43.31           NONE => (case zero1 (not pos,t) y of NONE => NONE
   43.32                    | SOME z => SOME(c $ x $ z))
   43.33         | SOME z => SOME(c $ z $ y))
   43.34 -  | zero1 (pos,t) (u as (c as Const("uminus",_)) $ x) =
   43.35 +  | zero1 (pos,t) (u as (c as Const("HOL.uminus",_)) $ x) =
   43.36        (case zero1 (not pos,t) x of NONE => NONE
   43.37         | SOME z => SOME(c $ z))
   43.38    | zero1 (pos,t) u =
   43.39 @@ -77,7 +77,7 @@
   43.40                then tracing ("Abel cancel: " ^ string_of_cterm (cterm_of sg t))
   43.41                else ()
   43.42        val c $ lhs $ rhs = t
   43.43 -      val opp = case c of Const("op +",_) => true | _ => false;
   43.44 +      val opp = case c of Const("HOL.plus",_) => true | _ => false;
   43.45        val (pos,l) = find_common opp (terms lhs) (terms rhs)
   43.46        val posr = if opp then not pos else pos
   43.47        val t' = c $ (the(zero1 (pos,l) lhs)) $ (the(zero1 (posr,l) rhs))
    44.1 --- a/src/Provers/Arith/cancel_div_mod.ML	Fri Mar 10 12:28:38 2006 +0100
    44.2 +++ b/src/Provers/Arith/cancel_div_mod.ML	Fri Mar 10 15:33:48 2006 +0100
    44.3 @@ -6,8 +6,8 @@
    44.4  
    44.5    A + n*(m div n) + B + (m mod n) + C  ==  A + B + C + m
    44.6  
    44.7 -Is parameterized but assumes for simplicity that + and * are called
    44.8 -"op +" and "op *"
    44.9 +FIXME: Is parameterized but assumes for simplicity that + and * are called
   44.10 +"HOL.plus" and "HOL.minus"
   44.11  *)
   44.12  
   44.13  signature CANCEL_DIV_MOD_DATA =
   44.14 @@ -35,12 +35,12 @@
   44.15  functor CancelDivModFun(Data: CANCEL_DIV_MOD_DATA): CANCEL_DIV_MOD =
   44.16  struct
   44.17  
   44.18 -fun coll_div_mod (Const("op +",_) $ s $ t) dms =
   44.19 +fun coll_div_mod (Const("HOL.plus",_) $ s $ t) dms =
   44.20        coll_div_mod t (coll_div_mod s dms)
   44.21 -  | coll_div_mod (Const("op *",_) $ m $ (Const(d,_) $ s $ n))
   44.22 +  | coll_div_mod (Const("HOL.times",_) $ m $ (Const(d,_) $ s $ n))
   44.23                   (dms as (divs,mods)) =
   44.24        if d = Data.div_name andalso m=n then ((s,n)::divs,mods) else dms
   44.25 -  | coll_div_mod (Const("op *",_) $ (Const(d,_) $ s $ n) $ m)
   44.26 +  | coll_div_mod (Const("HOL.times",_) $ (Const(d,_) $ s $ n) $ m)
   44.27                   (dms as (divs,mods)) =
   44.28        if d = Data.div_name andalso m=n then ((s,n)::divs,mods) else dms
   44.29    | coll_div_mod (Const(m,_) $ s $ n) (dms as (divs,mods)) =
   44.30 @@ -56,8 +56,8 @@
   44.31     ==> thesis by transitivity
   44.32  *)
   44.33  
   44.34 -val mk_plus = Data.mk_binop "op +"
   44.35 -val mk_times = Data.mk_binop "op *"
   44.36 +val mk_plus = Data.mk_binop "HOL.plus"
   44.37 +val mk_times = Data.mk_binop "HOL.times"
   44.38  
   44.39  fun rearrange t pq =
   44.40    let val ts = Data.dest_sum t;
    45.1 --- a/src/Pure/Tools/class_package.ML	Fri Mar 10 12:28:38 2006 +0100
    45.2 +++ b/src/Pure/Tools/class_package.ML	Fri Mar 10 15:33:48 2006 +0100
    45.3 @@ -623,18 +623,10 @@
    45.4      val typ_def = Type.varifyT raw_typ_def;
    45.5      val typ_use = Type.varifyT raw_typ_use;
    45.6      val match_tab = Sign.typ_match thy (typ_def, typ_use) Vartab.empty;
    45.7 -    fun get_first_index f =
    45.8 -      let
    45.9 -        fun get _ [] = NONE
   45.10 -          | get i (x::xs) = 
   45.11 -              case f x
   45.12 -               of NONE => get (i+1) xs
   45.13 -                | SOME y => SOME (i, y)
   45.14 -      in get 0 end;
   45.15      fun tab_lookup vname = (the o Vartab.lookup match_tab) (vname, 0);
   45.16      fun mk_class_deriv thy subclasses superclass =
   45.17        let
   45.18 -        val (i, (subclass::deriv)) = (the oo get_first_index) (fn subclass =>
   45.19 +        val (i, (subclass::deriv)) = (the oo get_index) (fn subclass =>
   45.20              get_superclass_derivation thy (subclass, superclass)
   45.21            ) subclasses;
   45.22          val i' = if length subclasses = 1 then ~1 else i;
    46.1 --- a/src/Pure/library.ML	Fri Mar 10 12:28:38 2006 +0100
    46.2 +++ b/src/Pure/library.ML	Fri Mar 10 15:33:48 2006 +0100
    46.3 @@ -126,6 +126,7 @@
    46.4    val find_index: ('a -> bool) -> 'a list -> int
    46.5    val find_index_eq: ''a -> ''a list -> int
    46.6    val find_first: ('a -> bool) -> 'a list -> 'a option
    46.7 +  val get_index: ('a -> 'b option) -> 'a list -> (int * 'b) option
    46.8    val get_first: ('a -> 'b option) -> 'a list -> 'b option
    46.9    val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
   46.10    val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
   46.11 @@ -632,6 +633,15 @@
   46.12          NONE => get_first f xs
   46.13        | some => some);
   46.14  
   46.15 +fun get_index f =
   46.16 +  let
   46.17 +    fun get _ [] = NONE
   46.18 +      | get i (x::xs) = 
   46.19 +          case f x
   46.20 +           of NONE => get (i+1) xs
   46.21 +            | SOME y => SOME (i, y)
   46.22 +  in get 0 end;
   46.23 +
   46.24  (*flatten a list of lists to a list*)
   46.25  val flat = List.concat;
   46.26