--- a/NEWS Mon Aug 30 09:28:02 2010 +0200
+++ b/NEWS Mon Aug 30 09:35:30 2010 +0200
@@ -136,6 +136,7 @@
op & ~> HOL.conj
op | ~> HOL.disj
op --> ~> HOL.implies
+ op = ~> HOL.eq
Not ~> HOL.Not
The ~> HOL.The
All ~> HOL.All
--- a/src/HOL/Decision_Procs/Approximation.thy Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Mon Aug 30 09:35:30 2010 +0200
@@ -3305,7 +3305,7 @@
(Const (@{const_name Set.member}, _) $
Free (name, _) $ _)) = name
| variable_of_bound (Const (@{const_name Trueprop}, _) $
- (Const (@{const_name "op ="}, _) $
+ (Const (@{const_name HOL.eq}, _) $
Free (name, _) $ _)) = name
| variable_of_bound t = raise TERM ("variable_of_bound", [t])
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Mon Aug 30 09:35:30 2010 +0200
@@ -519,9 +519,9 @@
val [lt, le] = map (Morphism.term phi) [@{term "op \<sqsubset>"}, @{term "op \<sqsubseteq>"}]
fun h x t =
case term_of t of
- Const(@{const_name "op ="}, _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
+ Const(@{const_name HOL.eq}, _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
else Ferrante_Rackoff_Data.Nox
- | @{term "Not"}$(Const(@{const_name "op ="}, _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
+ | @{term "Not"}$(Const(@{const_name HOL.eq}, _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
else Ferrante_Rackoff_Data.Nox
| b$y$z => if Term.could_unify (b, lt) then
if term_of x aconv y then Ferrante_Rackoff_Data.Lt
@@ -771,7 +771,7 @@
in rth end
| _ => Thm.reflexive ct)
-| Const(@{const_name "op ="},_)$_$Const(@{const_name Groups.zero},_) =>
+| Const(@{const_name HOL.eq},_)$_$Const(@{const_name Groups.zero},_) =>
(case whatis x (Thm.dest_arg1 ct) of
("c*x+t",[c,t]) =>
let
@@ -835,7 +835,7 @@
val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
in rth end
-| Const(@{const_name "op ="},_)$a$b =>
+| Const(@{const_name HOL.eq},_)$a$b =>
let val (ca,cb) = Thm.dest_binop ct
val T = ctyp_of_term ca
val th = instantiate' [SOME T] [SOME ca, SOME cb] eq_iff_diff_eq_0
@@ -844,7 +844,7 @@
(Semiring_Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
in rth end
-| @{term "Not"} $(Const(@{const_name "op ="},_)$a$b) => Conv.arg_conv (field_isolate_conv phi ctxt vs) ct
+| @{term "Not"} $(Const(@{const_name HOL.eq},_)$a$b) => Conv.arg_conv (field_isolate_conv phi ctxt vs) ct
| _ => Thm.reflexive ct
end;
@@ -852,9 +852,9 @@
let
fun h x t =
case term_of t of
- Const(@{const_name "op ="}, _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
+ Const(@{const_name HOL.eq}, _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
else Ferrante_Rackoff_Data.Nox
- | @{term "Not"}$(Const(@{const_name "op ="}, _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
+ | @{term "Not"}$(Const(@{const_name HOL.eq}, _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
else Ferrante_Rackoff_Data.Nox
| Const(@{const_name Orderings.less},_)$y$z =>
if term_of x aconv y then Ferrante_Rackoff_Data.Lt
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Mon Aug 30 09:35:30 2010 +0200
@@ -912,7 +912,7 @@
definition "lt p = (case p of CP (C c) \<Rightarrow> if 0>\<^sub>N c then T else F| _ \<Rightarrow> Lt p)"
definition "le p = (case p of CP (C c) \<Rightarrow> if 0\<ge>\<^sub>N c then T else F | _ \<Rightarrow> Le p)"
-definition "eq p = (case p of CP (C c) \<Rightarrow> if c = 0\<^sub>N then T else F | _ \<Rightarrow> Eq p)"
+definition eq where "eq p = (case p of CP (C c) \<Rightarrow> if c = 0\<^sub>N then T else F | _ \<Rightarrow> Eq p)"
definition "neq p = not (eq p)"
lemma lt: "allpolys isnpoly p \<Longrightarrow> Ifm vs bs (lt p) = Ifm vs bs (Lt p)"
@@ -2960,7 +2960,7 @@
val ifft = @{term "op = :: bool => _"}
fun llt rT = Const(@{const_name Orderings.less},rrT rT);
fun lle rT = Const(@{const_name Orderings.less},rrT rT);
-fun eqt rT = Const(@{const_name "op ="},rrT rT);
+fun eqt rT = Const(@{const_name HOL.eq},rrT rT);
fun rz rT = Const(@{const_name Groups.zero},rT);
fun dest_nat t = case t of
@@ -3021,7 +3021,7 @@
| Const(@{const_name HOL.conj},_)$p$q => @{code And} (fm_of_term m m' p, fm_of_term m m' q)
| Const(@{const_name HOL.disj},_)$p$q => @{code Or} (fm_of_term m m' p, fm_of_term m m' q)
| Const(@{const_name HOL.implies},_)$p$q => @{code Imp} (fm_of_term m m' p, fm_of_term m m' q)
- | Const(@{const_name "op ="},ty)$p$q =>
+ | Const(@{const_name HOL.eq},ty)$p$q =>
if domain_type ty = bT then @{code Iff} (fm_of_term m m' p, fm_of_term m m' q)
else @{code Eq} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
| Const(@{const_name Orderings.less},_)$p$q =>
--- a/src/HOL/Decision_Procs/commutative_ring_tac.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML Mon Aug 30 09:35:30 2010 +0200
@@ -65,7 +65,7 @@
(* reification of the equation *)
val cr_sort = @{sort "comm_ring_1"};
-fun reif_eq thy (eq as Const(@{const_name "op ="}, Type("fun", [T, _])) $ lhs $ rhs) =
+fun reif_eq thy (eq as Const(@{const_name HOL.eq}, Type("fun", [T, _])) $ lhs $ rhs) =
if Sign.of_sort thy (T, cr_sort) then
let
val fs = OldTerm.term_frees eq;
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Mon Aug 30 09:35:30 2010 +0200
@@ -175,7 +175,7 @@
let
fun h bounds tm =
(case term_of tm of
- Const (@{const_name "op ="}, T) $ _ $ _ =>
+ Const (@{const_name HOL.eq}, T) $ _ $ _ =>
if domain_type T = HOLogic.boolT then find_args bounds tm
else Thm.dest_fun2 tm
| Const (@{const_name Not}, _) $ _ => h bounds (Thm.dest_arg tm)
--- a/src/HOL/Decision_Procs/langford.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Decision_Procs/langford.ML Mon Aug 30 09:35:30 2010 +0200
@@ -116,7 +116,7 @@
fun contains x ct = member (op aconv) (OldTerm.term_frees (term_of ct)) (term_of x);
fun is_eqx x eq = case term_of eq of
- Const(@{const_name "op ="},_)$l$r => l aconv term_of x orelse r aconv term_of x
+ Const(@{const_name HOL.eq},_)$l$r => l aconv term_of x orelse r aconv term_of x
| _ => false ;
local
@@ -176,7 +176,7 @@
let
fun h bounds tm =
(case term_of tm of
- Const (@{const_name "op ="}, T) $ _ $ _ =>
+ Const (@{const_name HOL.eq}, T) $ _ $ _ =>
if domain_type T = HOLogic.boolT then find_args bounds tm
else Thm.dest_fun2 tm
| Const (@{const_name Not}, _) $ _ => h bounds (Thm.dest_arg tm)
--- a/src/HOL/HOL.thy Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/HOL.thy Mon Aug 30 09:35:30 2010 +0200
@@ -61,14 +61,8 @@
disj :: "[bool, bool] => bool" (infixr "|" 30)
implies :: "[bool, bool] => bool" (infixr "-->" 25)
-setup Sign.root_path
+ eq :: "['a, 'a] => bool" (infixl "=" 50)
-consts
- "op =" :: "['a, 'a] => bool" (infixl "=" 50)
-
-setup Sign.local_path
-
-consts
The :: "('a => bool) => 'a"
All :: "('a => bool) => bool" (binder "ALL " 10)
Ex :: "('a => bool) => bool" (binder "EX " 10)
@@ -78,7 +72,7 @@
subsubsection {* Additional concrete syntax *}
notation (output)
- "op =" (infix "=" 50)
+ eq (infix "=" 50)
abbreviation
not_equal :: "['a, 'a] => bool" (infixl "~=" 50) where
@@ -89,15 +83,15 @@
notation (xsymbols)
Not ("\<not> _" [40] 40) and
- HOL.conj (infixr "\<and>" 35) and
- HOL.disj (infixr "\<or>" 30) and
- HOL.implies (infixr "\<longrightarrow>" 25) and
+ conj (infixr "\<and>" 35) and
+ disj (infixr "\<or>" 30) and
+ implies (infixr "\<longrightarrow>" 25) and
not_equal (infix "\<noteq>" 50)
notation (HTML output)
Not ("\<not> _" [40] 40) and
- HOL.conj (infixr "\<and>" 35) and
- HOL.disj (infixr "\<or>" 30) and
+ conj (infixr "\<and>" 35) and
+ disj (infixr "\<or>" 30) and
not_equal (infix "\<noteq>" 50)
abbreviation (iff)
@@ -183,8 +177,8 @@
True_or_False: "(P=True) | (P=False)"
finalconsts
- "op ="
- HOL.implies
+ eq
+ implies
The
definition If :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" ("(if (_)/ then (_)/ else (_))" [0, 0, 10] 10) where
@@ -864,7 +858,7 @@
setup {*
let
- fun non_bool_eq (@{const_name "op ="}, Type (_, [T, _])) = T <> @{typ bool}
+ fun non_bool_eq (@{const_name HOL.eq}, Type (_, [T, _])) = T <> @{typ bool}
| non_bool_eq _ = false;
val hyp_subst_tac' =
SUBGOAL (fn (goal, i) =>
@@ -930,7 +924,7 @@
(
val thy = @{theory}
type claset = Classical.claset
- val equality_name = @{const_name "op ="}
+ val equality_name = @{const_name HOL.eq}
val not_name = @{const_name Not}
val notE = @{thm notE}
val ccontr = @{thm ccontr}
@@ -1746,8 +1740,8 @@
fun eq_codegen thy defs dep thyname b t gr =
(case strip_comb t of
- (Const (@{const_name "op ="}, Type (_, [Type ("fun", _), _])), _) => NONE
- | (Const (@{const_name "op ="}, _), [t, u]) =>
+ (Const (@{const_name HOL.eq}, Type (_, [Type ("fun", _), _])), _) => NONE
+ | (Const (@{const_name HOL.eq}, _), [t, u]) =>
let
val (pt, gr') = Codegen.invoke_codegen thy defs dep thyname false t gr;
val (pu, gr'') = Codegen.invoke_codegen thy defs dep thyname false u gr';
@@ -1756,7 +1750,7 @@
SOME (Codegen.parens
(Pretty.block [pt, Codegen.str " =", Pretty.brk 1, pu]), gr''')
end
- | (t as Const (@{const_name "op ="}, _), ts) => SOME (Codegen.invoke_codegen
+ | (t as Const (@{const_name HOL.eq}, _), ts) => SOME (Codegen.invoke_codegen
thy defs dep thyname b (Codegen.eta_expand t ts 2) gr)
| _ => NONE);
@@ -1796,7 +1790,7 @@
setup {*
Code_Preproc.map_pre (fn simpset =>
- simpset addsimprocs [Simplifier.simproc_global_i @{theory} "equal" [@{term "op ="}]
+ simpset addsimprocs [Simplifier.simproc_global_i @{theory} "equal" [@{term HOL.eq}]
(fn thy => fn _ => fn Const (_, T) => case strip_type T
of (Type _ :: _, _) => SOME @{thm eq_equal}
| _ => NONE)])
@@ -1944,7 +1938,7 @@
code_const "HOL.equal"
(Haskell infixl 4 "==")
-code_const "op ="
+code_const HOL.eq
(Haskell infixl 4 "==")
text {* undefined *}
--- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Mon Aug 30 09:35:30 2010 +0200
@@ -53,7 +53,7 @@
F > False
ONE_ONE > HOL4Setup.ONE_ONE
ONTO > Fun.surj
- "=" > "op ="
+ "=" > HOL.eq
"==>" > HOL.implies
"/\\" > HOL.conj
"\\/" > HOL.disj
--- a/src/HOL/Import/HOLLight/hollight.imp Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Import/HOLLight/hollight.imp Mon Aug 30 09:35:30 2010 +0200
@@ -234,7 +234,7 @@
">=" > "HOLLight.hollight.>="
">" > "HOLLight.hollight.>"
"==>" > HOL.implies
- "=" > "op ="
+ "=" > HOL.eq
"<=" > "HOLLight.hollight.<="
"<" > "HOLLight.hollight.<"
"/\\" > HOL.conj
--- a/src/HOL/Import/hol4rews.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Import/hol4rews.ML Mon Aug 30 09:35:30 2010 +0200
@@ -627,7 +627,7 @@
thy |> add_hol4_type_mapping "min" "bool" false @{type_name bool}
|> add_hol4_type_mapping "min" "fun" false "fun"
|> add_hol4_type_mapping "min" "ind" false @{type_name ind}
- |> add_hol4_const_mapping "min" "=" false @{const_name "op ="}
+ |> add_hol4_const_mapping "min" "=" false @{const_name HOL.eq}
|> add_hol4_const_mapping "min" "==>" false @{const_name HOL.implies}
|> add_hol4_const_mapping "min" "@" false @{const_name "Eps"}
in
--- a/src/HOL/Import/proof_kernel.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML Mon Aug 30 09:35:30 2010 +0200
@@ -1205,7 +1205,7 @@
fun non_trivial_term_consts t = fold_aterms
(fn Const (c, _) =>
if c = @{const_name Trueprop} orelse c = @{const_name All}
- orelse c = @{const_name HOL.implies} orelse c = @{const_name HOL.conj} orelse c = @{const_name "op ="}
+ orelse c = @{const_name HOL.implies} orelse c = @{const_name HOL.conj} orelse c = @{const_name HOL.eq}
then I else insert (op =) c
| _ => I) t [];
@@ -1213,7 +1213,7 @@
let
fun add_consts (Const (c, _), cs) =
(case c of
- @{const_name "op ="} => insert (op =) "==" cs
+ @{const_name HOL.eq} => insert (op =) "==" cs
| @{const_name HOL.implies} => insert (op =) "==>" cs
| @{const_name All} => cs
| "all" => cs
@@ -1476,10 +1476,10 @@
fun mk_COMB th1 th2 thy =
let
val (f,g) = case concl_of th1 of
- _ $ (Const(@{const_name "op ="},_) $ f $ g) => (f,g)
+ _ $ (Const(@{const_name HOL.eq},_) $ f $ g) => (f,g)
| _ => raise ERR "mk_COMB" "First theorem not an equality"
val (x,y) = case concl_of th2 of
- _ $ (Const(@{const_name "op ="},_) $ x $ y) => (x,y)
+ _ $ (Const(@{const_name HOL.eq},_) $ x $ y) => (x,y)
| _ => raise ERR "mk_COMB" "Second theorem not an equality"
val fty = type_of f
val (fd,fr) = dom_rng fty
@@ -1788,7 +1788,7 @@
val cv = cterm_of thy v
val th1 = implies_elim_all (beta_eta_thm th)
val (f,g) = case concl_of th1 of
- _ $ (Const(@{const_name "op ="},_) $ f $ g) => (Term.lambda v f,Term.lambda v g)
+ _ $ (Const(@{const_name HOL.eq},_) $ f $ g) => (Term.lambda v f,Term.lambda v g)
| _ => raise ERR "mk_ABS" "Bad conclusion"
val (fd,fr) = dom_rng (type_of f)
val abs_thm' = Drule.instantiate' [SOME (ctyp_of thy fd), SOME (ctyp_of thy fr)] [SOME (cterm_of thy f), SOME (cterm_of thy g)] abs_thm
--- a/src/HOL/Import/shuffler.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Import/shuffler.ML Mon Aug 30 09:35:30 2010 +0200
@@ -60,14 +60,14 @@
fun mk_meta_eq th =
(case concl_of th of
- Const(@{const_name Trueprop},_) $ (Const(@{const_name "op ="},_) $ _ $ _) => th RS eq_reflection
+ Const(@{const_name Trueprop},_) $ (Const(@{const_name HOL.eq},_) $ _ $ _) => th RS eq_reflection
| Const("==",_) $ _ $ _ => th
| _ => raise THM("Not an equality",0,[th]))
handle _ => raise THM("Couldn't make meta equality",0,[th]) (* FIXME avoid handle _ *)
fun mk_obj_eq th =
(case concl_of th of
- Const(@{const_name Trueprop},_) $ (Const(@{const_name "op ="},_) $ _ $ _) => th
+ Const(@{const_name Trueprop},_) $ (Const(@{const_name HOL.eq},_) $ _ $ _) => th
| Const("==",_) $ _ $ _ => th RS meta_eq_to_obj_eq
| _ => raise THM("Not an equality",0,[th]))
handle _ => raise THM("Couldn't make object equality",0,[th]) (* FIXME avoid handle _ *)
--- a/src/HOL/Library/OptionalSugar.thy Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Library/OptionalSugar.thy Mon Aug 30 09:35:30 2010 +0200
@@ -32,7 +32,7 @@
(* deprecated, use thm with style instead, will be removed *)
(* aligning equations *)
notation (tab output)
- "op =" ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and
+ "HOL.eq" ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and
"==" ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)")
(* Let *)
--- a/src/HOL/Library/reflection.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Library/reflection.ML Mon Aug 30 09:35:30 2010 +0200
@@ -82,7 +82,7 @@
fun rearrange congs =
let
fun P (_, th) =
- let val @{term "Trueprop"}$(Const (@{const_name "op ="},_) $l$_) = concl_of th
+ let val @{term "Trueprop"}$(Const (@{const_name HOL.eq},_) $l$_) = concl_of th
in can dest_Var l end
val (yes,no) = List.partition P congs
in no @ yes end
--- a/src/HOL/Mutabelle/Mutabelle.thy Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Mutabelle/Mutabelle.thy Mon Aug 30 09:35:30 2010 +0200
@@ -4,7 +4,7 @@
begin
ML {*
-val comms = [@{const_name "op ="}, @{const_name HOL.disj}, @{const_name HOL.conj}];
+val comms = [@{const_name HOL.eq}, @{const_name HOL.disj}, @{const_name HOL.conj}];
val forbidden =
[(@{const_name Power.power}, "'a"),
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Mon Aug 30 09:35:30 2010 +0200
@@ -187,7 +187,7 @@
val nitpick_mtd = ("nitpick", invoke_nitpick)
*)
-val comms = [@{const_name "op ="}, @{const_name HOL.disj}, @{const_name HOL.conj}]
+val comms = [@{const_name HOL.eq}, @{const_name HOL.disj}, @{const_name HOL.conj}]
val forbidden =
[(* (@{const_name "power"}, "'a"), *)
--- a/src/HOL/Nominal/nominal_datatype.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Mon Aug 30 09:35:30 2010 +0200
@@ -183,7 +183,7 @@
end;
fun mk_not_sym ths = maps (fn th => case prop_of th of
- _ $ (Const (@{const_name Not}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _)) => [th, th RS not_sym]
+ _ $ (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _)) => [th, th RS not_sym]
| _ => [th]) ths;
fun fresh_const T U = Const ("Nominal.fresh", T --> U --> HOLogic.boolT);
--- a/src/HOL/Nominal/nominal_thmdecls.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML Mon Aug 30 09:35:30 2010 +0200
@@ -147,7 +147,7 @@
else raise EQVT_FORM "Type Implication"
end
(* case: eqvt-lemma is of the equational form *)
- | (Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, _) $
+ | (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $
(Const (@{const_name "perm"},typrm) $ Var (pi,typi) $ lhs) $ rhs)) =>
(if (apply_pi lhs (pi,typi)) = rhs
then [orig_thm]
--- a/src/HOL/Set.thy Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Set.thy Mon Aug 30 09:35:30 2010 +0200
@@ -268,7 +268,7 @@
fun setcompr_tr [e, idts, b] =
let
- val eq = Syntax.const @{const_syntax "op ="} $ Bound (nvars idts) $ e;
+ val eq = Syntax.const @{const_syntax HOL.eq} $ Bound (nvars idts) $ e;
val P = Syntax.const @{const_syntax HOL.conj} $ eq $ b;
val exP = ex_tr [idts, P];
in Syntax.const @{const_syntax Collect} $ Term.absdummy (dummyT, exP) end;
@@ -289,7 +289,7 @@
let
fun check (Const (@{const_syntax Ex}, _) $ Abs (_, _, P), n) = check (P, n + 1)
| check (Const (@{const_syntax HOL.conj}, _) $
- (Const (@{const_syntax "op ="}, _) $ Bound m $ e) $ P, n) =
+ (Const (@{const_syntax HOL.eq}, _) $ Bound m $ e) $ P, n) =
n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso
subset (op =) (0 upto (n - 1), add_loose_bnos (e, 0, []))
| check _ = false;
--- a/src/HOL/Statespace/distinct_tree_prover.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Statespace/distinct_tree_prover.ML Mon Aug 30 09:35:30 2010 +0200
@@ -343,7 +343,7 @@
end handle Option => NONE)
fun distinctTree_tac names ctxt
- (Const (@{const_name Trueprop},_) $ (Const (@{const_name Not}, _) $ (Const (@{const_name "op ="}, _) $ x $ y)), i) =
+ (Const (@{const_name Trueprop},_) $ (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, _) $ x $ y)), i) =
(case get_fst_success (neq_x_y ctxt x y) names of
SOME neq => rtac neq i
| NONE => no_tac)
@@ -356,7 +356,7 @@
fun distinct_simproc names =
Simplifier.simproc_global @{theory HOL} "DistinctTreeProver.distinct_simproc" ["x = y"]
- (fn thy => fn ss => fn (Const (@{const_name "op ="},_)$x$y) =>
+ (fn thy => fn ss => fn (Const (@{const_name HOL.eq},_)$x$y) =>
case try Simplifier.the_context ss of
SOME ctxt => Option.map (fn neq => neq_to_eq_False OF [neq])
(get_fst_success (neq_x_y ctxt x y) names)
--- a/src/HOL/Statespace/state_fun.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Statespace/state_fun.ML Mon Aug 30 09:35:30 2010 +0200
@@ -285,7 +285,7 @@
then Bound 2
else raise TERM ("",[n]);
val sel' = lo $ d $ n' $ s;
- in (Const (@{const_name "op ="},Teq)$sel'$x',hd (binder_types Teq),nT,swap) end;
+ in (Const (@{const_name HOL.eq},Teq)$sel'$x',hd (binder_types Teq),nT,swap) end;
fun dest_state (s as Bound 0) = s
| dest_state (s as (Const (sel,sT)$Bound 0)) =
@@ -295,10 +295,10 @@
| dest_state s =
raise TERM ("StateFun.ex_lookup_eq_simproc: not a record slector",[s]);
- fun dest_sel_eq (Const (@{const_name "op ="},Teq)$
+ fun dest_sel_eq (Const (@{const_name HOL.eq},Teq)$
((lo as (Const ("StateFun.lookup",lT)))$d$n$s)$X) =
(false,Teq,lT,lo,d,n,X,dest_state s)
- | dest_sel_eq (Const (@{const_name "op ="},Teq)$X$
+ | dest_sel_eq (Const (@{const_name HOL.eq},Teq)$X$
((lo as (Const ("StateFun.lookup",lT)))$d$n$s)) =
(true,Teq,lT,lo,d,n,X,dest_state s)
| dest_sel_eq _ = raise TERM ("",[]);
--- a/src/HOL/Statespace/state_space.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Statespace/state_space.ML Mon Aug 30 09:35:30 2010 +0200
@@ -223,7 +223,7 @@
fun distinctTree_tac ctxt
(Const (@{const_name Trueprop},_) $
- (Const (@{const_name Not}, _) $ (Const (@{const_name "op ="}, _) $ (x as Free _)$ (y as Free _))), i) =
+ (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, _) $ (x as Free _)$ (y as Free _))), i) =
(case (neq_x_y ctxt x y) of
SOME neq => rtac neq i
| NONE => no_tac)
@@ -236,7 +236,7 @@
val distinct_simproc =
Simplifier.simproc_global @{theory HOL} "StateSpace.distinct_simproc" ["x = y"]
- (fn thy => fn ss => (fn (Const (@{const_name "op ="},_)$(x as Free _)$(y as Free _)) =>
+ (fn thy => fn ss => (fn (Const (@{const_name HOL.eq},_)$(x as Free _)$(y as Free _)) =>
(case try Simplifier.the_context ss of
SOME ctxt => Option.map (fn neq => DistinctTreeProver.neq_to_eq_False OF [neq])
(neq_x_y ctxt x y)
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Mon Aug 30 09:35:30 2010 +0200
@@ -416,7 +416,7 @@
fun prove_case_cong ((t, nchotomy), case_rewrites) =
let
val (Const ("==>", _) $ tm $ _) = t;
- val (Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, _) $ _ $ Ma)) = tm;
+ val (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ Ma)) = tm;
val cert = cterm_of thy;
val nchotomy' = nchotomy RS spec;
val [v] = Term.add_vars (concl_of nchotomy') [];
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Mon Aug 30 09:35:30 2010 +0200
@@ -96,7 +96,7 @@
fun mk_side const_name = Const (const_name, ty --> ty --> HOLogic.boolT)
$ Free ("x", ty) $ Free ("y", ty);
val def = HOLogic.mk_Trueprop (HOLogic.mk_eq
- (mk_side @{const_name HOL.equal}, mk_side @{const_name "op ="}));
+ (mk_side @{const_name HOL.equal}, mk_side @{const_name HOL.eq}));
val def' = Syntax.check_term lthy def;
val ((_, (_, thm)), lthy') = Specification.definition
(NONE, (Attrib.empty_binding, def')) lthy;
--- a/src/HOL/Tools/Function/termination.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Function/termination.ML Mon Aug 30 09:35:30 2010 +0200
@@ -148,7 +148,7 @@
val cs = Function_Lib.dest_binop_list @{const_name Lattices.sup} rel
fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
let
- val (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ _)
+ val (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ _)
= Term.strip_qnt_body @{const_name Ex} c
in cons r o cons l end
in
@@ -185,7 +185,7 @@
val vs = Term.strip_qnt_vars @{const_name Ex} c
(* FIXME: throw error "dest_call" for malformed terms *)
- val (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ Gam)
+ val (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ Gam)
= Term.strip_qnt_body @{const_name Ex} c
val (p, l') = dest_inj sk l
val (q, r') = dest_inj sk r
--- a/src/HOL/Tools/Nitpick/minipick.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Nitpick/minipick.ML Mon Aug 30 09:35:30 2010 +0200
@@ -123,7 +123,7 @@
Exist (decls_for SRep card Ts T, to_F (T :: Ts) t')
| (t0 as Const (@{const_name Ex}, _)) $ t1 =>
to_F Ts (t0 $ eta_expand Ts t1 1)
- | Const (@{const_name "op ="}, _) $ t1 $ t2 =>
+ | Const (@{const_name HOL.eq}, _) $ t1 $ t2 =>
RelEq (to_R_rep Ts t1, to_R_rep Ts t2)
| Const (@{const_name ord_class.less_eq},
Type (@{type_name fun},
@@ -165,8 +165,8 @@
@{const Not} => to_R_rep Ts (eta_expand Ts t 1)
| Const (@{const_name All}, _) => to_R_rep Ts (eta_expand Ts t 1)
| Const (@{const_name Ex}, _) => to_R_rep Ts (eta_expand Ts t 1)
- | Const (@{const_name "op ="}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
- | Const (@{const_name "op ="}, _) => to_R_rep Ts (eta_expand Ts t 2)
+ | Const (@{const_name HOL.eq}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
+ | Const (@{const_name HOL.eq}, _) => to_R_rep Ts (eta_expand Ts t 2)
| Const (@{const_name ord_class.less_eq},
Type (@{type_name fun},
[Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ =>
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Aug 30 09:35:30 2010 +0200
@@ -408,7 +408,7 @@
(@{const_name True}, 0),
(@{const_name All}, 1),
(@{const_name Ex}, 1),
- (@{const_name "op ="}, 1),
+ (@{const_name HOL.eq}, 1),
(@{const_name HOL.conj}, 2),
(@{const_name HOL.disj}, 2),
(@{const_name HOL.implies}, 2),
@@ -1275,7 +1275,7 @@
forall is_Var args andalso not (has_duplicates (op =) args)
| _ => false
fun do_eq (Const (@{const_name "=="}, _) $ t1 $ _) = do_lhs t1
- | do_eq (@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)) =
+ | do_eq (@{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t1 $ _)) =
do_lhs t1
| do_eq _ = false
in do_eq end
@@ -1347,7 +1347,7 @@
@{const "==>"} $ _ $ t2 => term_under_def t2
| Const (@{const_name "=="}, _) $ t1 $ _ => term_under_def t1
| @{const Trueprop} $ t1 => term_under_def t1
- | Const (@{const_name "op ="}, _) $ t1 $ _ => term_under_def t1
+ | Const (@{const_name HOL.eq}, _) $ t1 $ _ => term_under_def t1
| Abs (_, _, t') => term_under_def t'
| t1 $ _ => term_under_def t1
| _ => t
@@ -1371,7 +1371,7 @@
val (lhs, rhs) =
case t of
Const (@{const_name "=="}, _) $ t1 $ t2 => (t1, t2)
- | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ t2) =>
+ | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t1 $ t2) =>
(t1, t2)
| _ => raise TERM ("Nitpick_HOL.normalized_rhs_of", [t])
val args = strip_comb lhs |> snd
@@ -1453,7 +1453,7 @@
| @{const "==>"} $ _ $ t2 => lhs_of_equation t2
| @{const Trueprop} $ t1 => lhs_of_equation t1
| Const (@{const_name All}, _) $ Abs (_, _, t1) => lhs_of_equation t1
- | Const (@{const_name "op ="}, _) $ t1 $ _ => SOME t1
+ | Const (@{const_name HOL.eq}, _) $ t1 $ _ => SOME t1
| @{const HOL.implies} $ _ $ t2 => lhs_of_equation t2
| _ => NONE
fun is_constr_pattern _ (Bound _) = true
@@ -1807,7 +1807,7 @@
(betapply (t2, var_t))
end
| extensional_equal _ T t1 t2 =
- Const (@{const_name "op ="}, T --> T --> bool_T) $ t1 $ t2
+ Const (@{const_name HOL.eq}, T --> T --> bool_T) $ t1 $ t2
fun equationalize_term ctxt tag t =
let
@@ -1816,7 +1816,7 @@
in
Logic.list_implies (prems,
case concl of
- @{const Trueprop} $ (Const (@{const_name "op ="}, Type (_, [T, _]))
+ @{const Trueprop} $ (Const (@{const_name HOL.eq}, Type (_, [T, _]))
$ t1 $ t2) =>
@{const Trueprop} $ extensional_equal j T t1 t2
| @{const Trueprop} $ t' =>
@@ -2290,7 +2290,7 @@
| simps => simps
fun is_equational_fun_surely_complete hol_ctxt x =
case equational_fun_axioms hol_ctxt x of
- [@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)] =>
+ [@{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t1 $ _)] =>
strip_comb t1 |> snd |> forall is_Var
| _ => false
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Aug 30 09:35:30 2010 +0200
@@ -590,7 +590,7 @@
if co then
Const (@{const_name The}, (T --> bool_T) --> T)
$ Abs (cyclic_co_val_name (), T,
- Const (@{const_name "op ="}, T --> T --> bool_T)
+ Const (@{const_name HOL.eq}, T --> T --> bool_T)
$ Bound 0 $ abstract_over (var, t))
else
cyclic_atom ()
@@ -849,7 +849,7 @@
(** Model reconstruction **)
fun unfold_outer_the_binders (t as Const (@{const_name The}, _)
- $ Abs (s, T, Const (@{const_name "op ="}, _)
+ $ Abs (s, T, Const (@{const_name HOL.eq}, _)
$ Bound 0 $ t')) =
betapply (Abs (s, T, t'), t) |> unfold_outer_the_binders
| unfold_outer_the_binders t = t
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Aug 30 09:35:30 2010 +0200
@@ -222,7 +222,7 @@
| fin_fun_body _ _ (t as Const (@{const_name None}, _)) = SOME t
| fin_fun_body dom_T ran_T
((t0 as Const (@{const_name If}, _))
- $ (t1 as Const (@{const_name "op ="}, _) $ Bound 0 $ t1')
+ $ (t1 as Const (@{const_name HOL.eq}, _) $ Bound 0 $ t1')
$ t2 $ t3) =
(if loose_bvar1 (t1', 0) then
NONE
@@ -650,7 +650,7 @@
Bound 0)))) accum
|>> mtype_of_mterm
end
- | @{const_name "op ="} => do_equals T accum
+ | @{const_name HOL.eq} => do_equals T accum
| @{const_name The} =>
(trace_msg (K "*** The"); raise UNSOLVABLE ())
| @{const_name Eps} =>
@@ -760,7 +760,7 @@
do_term (incr_boundvars ~1 t1') accum
else
raise SAME ()
- | (t11 as Const (@{const_name "op ="}, _)) $ Bound 0 $ t13 =>
+ | (t11 as Const (@{const_name HOL.eq}, _)) $ Bound 0 $ t13 =>
if not (loose_bvar1 (t13, 0)) then
do_term (incr_boundvars ~1 (t11 $ t13)) accum
else
@@ -876,7 +876,7 @@
do_term (@{const Not}
$ (HOLogic.eq_const (domain_type T0) $ t1
$ Abs (Name.uu, T1, @{const False}))) accum)
- | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
+ | Const (x as (@{const_name HOL.eq}, _)) $ t1 $ t2 =>
do_equals x t1 t2
| Const (@{const_name Let}, _) $ t1 $ t2 =>
do_formula sn (betapply (t2, t1)) accum
@@ -973,7 +973,7 @@
do_conjunction t0 t1 t2 accum
| (t0 as Const (@{const_name All}, _)) $ Abs (s0, T1, t1) =>
do_all t0 s0 T1 t1 accum
- | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
+ | Const (x as (@{const_name HOL.eq}, _)) $ t1 $ t2 =>
consider_general_equals mdata true x t1 t2 accum
| (t0 as @{const HOL.conj}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum
| (t0 as @{const HOL.implies}) $ t1 $ t2 => do_implies t0 t1 t2 accum
@@ -1069,7 +1069,7 @@
Abs (Name.uu, set_T', @{const True})
| _ => Const (s, T')
else if s = @{const_name "=="} orelse
- s = @{const_name "op ="} then
+ s = @{const_name HOL.eq} then
let
val T =
case T' of
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Aug 30 09:35:30 2010 +0200
@@ -447,7 +447,7 @@
val t1 = incr_boundvars n t1
val t2 = incr_boundvars n t2
val xs = map Bound (n - 1 downto 0)
- val equation = Const (@{const_name "op ="},
+ val equation = Const (@{const_name HOL.eq},
body_T --> body_T --> bool_T)
$ betapplys (t1, xs) $ betapplys (t2, xs)
val t =
@@ -515,9 +515,9 @@
do_description_operator The @{const_name undefined_fast_The} x t1
| (Const (x as (@{const_name Eps}, _)), [t1]) =>
do_description_operator Eps @{const_name undefined_fast_Eps} x t1
- | (Const (@{const_name "op ="}, T), [t1]) =>
+ | (Const (@{const_name HOL.eq}, T), [t1]) =>
Op1 (SingletonSet, range_type T, Any, sub t1)
- | (Const (@{const_name "op ="}, T), [t1, t2]) => sub_equals T t1 t2
+ | (Const (@{const_name HOL.eq}, T), [t1, t2]) => sub_equals T t1 t2
| (Const (@{const_name HOL.conj}, _), [t1, t2]) =>
Op2 (And, bool_T, Any, sub' t1, sub' t2)
| (Const (@{const_name HOL.disj}, _), [t1, t2]) =>
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Aug 30 09:35:30 2010 +0200
@@ -41,7 +41,7 @@
fun aux def (Const (@{const_name "=="}, _) $ t1 $ t2) =
aux def t1 andalso aux false t2
| aux def (@{const "==>"} $ t1 $ t2) = aux false t1 andalso aux def t2
- | aux def (Const (@{const_name "op ="}, _) $ t1 $ t2) =
+ | aux def (Const (@{const_name HOL.eq}, _) $ t1 $ t2) =
aux def t1 andalso aux false t2
| aux def (@{const HOL.implies} $ t1 $ t2) = aux false t1 andalso aux def t2
| aux def (t1 $ t2) = aux def t1 andalso aux def t2
@@ -149,7 +149,7 @@
case t of
@{const Trueprop} $ t1 => box_var_in_def new_Ts old_Ts t1 z
| Const (s0, _) $ t1 $ _ =>
- if s0 = @{const_name "=="} orelse s0 = @{const_name "op ="} then
+ if s0 = @{const_name "=="} orelse s0 = @{const_name HOL.eq} then
let
val (t', args) = strip_comb t1
val T' = fastype_of1 (new_Ts, do_term new_Ts old_Ts Neut t')
@@ -209,7 +209,7 @@
do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
| Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
- | Const (s0 as @{const_name "op ="}, T0) $ t1 $ t2 =>
+ | Const (s0 as @{const_name HOL.eq}, T0) $ t1 $ t2 =>
do_equals new_Ts old_Ts s0 T0 t1 t2
| @{const HOL.conj} $ t1 $ t2 =>
@{const HOL.conj} $ do_term new_Ts old_Ts polar t1
@@ -332,7 +332,7 @@
do_eq_or_imp Ts true def t0 t1 t2 seen
| (t0 as @{const "==>"}) $ t1 $ t2 =>
if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen
- | (t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2 =>
+ | (t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2 =>
do_eq_or_imp Ts true def t0 t1 t2 seen
| (t0 as @{const HOL.implies}) $ t1 $ t2 =>
do_eq_or_imp Ts false def t0 t1 t2 seen
@@ -399,7 +399,7 @@
aux_eq careful true t0 t1 t2
| aux careful ((t0 as @{const "==>"}) $ t1 $ t2) =
t0 $ aux false t1 $ aux careful t2
- | aux careful ((t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2) =
+ | aux careful ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2) =
aux_eq careful true t0 t1 t2
| aux careful ((t0 as @{const HOL.implies}) $ t1 $ t2) =
t0 $ aux false t1 $ aux careful t2
@@ -464,9 +464,9 @@
and aux_implies prems zs t1 t2 =
case t1 of
Const (@{const_name "=="}, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2
- | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ Var z $ t') =>
+ | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ Var z $ t') =>
aux_eq prems zs z t' t1 t2
- | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t' $ Var z) =>
+ | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t' $ Var z) =>
aux_eq prems zs z t' t1 t2
| _ => aux (t1 :: prems) (Term.add_vars t1 zs) t2
and aux_eq prems zs z t' t1 t2 =
@@ -499,7 +499,7 @@
handle SAME () => do_term (t :: seen) ts
in
case t of
- Const (@{const_name "op ="}, _) $ t1 $ t2 => do_eq true t1 t2
+ Const (@{const_name HOL.eq}, _) $ t1 $ t2 => do_eq true t1 t2
| _ => do_term (t :: seen) ts
end
in do_term end
@@ -653,7 +653,7 @@
fun params_in_equation (@{const "==>"} $ _ $ t2) = params_in_equation t2
| params_in_equation (@{const Trueprop} $ t1) = params_in_equation t1
- | params_in_equation (Const (@{const_name "op ="}, _) $ t1 $ _) =
+ | params_in_equation (Const (@{const_name HOL.eq}, _) $ t1 $ _) =
snd (strip_comb t1)
| params_in_equation _ = []
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Mon Aug 30 09:35:30 2010 +0200
@@ -179,7 +179,7 @@
fun translate_literal ctxt constant_table t =
case strip_comb t of
- (Const (@{const_name "op ="}, _), [l, r]) =>
+ (Const (@{const_name HOL.eq}, _), [l, r]) =>
let
val l' = translate_term ctxt constant_table l
val r' = translate_term ctxt constant_table r
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Mon Aug 30 09:35:30 2010 +0200
@@ -411,7 +411,7 @@
fun conjuncts t = conjuncts_aux t [];
fun is_equationlike_term (Const ("==", _) $ _ $ _) = true
- | is_equationlike_term (Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _)) = true
+ | is_equationlike_term (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _)) = true
| is_equationlike_term _ = false
val is_equationlike = is_equationlike_term o prop_of
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Aug 30 09:35:30 2010 +0200
@@ -587,7 +587,7 @@
fun preprocess_elim ctxt elimrule =
let
- fun replace_eqs (Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, T) $ lhs $ rhs)) =
+ fun replace_eqs (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, T) $ lhs $ rhs)) =
HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs)
| replace_eqs t = t
val thy = ProofContext.theory_of ctxt
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Mon Aug 30 09:35:30 2010 +0200
@@ -111,7 +111,7 @@
fun mk_meta_equation th =
case prop_of th of
- Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _) => th RS @{thm eq_reflection}
+ Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => th RS @{thm eq_reflection}
| _ => th
val meta_fun_cong = @{lemma "f == g ==> f x == g x" by simp}
@@ -217,7 +217,7 @@
@{const_name "==>"},
@{const_name Trueprop},
@{const_name Not},
- @{const_name "op ="},
+ @{const_name HOL.eq},
@{const_name HOL.implies},
@{const_name All},
@{const_name Ex},
--- a/src/HOL/Tools/Qelim/cooper.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Mon Aug 30 09:35:30 2010 +0200
@@ -122,8 +122,8 @@
( case (term_of ct) of
Const(@{const_name HOL.conj},_)$_$_ => And (Thm.dest_binop ct)
| Const (@{const_name HOL.disj},_)$_$_ => Or (Thm.dest_binop ct)
-| Const (@{const_name "op ="},_)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox
-| Const (@{const_name Not},_) $ (Const (@{const_name "op ="},_)$y$_) =>
+| Const (@{const_name HOL.eq},_)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox
+| Const (@{const_name Not},_) $ (Const (@{const_name HOL.eq},_)$y$_) =>
if term_of x aconv y then NEq (funpow 2 Thm.dest_arg ct) else Nox
| Const (@{const_name Orderings.less}, _) $ y$ z =>
if term_of x aconv y then Lt (Thm.dest_arg ct)
@@ -274,7 +274,7 @@
| lin vs (Const (@{const_name Not},T)$t) = Const (@{const_name Not},T)$ (lin vs t)
| lin (vs as x::_) (Const(@{const_name Rings.dvd},_)$d$t) =
HOLogic.mk_binrel @{const_name Rings.dvd} (numeral1 abs d, lint vs t)
- | lin (vs as x::_) ((b as Const(@{const_name "op ="},_))$s$t) =
+ | lin (vs as x::_) ((b as Const(@{const_name HOL.eq},_))$s$t) =
(case lint vs (subC$t$s) of
(t as a$(m$c$y)$r) =>
if x <> y then b$zero$t
@@ -345,7 +345,7 @@
case (term_of t) of
Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ =>
if x aconv y andalso member (op =)
- ["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
+ [@{const_name HOL.eq}, @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
then (ins (dest_number c) acc,dacc) else (acc,dacc)
| Const(s,_)$_$(Const(@{const_name Groups.times},_)$c$y) =>
if x aconv y andalso member (op =)
@@ -387,7 +387,7 @@
| Const (@{const_name Not},_)$_ => Conv.arg_conv unit_conv t
| Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ =>
if x=y andalso member (op =)
- ["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
+ [@{const_name HOL.eq}, @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
then cv (l div dest_number c) t else Thm.reflexive t
| Const(s,_)$_$(Const(@{const_name Groups.times},_)$c$y) =>
if x=y andalso member (op =)
--- a/src/HOL/Tools/Qelim/qelim.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Qelim/qelim.ML Mon Aug 30 09:35:30 2010 +0200
@@ -26,7 +26,7 @@
Const(s,T)$_$_ =>
if domain_type T = HOLogic.boolT
andalso member (op =) [@{const_name HOL.conj}, @{const_name HOL.disj},
- @{const_name HOL.implies}, @{const_name "op ="}] s
+ @{const_name HOL.implies}, @{const_name HOL.eq}] s
then binop_conv (conv env) p
else atcv env p
| Const(@{const_name Not},_)$_ => arg_conv (conv env) p
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Mon Aug 30 09:35:30 2010 +0200
@@ -338,7 +338,7 @@
=> rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
(* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *)
-| (Const (@{const_name "op ="},_) $
+| (Const (@{const_name HOL.eq},_) $
(Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
(Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
=> rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}
@@ -350,7 +350,7 @@
=> rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
(* (op =) (Bex...) (Bex...) ----> (op =) (...) (...) *)
-| Const (@{const_name "op ="},_) $
+| Const (@{const_name HOL.eq},_) $
(Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
(Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
=> rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}
@@ -370,13 +370,13 @@
(Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
=> rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt]
-| Const (@{const_name "op ="},_) $ (R $ _ $ _) $ (_ $ _ $ _) =>
+| Const (@{const_name HOL.eq},_) $ (R $ _ $ _) $ (_ $ _ $ _) =>
(rtac @{thm refl} ORELSE'
(equals_rsp_tac R ctxt THEN' RANGE [
quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]))
(* reflexivity of operators arising from Cong_tac *)
-| Const (@{const_name "op ="},_) $ _ $ _ => rtac @{thm refl}
+| Const (@{const_name HOL.eq},_) $ _ $ _ => rtac @{thm refl}
(* respectfulness of constants; in particular of a simple relation *)
| _ $ (Const _) $ (Const _) (* fun_rel, list_rel, etc but not equality *)
--- a/src/HOL/Tools/Quotient/quotient_term.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Mon Aug 30 09:35:30 2010 +0200
@@ -267,7 +267,7 @@
map_types (Envir.subst_type ty_inst) trm
end
-fun is_eq (Const (@{const_name "op ="}, _)) = true
+fun is_eq (Const (@{const_name HOL.eq}, _)) = true
| is_eq _ = false
fun mk_rel_compose (trm1, trm2) =
@@ -539,12 +539,12 @@
end
| (* equalities need to be replaced by appropriate equivalence relations *)
- (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) =>
+ (Const (@{const_name HOL.eq}, ty), Const (@{const_name HOL.eq}, ty')) =>
if ty = ty' then rtrm
else equiv_relation ctxt (domain_type ty, domain_type ty')
| (* in this case we just check whether the given equivalence relation is correct *)
- (rel, Const (@{const_name "op ="}, ty')) =>
+ (rel, Const (@{const_name HOL.eq}, ty')) =>
let
val rel_ty = fastype_of rel
val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty')
@@ -680,7 +680,7 @@
if T = T' then rtrm
else mk_repabs ctxt (T, T') rtrm
- | (_, Const (@{const_name "op ="}, _)) => rtrm
+ | (_, Const (@{const_name HOL.eq}, _)) => rtrm
| (_, Const (_, T')) =>
let
--- a/src/HOL/Tools/SMT/smt_monomorph.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_monomorph.ML Mon Aug 30 09:35:30 2010 +0200
@@ -16,7 +16,7 @@
val ignored = member (op =) [
@{const_name All}, @{const_name Ex}, @{const_name Let}, @{const_name If},
- @{const_name "op ="}, @{const_name zero_class.zero},
+ @{const_name HOL.eq}, @{const_name zero_class.zero},
@{const_name one_class.one}, @{const_name number_of}]
fun is_const f (n, T) = not (ignored n) andalso f T
--- a/src/HOL/Tools/SMT/smt_normalize.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Mon Aug 30 09:35:30 2010 +0200
@@ -252,7 +252,7 @@
fun norm_def ctxt thm =
(case Thm.prop_of thm of
- @{term Trueprop} $ (Const (@{const_name "op ="}, _) $ _ $ Abs _) =>
+ @{term Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Abs _) =>
norm_def ctxt (thm RS @{thm fun_cong})
| Const (@{const_name "=="}, _) $ _ $ Abs _ =>
norm_def ctxt (thm RS @{thm meta_eq_to_obj_eq})
--- a/src/HOL/Tools/SMT/smtlib_interface.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML Mon Aug 30 09:35:30 2010 +0200
@@ -162,12 +162,12 @@
| conn @{const_name HOL.conj} = SOME "and"
| conn @{const_name HOL.disj} = SOME "or"
| conn @{const_name HOL.implies} = SOME "implies"
- | conn @{const_name "op ="} = SOME "iff"
+ | conn @{const_name HOL.eq} = SOME "iff"
| conn @{const_name If} = SOME "if_then_else"
| conn _ = NONE
fun pred @{const_name distinct} _ = SOME "distinct"
- | pred @{const_name "op ="} _ = SOME "="
+ | pred @{const_name HOL.eq} _ = SOME "="
| pred @{const_name term_eq} _ = SOME "="
| pred @{const_name less} T = if_int_type T "<"
| pred @{const_name less_eq} T = if_int_type T "<="
--- a/src/HOL/Tools/SMT/z3_interface.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_interface.ML Mon Aug 30 09:35:30 2010 +0200
@@ -176,7 +176,7 @@
fun mk_nary _ cu [] = cu
| mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts)
-val eq = mk_inst_pair destT1 @{cpat "op ="}
+val eq = mk_inst_pair destT1 @{cpat HOL.eq}
fun mk_eq ct cu = Thm.mk_binop (instT' ct eq) ct cu
val if_term = mk_inst_pair (destT1 o destT2) @{cpat If}
--- a/src/HOL/Tools/SMT/z3_proof_literals.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_literals.ML Mon Aug 30 09:35:30 2010 +0200
@@ -234,7 +234,7 @@
@{term Not} $ (@{term Not} $ t) => (T.compose dnegI, lookup t)
| @{term Not} $ (@{term "op = :: bool => _"} $ t $ (@{term Not} $ u)) =>
(T.compose negIffI, lookup (iff_const $ u $ t))
- | @{term Not} $ ((eq as Const (@{const_name "op ="}, _)) $ t $ u) =>
+ | @{term Not} $ ((eq as Const (@{const_name HOL.eq}, _)) $ t $ u) =>
let fun rewr lit = lit COMP @{thm not_sym}
in (rewr, lookup (@{term Not} $ (eq $ u $ t))) end
| _ =>
--- a/src/HOL/Tools/SMT/z3_proof_tools.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML Mon Aug 30 09:35:30 2010 +0200
@@ -199,7 +199,7 @@
| @{term HOL.conj} $ _ $ _ => abstr2 cvs ct
| @{term HOL.disj} $ _ $ _ => abstr2 cvs ct
| @{term HOL.implies} $ _ $ _ => abstr2 cvs ct
- | Const (@{const_name "op ="}, _) $ _ $ _ => abstr2 cvs ct
+ | Const (@{const_name HOL.eq}, _) $ _ $ _ => abstr2 cvs ct
| Const (@{const_name distinct}, _) $ _ =>
if ext_logic then abs_arg (abs_list abstr fresh_abstraction) cvs ct
else fresh_abstraction cvs ct
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Mon Aug 30 09:35:30 2010 +0200
@@ -83,7 +83,7 @@
(Cf. "extensionalize_term" in "Sledgehammer_Translate".) *)
fun extensionalize_theorem th =
case prop_of th of
- _ $ (Const (@{const_name "op ="}, Type (_, [Type (@{type_name fun}, _), _]))
+ _ $ (Const (@{const_name HOL.eq}, Type (_, [Type (@{type_name fun}, _), _]))
$ _ $ Abs (s, _, _)) => extensionalize_theorem (th RS fun_cong_all)
| _ => th
--- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Mon Aug 30 09:35:30 2010 +0200
@@ -94,7 +94,7 @@
val const_trans_table =
Symtab.make [(@{type_name Product_Type.prod}, "prod"),
(@{type_name Sum_Type.sum}, "sum"),
- (@{const_name "op ="}, "equal"),
+ (@{const_name HOL.eq}, "equal"),
(@{const_name HOL.conj}, "and"),
(@{const_name HOL.disj}, "or"),
(@{const_name HOL.implies}, "implies"),
@@ -111,7 +111,7 @@
(* Invert the table of translations between Isabelle and ATPs. *)
val const_trans_table_inv =
- Symtab.update ("fequal", @{const_name "op ="})
+ Symtab.update ("fequal", @{const_name HOL.eq})
(Symtab.make (map swap (Symtab.dest const_trans_table)))
val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
@@ -185,8 +185,8 @@
SOME c' => c'
| NONE => ascii_of c
-(* "op =" MUST BE "equal" because it's built into ATPs. *)
-fun make_fixed_const @{const_name "op ="} = "equal"
+(* HOL.eq MUST BE "equal" because it's built into ATPs. *)
+fun make_fixed_const @{const_name HOL.eq} = "equal"
| make_fixed_const c = const_prefix ^ lookup_const c
fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Aug 30 09:35:30 2010 +0200
@@ -224,7 +224,7 @@
fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
-fun smart_invert_const "fequal" = @{const_name "op ="}
+fun smart_invert_const "fequal" = @{const_name HOL.eq}
| smart_invert_const s = invert_const s
fun hol_type_from_metis_term _ (Metis.Term.Var v) =
@@ -264,7 +264,7 @@
end
| tm_to_tt (Metis.Term.Fn (fname, args)) = applic_to_tt (fname,args)
and applic_to_tt ("=",ts) =
- Term (list_comb(Const (@{const_name "op ="}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
+ Term (list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
| applic_to_tt (a,ts) =
case strip_prefix_and_unascii const_prefix a of
SOME b =>
@@ -311,7 +311,7 @@
SOME w => mk_var(w, dummyT)
| NONE => mk_var(v, dummyT))
| cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) =
- Const (@{const_name "op ="}, HOLogic.typeT)
+ Const (@{const_name HOL.eq}, HOLogic.typeT)
| cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
(case strip_prefix_and_unascii const_prefix x of
SOME c => Const (smart_invert_const c, dummyT)
@@ -325,7 +325,7 @@
cvt tm1 $ cvt tm2
| cvt (Metis.Term.Fn ("{}", [arg])) = cvt arg (*hBOOL*)
| cvt (Metis.Term.Fn ("=", [tm1,tm2])) =
- list_comb(Const (@{const_name "op ="}, HOLogic.typeT), map cvt [tm1,tm2])
+ list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), map cvt [tm1,tm2])
| cvt (t as Metis.Term.Fn (x, [])) =
(case strip_prefix_and_unascii const_prefix x of
SOME c => Const (smart_invert_const c, dummyT)
@@ -480,7 +480,7 @@
val c_t = cterm_incr_types thy refl_idx i_t
in cterm_instantiate [(refl_x, c_t)] REFL_THM end;
-fun get_ty_arg_size _ (Const (@{const_name "op ="}, _)) = 0 (*equality has no type arguments*)
+fun get_ty_arg_size _ (Const (@{const_name HOL.eq}, _)) = 0 (*equality has no type arguments*)
| get_ty_arg_size thy (Const (c, _)) = (num_type_args thy c handle TYPE _ => 0)
| get_ty_arg_size _ _ = 0;
@@ -529,13 +529,13 @@
" isa-term: " ^ Syntax.string_of_term ctxt tm ^
" fol-term: " ^ Metis.Term.toString t)
fun path_finder FO tm ps _ = path_finder_FO tm ps
- | path_finder HO (tm as Const(@{const_name "op ="},_) $ _ $ _) (p::ps) _ =
+ | path_finder HO (tm as Const(@{const_name HOL.eq},_) $ _ $ _) (p::ps) _ =
(*equality: not curried, as other predicates are*)
if p=0 then path_finder_HO tm (0::1::ps) (*select first operand*)
else path_finder_HO tm (p::ps) (*1 selects second operand*)
| path_finder HO tm (_ :: ps) (Metis.Term.Fn ("{}", [_])) =
path_finder_HO tm ps (*if not equality, ignore head to skip hBOOL*)
- | path_finder FT (tm as Const(@{const_name "op ="}, _) $ _ $ _) (p::ps)
+ | path_finder FT (tm as Const(@{const_name HOL.eq}, _) $ _ $ _) (p::ps)
(Metis.Term.Fn ("=", [t1,t2])) =
(*equality: not curried, as other predicates are*)
if p=0 then path_finder_FT tm (0::1::ps)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Aug 30 09:35:30 2010 +0200
@@ -121,7 +121,7 @@
handled specially via "fequal". *)
val boring_consts =
[@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let},
- @{const_name "op ="}]
+ @{const_name HOL.eq}]
(* Add a pconstant to the table, but a [] entry means a standard
connective, which we ignore.*)
@@ -177,7 +177,7 @@
| @{const HOL.disj} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
| @{const HOL.implies} $ t1 $ t2 =>
do_formula (flip pos) t1 #> do_formula pos t2
- | Const (@{const_name "op ="}, Type (_, [T, _])) $ t1 $ t2 =>
+ | Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t1 $ t2 =>
fold (do_term_or_formula T) [t1, t2]
| Const (@{const_name If}, Type (_, [_, Type (_, [T, _])]))
$ t1 $ t2 $ t3 =>
@@ -557,7 +557,7 @@
| (_, @{const Not} $ t1) => do_formula (not pos) t1
| (true, @{const HOL.disj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
| (false, @{const HOL.conj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
- | (true, Const (@{const_name "op ="}, _) $ t1 $ t2) => do_equals t1 t2
+ | (true, Const (@{const_name HOL.eq}, _) $ t1 $ t2) => do_equals t1 t2
| (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2
| _ => false
in do_formula true end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon Aug 30 09:35:30 2010 +0200
@@ -315,7 +315,7 @@
| _ => raise FO_TERM us
else case strip_prefix_and_unascii const_prefix a of
SOME "equal" =>
- list_comb (Const (@{const_name "op ="}, HOLogic.typeT),
+ list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT),
map (aux NONE []) us)
| SOME b =>
let
@@ -527,7 +527,7 @@
| is_bad_free _ _ = false
(* Vampire is keen on producing these. *)
-fun is_trivial_formula (@{const Not} $ (Const (@{const_name "op ="}, _)
+fun is_trivial_formula (@{const Not} $ (Const (@{const_name HOL.eq}, _)
$ t1 $ t2)) = (t1 aconv t2)
| is_trivial_formula _ = false
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Mon Aug 30 09:35:30 2010 +0200
@@ -73,7 +73,7 @@
| @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2
| @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2
| @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2
- | Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
+ | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
do_conn bs AIff t1 t2
| _ => (fn ts => do_term bs (Envir.eta_contract t)
|>> AAtom ||> union (op =) ts)
@@ -97,7 +97,7 @@
| aux j (t as Const (s, Type (_, [Type (_, [_, T']),
Type (_, [_, res_T])]))
$ t2 $ Abs (var_s, var_T, t')) =
- if s = @{const_name "op ="} orelse s = @{const_name "=="} then
+ if s = @{const_name HOL.eq} orelse s = @{const_name "=="} then
let val var_t = Var ((var_s, j), var_T) in
Const (s, T' --> T' --> res_T)
$ betapply (t2, var_t) $ subst_bound (var_t, t')
@@ -128,7 +128,7 @@
| (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
| (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
| (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
- | (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])))
+ | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
$ t1 $ t2 =>
t0 $ aux Ts t1 $ aux Ts t2
| _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
--- a/src/HOL/Tools/TFL/dcterm.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/TFL/dcterm.ML Mon Aug 30 09:35:30 2010 +0200
@@ -127,7 +127,7 @@
val dest_neg = dest_monop @{const_name Not}
val dest_pair = dest_binop @{const_name Pair}
-val dest_eq = dest_binop @{const_name "op ="}
+val dest_eq = dest_binop @{const_name HOL.eq}
val dest_imp = dest_binop @{const_name HOL.implies}
val dest_conj = dest_binop @{const_name HOL.conj}
val dest_disj = dest_binop @{const_name HOL.disj}
--- a/src/HOL/Tools/TFL/post.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/TFL/post.ML Mon Aug 30 09:35:30 2010 +0200
@@ -67,7 +67,7 @@
val P_imp_P_eq_True = @{thm eqTrueI} RS eq_reflection;
fun mk_meta_eq r = case concl_of r of
Const("==",_)$_$_ => r
- | _ $(Const(@{const_name "op ="},_)$_$_) => r RS eq_reflection
+ | _ $(Const(@{const_name HOL.eq},_)$_$_) => r RS eq_reflection
| _ => r RS P_imp_P_eq_True
(*Is this the best way to invoke the simplifier??*)
--- a/src/HOL/Tools/TFL/usyntax.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/TFL/usyntax.ML Mon Aug 30 09:35:30 2010 +0200
@@ -244,7 +244,7 @@
end
| dest_abs _ _ = raise USYN_ERR "dest_abs" "not an abstraction";
-fun dest_eq(Const(@{const_name "op ="},_) $ M $ N) = {lhs=M, rhs=N}
+fun dest_eq(Const(@{const_name HOL.eq},_) $ M $ N) = {lhs=M, rhs=N}
| dest_eq _ = raise USYN_ERR "dest_eq" "not an equality";
fun dest_imp(Const(@{const_name HOL.implies},_) $ M $ N) = {ant=M, conseq=N}
--- a/src/HOL/Tools/cnf_funcs.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML Mon Aug 30 09:35:30 2010 +0200
@@ -98,7 +98,7 @@
| is_atom (Const (@{const_name HOL.conj}, _) $ _ $ _) = false
| is_atom (Const (@{const_name HOL.disj}, _) $ _ $ _) = false
| is_atom (Const (@{const_name HOL.implies}, _) $ _ $ _) = false
- | is_atom (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ _ $ _) = false
+ | is_atom (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ _ $ _) = false
| is_atom (Const (@{const_name Not}, _) $ _) = false
| is_atom _ = true;
@@ -205,7 +205,7 @@
in
make_nnf_imp OF [thm1, thm2]
end
- | make_nnf_thm thy (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ x $ y) =
+ | make_nnf_thm thy (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ x $ y) =
let
val thm1 = make_nnf_thm thy x
val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
@@ -239,7 +239,7 @@
in
make_nnf_not_imp OF [thm1, thm2]
end
- | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ x $ y)) =
+ | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ x $ y)) =
let
val thm1 = make_nnf_thm thy x
val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
--- a/src/HOL/Tools/groebner.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/groebner.ML Mon Aug 30 09:35:30 2010 +0200
@@ -409,7 +409,7 @@
| _ => false;
fun is_eq t =
case term_of t of
- (Const(@{const_name "op ="},_)$_$_) => true
+ (Const(@{const_name HOL.eq},_)$_$_) => true
| _ => false;
fun end_itlist f l =
@@ -923,7 +923,7 @@
fun find_term bounds tm =
(case term_of tm of
- Const (@{const_name "op ="}, T) $ _ $ _ =>
+ Const (@{const_name HOL.eq}, T) $ _ $ _ =>
if domain_type T = HOLogic.boolT then find_args bounds tm
else dest_arg tm
| Const (@{const_name Not}, _) $ _ => find_term bounds (dest_arg tm)
@@ -985,7 +985,7 @@
local
fun lhs t = case term_of t of
- Const(@{const_name "op ="},_)$_$_ => Thm.dest_arg1 t
+ Const(@{const_name HOL.eq},_)$_$_ => Thm.dest_arg1 t
| _=> raise CTERM ("ideal_tac - lhs",[t])
fun exitac NONE = no_tac
| exitac (SOME y) = rtac (instantiate' [SOME (ctyp_of_term y)] [NONE,SOME y] exI) 1
--- a/src/HOL/Tools/hologic.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/hologic.ML Mon Aug 30 09:35:30 2010 +0200
@@ -236,10 +236,10 @@
fun dest_not (Const ("HOL.Not", _) $ t) = t
| dest_not t = raise TERM ("dest_not", [t]);
-fun eq_const T = Const ("op =", T --> T --> boolT);
+fun eq_const T = Const ("HOL.eq", T --> T --> boolT);
fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
-fun dest_eq (Const ("op =", _) $ lhs $ rhs) = (lhs, rhs)
+fun dest_eq (Const ("HOL.eq", _) $ lhs $ rhs) = (lhs, rhs)
| dest_eq t = raise TERM ("dest_eq", [t])
fun all_const T = Const ("HOL.All", [T --> boolT] ---> boolT);
--- a/src/HOL/Tools/inductive.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/inductive.ML Mon Aug 30 09:35:30 2010 +0200
@@ -182,7 +182,7 @@
in
case concl_of thm of
Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq)
- | _ $ (Const (@{const_name "op ="}, _) $ _ $ _) => eq2mono thm
+ | _ $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => eq2mono thm
| _ $ (Const (@{const_name Orderings.less_eq}, _) $ _ $ _) =>
dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
(resolve_tac [@{thm le_funI}, @{thm le_boolI'}])) thm))
--- a/src/HOL/Tools/inductive_codegen.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Mon Aug 30 09:35:30 2010 +0200
@@ -52,7 +52,7 @@
fun thyname_of s = (case optmod of
NONE => Codegen.thyname_of_const thy s | SOME s => s);
in (case Option.map strip_comb (try HOLogic.dest_Trueprop (concl_of thm)) of
- SOME (Const (@{const_name "op ="}, _), [t, _]) =>
+ SOME (Const (@{const_name HOL.eq}, _), [t, _]) =>
(case head_of t of
Const (s, _) =>
CodegenData.put {intros = intros, graph = graph,
@@ -188,7 +188,7 @@
end)) (AList.lookup op = modes name)
in (case strip_comb t of
- (Const (@{const_name "op ="}, Type (_, [T, _])), _) =>
+ (Const (@{const_name HOL.eq}, Type (_, [T, _])), _) =>
[Mode ((([], [1]), false), [1], []), Mode ((([], [2]), false), [2], [])] @
(if is_eqT T then [Mode ((([], [1, 2]), false), [1, 2], [])] else [])
| (Const (name, _), args) => the_default default (mk_modes name args)
@@ -344,7 +344,7 @@
end;
fun modename module s (iss, is) gr =
- let val (id, gr') = if s = @{const_name "op ="} then (("", "equal"), gr)
+ let val (id, gr') = if s = @{const_name HOL.eq} then (("", "equal"), gr)
else mk_const_id module s gr
in (space_implode "__"
(mk_qual_id module id ::
@@ -363,7 +363,7 @@
| compile_expr thy defs dep module brack modes (SOME (Mode ((mode, _), _, ms)), t) gr =
(case strip_comb t of
(Const (name, _), args) =>
- if name = @{const_name "op ="} orelse AList.defined op = modes name then
+ if name = @{const_name HOL.eq} orelse AList.defined op = modes name then
let
val (args1, args2) = chop (length ms) args;
val ((ps, mode_id), gr') = gr |> fold_map
@@ -581,7 +581,7 @@
fun dest_prem (_ $ (Const (@{const_name Set.member}, _) $ t $ u)) =
Prem ([t], Envir.beta_eta_contract u, true)
- | dest_prem (_ $ ((eq as Const (@{const_name "op ="}, _)) $ t $ u)) =
+ | dest_prem (_ $ ((eq as Const (@{const_name HOL.eq}, _)) $ t $ u)) =
Prem ([t, u], eq, false)
| dest_prem (_ $ t) =
(case strip_comb t of
--- a/src/HOL/Tools/inductive_set.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/inductive_set.ML Mon Aug 30 09:35:30 2010 +0200
@@ -265,7 +265,7 @@
fun add ctxt thm (tab as {to_set_simps, to_pred_simps, set_arities, pred_arities}) =
case prop_of thm of
- Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, Type (_, [T, _])) $ lhs $ rhs) =>
+ Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, Type (_, [T, _])) $ lhs $ rhs) =>
(case body_type T of
@{typ bool} =>
let
--- a/src/HOL/Tools/int_arith.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/int_arith.ML Mon Aug 30 09:35:30 2010 +0200
@@ -51,7 +51,7 @@
fun check (Const (@{const_name Groups.one}, @{typ int})) = false
| check (Const (@{const_name Groups.one}, _)) = true
- | check (Const (s, _)) = member (op =) [@{const_name "op ="},
+ | check (Const (s, _)) = member (op =) [@{const_name HOL.eq},
@{const_name Groups.times}, @{const_name Groups.uminus},
@{const_name Groups.minus}, @{const_name Groups.plus},
@{const_name Groups.zero},
--- a/src/HOL/Tools/lin_arith.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/lin_arith.ML Mon Aug 30 09:35:30 2010 +0200
@@ -229,7 +229,7 @@
case rel of
@{const_name Orderings.less} => SOME (p, i, "<", q, j)
| @{const_name Orderings.less_eq} => SOME (p, i, "<=", q, j)
- | "op =" => SOME (p, i, "=", q, j)
+ | @{const_name HOL.eq} => SOME (p, i, "=", q, j)
| _ => NONE
end handle Rat.DIVZERO => NONE;
@@ -427,7 +427,7 @@
val t2' = incr_boundvars 1 t2
val t1_lt_t2 = Const (@{const_name Orderings.less},
split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
- val t1_eq_t2_plus_d = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
+ val t1_eq_t2_plus_d = Const (@{const_name HOL.eq}, split_type --> split_type --> HOLogic.boolT) $ t1' $
(Const (@{const_name Groups.plus},
split_type --> split_type --> split_type) $ t2' $ d)
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
@@ -447,7 +447,7 @@
(map (incr_boundvars 1) rev_terms)
val terms2 = map (subst_term [(split_term, zero_nat)]) rev_terms
val t1' = incr_boundvars 1 t1
- val t1_eq_nat_n = Const (@{const_name "op ="}, HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $
+ val t1_eq_nat_n = Const (@{const_name HOL.eq}, HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $
(Const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) $ n)
val t1_lt_zero = Const (@{const_name Orderings.less},
HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int
@@ -471,13 +471,13 @@
(map (incr_boundvars 2) rev_terms)
val t1' = incr_boundvars 2 t1
val t2' = incr_boundvars 2 t2
- val t2_eq_zero = Const (@{const_name "op ="},
+ val t2_eq_zero = Const (@{const_name HOL.eq},
split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
- val t2_neq_zero = HOLogic.mk_not (Const (@{const_name "op ="},
+ val t2_neq_zero = HOLogic.mk_not (Const (@{const_name HOL.eq},
split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
val j_lt_t2 = Const (@{const_name Orderings.less},
split_type --> split_type--> HOLogic.boolT) $ j $ t2'
- val t1_eq_t2_times_i_plus_j = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
+ val t1_eq_t2_times_i_plus_j = Const (@{const_name HOL.eq}, split_type --> split_type --> HOLogic.boolT) $ t1' $
(Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
(Const (@{const_name Groups.times},
split_type --> split_type --> split_type) $ t2' $ i) $ j)
@@ -503,13 +503,13 @@
(map (incr_boundvars 2) rev_terms)
val t1' = incr_boundvars 2 t1
val t2' = incr_boundvars 2 t2
- val t2_eq_zero = Const (@{const_name "op ="},
+ val t2_eq_zero = Const (@{const_name HOL.eq},
split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
- val t2_neq_zero = HOLogic.mk_not (Const (@{const_name "op ="},
+ val t2_neq_zero = HOLogic.mk_not (Const (@{const_name HOL.eq},
split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
val j_lt_t2 = Const (@{const_name Orderings.less},
split_type --> split_type--> HOLogic.boolT) $ j $ t2'
- val t1_eq_t2_times_i_plus_j = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
+ val t1_eq_t2_times_i_plus_j = Const (@{const_name HOL.eq}, split_type --> split_type --> HOLogic.boolT) $ t1' $
(Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
(Const (@{const_name Groups.times},
split_type --> split_type --> split_type) $ t2' $ i) $ j)
@@ -541,7 +541,7 @@
(map (incr_boundvars 2) rev_terms)
val t1' = incr_boundvars 2 t1
val t2' = incr_boundvars 2 t2
- val t2_eq_zero = Const (@{const_name "op ="},
+ val t2_eq_zero = Const (@{const_name HOL.eq},
split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
val zero_lt_t2 = Const (@{const_name Orderings.less},
split_type --> split_type --> HOLogic.boolT) $ zero $ t2'
@@ -555,7 +555,7 @@
split_type --> split_type--> HOLogic.boolT) $ j $ t2'
val t2_lt_j = Const (@{const_name Orderings.less},
split_type --> split_type--> HOLogic.boolT) $ t2' $ j
- val t1_eq_t2_times_i_plus_j = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
+ val t1_eq_t2_times_i_plus_j = Const (@{const_name HOL.eq}, split_type --> split_type --> HOLogic.boolT) $ t1' $
(Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
(Const (@{const_name Groups.times},
split_type --> split_type --> split_type) $ t2' $ i) $ j)
@@ -595,7 +595,7 @@
(map (incr_boundvars 2) rev_terms)
val t1' = incr_boundvars 2 t1
val t2' = incr_boundvars 2 t2
- val t2_eq_zero = Const (@{const_name "op ="},
+ val t2_eq_zero = Const (@{const_name HOL.eq},
split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
val zero_lt_t2 = Const (@{const_name Orderings.less},
split_type --> split_type --> HOLogic.boolT) $ zero $ t2'
@@ -609,7 +609,7 @@
split_type --> split_type--> HOLogic.boolT) $ j $ t2'
val t2_lt_j = Const (@{const_name Orderings.less},
split_type --> split_type--> HOLogic.boolT) $ t2' $ j
- val t1_eq_t2_times_i_plus_j = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
+ val t1_eq_t2_times_i_plus_j = Const (@{const_name HOL.eq}, split_type --> split_type --> HOLogic.boolT) $ t1' $
(Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
(Const (@{const_name Groups.times},
split_type --> split_type --> split_type) $ t2' $ i) $ j)
--- a/src/HOL/Tools/meson.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/meson.ML Mon Aug 30 09:35:30 2010 +0200
@@ -183,7 +183,7 @@
fun signed_lits th = signed_lits_aux (HOLogic.dest_Trueprop (concl_of th)) ([],[]);
(*Literals like X=X are tautologous*)
-fun taut_poslit (Const(@{const_name "op ="},_) $ t $ u) = t aconv u
+fun taut_poslit (Const(@{const_name HOL.eq},_) $ t $ u) = t aconv u
| taut_poslit (Const(@{const_name True},_)) = true
| taut_poslit _ = false;
@@ -213,7 +213,7 @@
case HOLogic.dest_Trueprop (concl_of th) of
(Const (@{const_name HOL.disj}, _) $ (Const (@{const_name HOL.disj}, _) $ _ $ _) $ _) =>
refl_clause_aux n (th RS disj_assoc) (*isolate an atom as first disjunct*)
- | (Const (@{const_name HOL.disj}, _) $ (Const(@{const_name Not},_) $ (Const(@{const_name "op ="},_) $ t $ u)) $ _) =>
+ | (Const (@{const_name HOL.disj}, _) $ (Const(@{const_name Not},_) $ (Const(@{const_name HOL.eq},_) $ t $ u)) $ _) =>
if eliminable(t,u)
then refl_clause_aux (n-1) (th RS not_refl_disj_D) (*Var inequation: delete*)
else refl_clause_aux (n-1) (th RS disj_comm) (*not between Vars: ignore*)
@@ -222,7 +222,7 @@
fun notequal_lits_count (Const (@{const_name HOL.disj}, _) $ P $ Q) =
notequal_lits_count P + notequal_lits_count Q
- | notequal_lits_count (Const(@{const_name Not},_) $ (Const(@{const_name "op ="},_) $ _ $ _)) = 1
+ | notequal_lits_count (Const(@{const_name Not},_) $ (Const(@{const_name HOL.eq},_) $ _ $ _)) = 1
| notequal_lits_count _ = 0;
(*Simplify a clause by applying reflexivity to its negated equality literals*)
@@ -280,7 +280,7 @@
| signed_nclauses b (Const(@{const_name HOL.implies},_) $ t $ u) =
if b then prod (signed_nclauses (not b) t) (signed_nclauses b u)
else sum (signed_nclauses (not b) t) (signed_nclauses b u)
- | signed_nclauses b (Const(@{const_name "op ="}, Type ("fun", [T, _])) $ t $ u) =
+ | signed_nclauses b (Const(@{const_name HOL.eq}, Type ("fun", [T, _])) $ t $ u) =
if T = HOLogic.boolT then (*Boolean equality is if-and-only-if*)
if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u))
(prod (signed_nclauses (not b) u) (signed_nclauses b t))
--- a/src/HOL/Tools/nat_arith.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/nat_arith.ML Mon Aug 30 09:35:30 2010 +0200
@@ -62,7 +62,7 @@
(struct
open CommonCancelSums;
val mk_bal = HOLogic.mk_eq;
- val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
+ val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT;
val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel"};
end);
--- a/src/HOL/Tools/nat_numeral_simprocs.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML Mon Aug 30 09:35:30 2010 +0200
@@ -168,7 +168,7 @@
(open CancelNumeralsCommon
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_eq
- val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
+ val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT
val bal_add1 = @{thm nat_eq_add_iff1} RS trans
val bal_add2 = @{thm nat_eq_add_iff2} RS trans
);
@@ -300,7 +300,7 @@
(open CancelNumeralFactorCommon
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_eq
- val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
+ val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT
val cancel = @{thm nat_mult_eq_cancel1} RS trans
val neg_exchanges = false
)
@@ -380,7 +380,7 @@
(open CancelFactorCommon
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_eq
- val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
+ val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT
fun simp_conv _ _ = SOME @{thm nat_mult_eq_cancel_disj}
);
--- a/src/HOL/Tools/numeral_simprocs.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML Mon Aug 30 09:35:30 2010 +0200
@@ -222,7 +222,7 @@
(open CancelNumeralsCommon
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_eq
- val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
+ val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT
val bal_add1 = @{thm eq_add_iff1} RS trans
val bal_add2 = @{thm eq_add_iff2} RS trans
);
@@ -401,7 +401,7 @@
(open CancelNumeralFactorCommon
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_eq
- val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
+ val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT
val cancel = @{thm mult_cancel_left} RS trans
val neg_exchanges = false
)
@@ -516,7 +516,7 @@
(open CancelFactorCommon
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_eq
- val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
+ val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT
fun simp_conv _ _ = SOME @{thm mult_cancel_left}
);
@@ -606,7 +606,7 @@
local
val zr = @{cpat "0"}
val zT = ctyp_of_term zr
- val geq = @{cpat "op ="}
+ val geq = @{cpat HOL.eq}
val eqT = Thm.dest_ctyp (ctyp_of_term geq) |> hd
val add_frac_eq = mk_meta_eq @{thm "add_frac_eq"}
val add_frac_num = mk_meta_eq @{thm "add_frac_num"}
@@ -676,7 +676,7 @@
val T = ctyp_of_term c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
in SOME (mk_meta_eq th) end
- | Const(@{const_name "op ="},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
+ | Const(@{const_name HOL.eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
let
val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
val _ = map is_number [a,b,c]
@@ -697,7 +697,7 @@
val T = ctyp_of_term c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
in SOME (mk_meta_eq th) end
- | Const(@{const_name "op ="},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
+ | Const(@{const_name HOL.eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
let
val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
val _ = map is_number [a,b,c]
--- a/src/HOL/Tools/recfun_codegen.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/recfun_codegen.ML Mon Aug 30 09:35:30 2010 +0200
@@ -40,7 +40,7 @@
end
| avoid_value thy thms = thms;
-fun get_equations thy defs (raw_c, T) = if raw_c = @{const_name "op ="} then ([], "") else
+fun get_equations thy defs (raw_c, T) = if raw_c = @{const_name HOL.eq} then ([], "") else
let
val c = AxClass.unoverload_const thy (raw_c, T);
val raw_thms = Code.get_cert thy (Code_Preproc.preprocess_functrans thy) c
--- a/src/HOL/Tools/record.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/record.ML Mon Aug 30 09:35:30 2010 +0200
@@ -1342,7 +1342,7 @@
val eq_simproc =
Simplifier.simproc_global @{theory HOL} "record_eq_simp" ["r = s"]
(fn thy => fn _ => fn t =>
- (case t of Const (@{const_name "op ="}, Type (_, [T, _])) $ _ $ _ =>
+ (case t of Const (@{const_name HOL.eq}, Type (_, [T, _])) $ _ $ _ =>
(case rec_id ~1 T of
"" => NONE
| name =>
@@ -1405,12 +1405,12 @@
else raise TERM ("", [x]);
val sel' = Const (sel, Tsel) $ Bound 0;
val (l, r) = if lr then (sel', x') else (x', sel');
- in Const (@{const_name "op ="}, Teq) $ l $ r end
+ in Const (@{const_name HOL.eq}, Teq) $ l $ r end
else raise TERM ("", [Const (sel, Tsel)]);
- fun dest_sel_eq (Const (@{const_name "op ="}, Teq) $ (Const (sel, Tsel) $ Bound 0) $ X) =
+ fun dest_sel_eq (Const (@{const_name HOL.eq}, Teq) $ (Const (sel, Tsel) $ Bound 0) $ X) =
(true, Teq, (sel, Tsel), X)
- | dest_sel_eq (Const (@{const_name "op ="}, Teq) $ X $ (Const (sel, Tsel) $ Bound 0)) =
+ | dest_sel_eq (Const (@{const_name HOL.eq}, Teq) $ X $ (Const (sel, Tsel) $ Bound 0)) =
(false, Teq, (sel, Tsel), X)
| dest_sel_eq _ = raise TERM ("", []);
in
@@ -1845,7 +1845,7 @@
val eq =
(HOLogic.mk_Trueprop o HOLogic.mk_eq)
(Const (@{const_name HOL.equal}, extT --> extT --> HOLogic.boolT),
- Const (@{const_name "op ="}, extT --> extT --> HOLogic.boolT));
+ Const (@{const_name HOL.eq}, extT --> extT --> HOLogic.boolT));
fun tac eq_def =
Class.intro_classes_tac []
THEN (Simplifier.rewrite_goals_tac [Simpdata.mk_eq eq_def])
--- a/src/HOL/Tools/refute.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/refute.ML Mon Aug 30 09:35:30 2010 +0200
@@ -647,7 +647,7 @@
| Const (@{const_name Hilbert_Choice.Eps}, _) => t
| Const (@{const_name All}, _) => t
| Const (@{const_name Ex}, _) => t
- | Const (@{const_name "op ="}, _) => t
+ | Const (@{const_name HOL.eq}, _) => t
| Const (@{const_name HOL.conj}, _) => t
| Const (@{const_name HOL.disj}, _) => t
| Const (@{const_name HOL.implies}, _) => t
@@ -823,7 +823,7 @@
end
| Const (@{const_name All}, T) => collect_type_axioms T axs
| Const (@{const_name Ex}, T) => collect_type_axioms T axs
- | Const (@{const_name "op ="}, T) => collect_type_axioms T axs
+ | Const (@{const_name HOL.eq}, T) => collect_type_axioms T axs
| Const (@{const_name HOL.conj}, _) => axs
| Const (@{const_name HOL.disj}, _) => axs
| Const (@{const_name HOL.implies}, _) => axs
@@ -1850,16 +1850,16 @@
end
| Const (@{const_name Ex}, _) =>
SOME (interpret thy model args (eta_expand t 1))
- | Const (@{const_name "op ="}, _) $ t1 $ t2 => (* similar to "==" (Pure) *)
+ | Const (@{const_name HOL.eq}, _) $ t1 $ t2 => (* similar to "==" (Pure) *)
let
val (i1, m1, a1) = interpret thy model args t1
val (i2, m2, a2) = interpret thy m1 a1 t2
in
SOME (make_equality (i1, i2), m2, a2)
end
- | Const (@{const_name "op ="}, _) $ t1 =>
+ | Const (@{const_name HOL.eq}, _) $ t1 =>
SOME (interpret thy model args (eta_expand t 1))
- | Const (@{const_name "op ="}, _) =>
+ | Const (@{const_name HOL.eq}, _) =>
SOME (interpret thy model args (eta_expand t 2))
| Const (@{const_name HOL.conj}, _) $ t1 $ t2 =>
(* 3-valued logic *)
--- a/src/HOL/Tools/simpdata.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/simpdata.ML Mon Aug 30 09:35:30 2010 +0200
@@ -10,7 +10,7 @@
structure Quantifier1 = Quantifier1Fun
(struct
(*abstract syntax*)
- fun dest_eq ((c as Const(@{const_name "op ="},_)) $ s $ t) = SOME (c, s, t)
+ fun dest_eq ((c as Const(@{const_name HOL.eq},_)) $ s $ t) = SOME (c, s, t)
| dest_eq _ = NONE;
fun dest_conj ((c as Const(@{const_name HOL.conj},_)) $ s $ t) = SOME (c, s, t)
| dest_conj _ = NONE;
@@ -44,7 +44,7 @@
fun mk_eq th = case concl_of th
(*expects Trueprop if not == *)
of Const (@{const_name "=="},_) $ _ $ _ => th
- | _ $ (Const (@{const_name "op ="}, _) $ _ $ _) => mk_meta_eq th
+ | _ $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => mk_meta_eq th
| _ $ (Const (@{const_name Not}, _) $ _) => th RS @{thm Eq_FalseI}
| _ => th RS @{thm Eq_TrueI}
--- a/src/HOL/ex/Meson_Test.thy Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/ex/Meson_Test.thy Mon Aug 30 09:35:30 2010 +0200
@@ -10,7 +10,7 @@
below and constants declared in HOL!
*}
-hide_const (open) implies union inter subset sum quotient
+hide_const (open) eq implies union inter subset sum quotient
text {*
Test data for the MESON proof procedure
--- a/src/HOL/ex/SVC_Oracle.thy Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/ex/SVC_Oracle.thy Mon Aug 30 09:35:30 2010 +0200
@@ -94,7 +94,7 @@
| fm ((c as Const(@{const_name Not}, _)) $ p) = c $ (fm p)
| fm ((c as Const(@{const_name True}, _))) = c
| fm ((c as Const(@{const_name False}, _))) = c
- | fm (t as Const(@{const_name "op ="}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
+ | fm (t as Const(@{const_name HOL.eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
| fm (t as Const(@{const_name Orderings.less}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
| fm (t as Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
| fm t = replace t
--- a/src/HOL/ex/svc_funcs.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/ex/svc_funcs.ML Mon Aug 30 09:35:30 2010 +0200
@@ -95,7 +95,7 @@
| Const(@{const_name Not}, _) => apply c (map tag ts)
| Const(@{const_name True}, _) => (c, false)
| Const(@{const_name False}, _) => (c, false)
- | Const(@{const_name "op ="}, Type ("fun", [T,_])) =>
+ | Const(@{const_name HOL.eq}, Type ("fun", [T,_])) =>
if T = HOLogic.boolT then
(*biconditional: with int/nat comparisons below?*)
let val [t1,t2] = ts
@@ -200,7 +200,7 @@
Buildin("AND", (*unfolding uses both polarities*)
[Buildin("=>", [fm (not pos) p, fm pos q]),
Buildin("=>", [fm (not pos) q, fm pos p])])
- | fm pos (t as Const(@{const_name "op ="}, Type ("fun", [T,_])) $ x $ y) =
+ | fm pos (t as Const(@{const_name HOL.eq}, Type ("fun", [T,_])) $ x $ y) =
let val tx = tm x and ty = tm y
in if pos orelse T = HOLogic.realT then
Buildin("=", [tx, ty])
--- a/src/HOLCF/Tools/Domain/domain_library.ML Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_library.ML Mon Aug 30 09:35:30 2010 +0200
@@ -190,9 +190,9 @@
fun mk_All (x,P) = %%:"all" $ mk_lam(x,P); (* meta universal quantification *)
-infixr 0 ===>; fun S ===> T = %%:"==>" $ S $ T;
-infix 0 ==; fun S == T = %%:"==" $ S $ T;
-infix 1 ===; fun S === T = %%:"op =" $ S $ T;
+infixr 0 ===>; fun S ===> T = %%: "==>" $ S $ T;
+infix 0 ==; fun S == T = %%: "==" $ S $ T;
+infix 1 ===; fun S === T = %%: @{const_name HOL.eq} $ S $ T;
infix 1 ~=; fun S ~= T = HOLogic.mk_not (S === T);
infix 9 ` ; fun f ` x = %%: @{const_name Rep_CFun} $ f $ x;