1.1 --- a/NEWS Sat Aug 28 20:24:40 2010 +0800
1.2 +++ b/NEWS Sat Aug 28 16:14:32 2010 +0200
1.3 @@ -136,6 +136,7 @@
1.4 op & ~> HOL.conj
1.5 op | ~> HOL.disj
1.6 op --> ~> HOL.implies
1.7 + op = ~> HOL.eq
1.8 Not ~> HOL.Not
1.9 The ~> HOL.The
1.10 All ~> HOL.All
2.1 --- a/src/HOL/Decision_Procs/Approximation.thy Sat Aug 28 20:24:40 2010 +0800
2.2 +++ b/src/HOL/Decision_Procs/Approximation.thy Sat Aug 28 16:14:32 2010 +0200
2.3 @@ -3305,7 +3305,7 @@
2.4 (Const (@{const_name Set.member}, _) $
2.5 Free (name, _) $ _)) = name
2.6 | variable_of_bound (Const (@{const_name Trueprop}, _) $
2.7 - (Const (@{const_name "op ="}, _) $
2.8 + (Const (@{const_name HOL.eq}, _) $
2.9 Free (name, _) $ _)) = name
2.10 | variable_of_bound t = raise TERM ("variable_of_bound", [t])
2.11
3.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Sat Aug 28 20:24:40 2010 +0800
3.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Sat Aug 28 16:14:32 2010 +0200
3.3 @@ -519,9 +519,9 @@
3.4 val [lt, le] = map (Morphism.term phi) [@{term "op \<sqsubset>"}, @{term "op \<sqsubseteq>"}]
3.5 fun h x t =
3.6 case term_of t of
3.7 - Const(@{const_name "op ="}, _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
3.8 + Const(@{const_name HOL.eq}, _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
3.9 else Ferrante_Rackoff_Data.Nox
3.10 - | @{term "Not"}$(Const(@{const_name "op ="}, _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
3.11 + | @{term "Not"}$(Const(@{const_name HOL.eq}, _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
3.12 else Ferrante_Rackoff_Data.Nox
3.13 | b$y$z => if Term.could_unify (b, lt) then
3.14 if term_of x aconv y then Ferrante_Rackoff_Data.Lt
3.15 @@ -771,7 +771,7 @@
3.16 in rth end
3.17 | _ => Thm.reflexive ct)
3.18
3.19 -| Const(@{const_name "op ="},_)$_$Const(@{const_name Groups.zero},_) =>
3.20 +| Const(@{const_name HOL.eq},_)$_$Const(@{const_name Groups.zero},_) =>
3.21 (case whatis x (Thm.dest_arg1 ct) of
3.22 ("c*x+t",[c,t]) =>
3.23 let
3.24 @@ -835,7 +835,7 @@
3.25 val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
3.26 in rth end
3.27
3.28 -| Const(@{const_name "op ="},_)$a$b =>
3.29 +| Const(@{const_name HOL.eq},_)$a$b =>
3.30 let val (ca,cb) = Thm.dest_binop ct
3.31 val T = ctyp_of_term ca
3.32 val th = instantiate' [SOME T] [SOME ca, SOME cb] eq_iff_diff_eq_0
3.33 @@ -844,7 +844,7 @@
3.34 (Semiring_Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
3.35 val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
3.36 in rth end
3.37 -| @{term "Not"} $(Const(@{const_name "op ="},_)$a$b) => Conv.arg_conv (field_isolate_conv phi ctxt vs) ct
3.38 +| @{term "Not"} $(Const(@{const_name HOL.eq},_)$a$b) => Conv.arg_conv (field_isolate_conv phi ctxt vs) ct
3.39 | _ => Thm.reflexive ct
3.40 end;
3.41
3.42 @@ -852,9 +852,9 @@
3.43 let
3.44 fun h x t =
3.45 case term_of t of
3.46 - Const(@{const_name "op ="}, _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
3.47 + Const(@{const_name HOL.eq}, _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
3.48 else Ferrante_Rackoff_Data.Nox
3.49 - | @{term "Not"}$(Const(@{const_name "op ="}, _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
3.50 + | @{term "Not"}$(Const(@{const_name HOL.eq}, _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
3.51 else Ferrante_Rackoff_Data.Nox
3.52 | Const(@{const_name Orderings.less},_)$y$z =>
3.53 if term_of x aconv y then Ferrante_Rackoff_Data.Lt
4.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Sat Aug 28 20:24:40 2010 +0800
4.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Sat Aug 28 16:14:32 2010 +0200
4.3 @@ -912,7 +912,7 @@
4.4
4.5 definition "lt p = (case p of CP (C c) \<Rightarrow> if 0>\<^sub>N c then T else F| _ \<Rightarrow> Lt p)"
4.6 definition "le p = (case p of CP (C c) \<Rightarrow> if 0\<ge>\<^sub>N c then T else F | _ \<Rightarrow> Le p)"
4.7 -definition "eq p = (case p of CP (C c) \<Rightarrow> if c = 0\<^sub>N then T else F | _ \<Rightarrow> Eq p)"
4.8 +definition eq where "eq p = (case p of CP (C c) \<Rightarrow> if c = 0\<^sub>N then T else F | _ \<Rightarrow> Eq p)"
4.9 definition "neq p = not (eq p)"
4.10
4.11 lemma lt: "allpolys isnpoly p \<Longrightarrow> Ifm vs bs (lt p) = Ifm vs bs (Lt p)"
4.12 @@ -2960,7 +2960,7 @@
4.13 val ifft = @{term "op = :: bool => _"}
4.14 fun llt rT = Const(@{const_name Orderings.less},rrT rT);
4.15 fun lle rT = Const(@{const_name Orderings.less},rrT rT);
4.16 -fun eqt rT = Const(@{const_name "op ="},rrT rT);
4.17 +fun eqt rT = Const(@{const_name HOL.eq},rrT rT);
4.18 fun rz rT = Const(@{const_name Groups.zero},rT);
4.19
4.20 fun dest_nat t = case t of
4.21 @@ -3021,7 +3021,7 @@
4.22 | Const(@{const_name HOL.conj},_)$p$q => @{code And} (fm_of_term m m' p, fm_of_term m m' q)
4.23 | Const(@{const_name HOL.disj},_)$p$q => @{code Or} (fm_of_term m m' p, fm_of_term m m' q)
4.24 | Const(@{const_name HOL.implies},_)$p$q => @{code Imp} (fm_of_term m m' p, fm_of_term m m' q)
4.25 - | Const(@{const_name "op ="},ty)$p$q =>
4.26 + | Const(@{const_name HOL.eq},ty)$p$q =>
4.27 if domain_type ty = bT then @{code Iff} (fm_of_term m m' p, fm_of_term m m' q)
4.28 else @{code Eq} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
4.29 | Const(@{const_name Orderings.less},_)$p$q =>
5.1 --- a/src/HOL/Decision_Procs/commutative_ring_tac.ML Sat Aug 28 20:24:40 2010 +0800
5.2 +++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML Sat Aug 28 16:14:32 2010 +0200
5.3 @@ -65,7 +65,7 @@
5.4 (* reification of the equation *)
5.5 val cr_sort = @{sort "comm_ring_1"};
5.6
5.7 -fun reif_eq thy (eq as Const(@{const_name "op ="}, Type("fun", [T, _])) $ lhs $ rhs) =
5.8 +fun reif_eq thy (eq as Const(@{const_name HOL.eq}, Type("fun", [T, _])) $ lhs $ rhs) =
5.9 if Sign.of_sort thy (T, cr_sort) then
5.10 let
5.11 val fs = OldTerm.term_frees eq;
6.1 --- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Sat Aug 28 20:24:40 2010 +0800
6.2 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Sat Aug 28 16:14:32 2010 +0200
6.3 @@ -175,7 +175,7 @@
6.4 let
6.5 fun h bounds tm =
6.6 (case term_of tm of
6.7 - Const (@{const_name "op ="}, T) $ _ $ _ =>
6.8 + Const (@{const_name HOL.eq}, T) $ _ $ _ =>
6.9 if domain_type T = HOLogic.boolT then find_args bounds tm
6.10 else Thm.dest_fun2 tm
6.11 | Const (@{const_name Not}, _) $ _ => h bounds (Thm.dest_arg tm)
7.1 --- a/src/HOL/Decision_Procs/langford.ML Sat Aug 28 20:24:40 2010 +0800
7.2 +++ b/src/HOL/Decision_Procs/langford.ML Sat Aug 28 16:14:32 2010 +0200
7.3 @@ -116,7 +116,7 @@
7.4 fun contains x ct = member (op aconv) (OldTerm.term_frees (term_of ct)) (term_of x);
7.5
7.6 fun is_eqx x eq = case term_of eq of
7.7 - Const(@{const_name "op ="},_)$l$r => l aconv term_of x orelse r aconv term_of x
7.8 + Const(@{const_name HOL.eq},_)$l$r => l aconv term_of x orelse r aconv term_of x
7.9 | _ => false ;
7.10
7.11 local
7.12 @@ -176,7 +176,7 @@
7.13 let
7.14 fun h bounds tm =
7.15 (case term_of tm of
7.16 - Const (@{const_name "op ="}, T) $ _ $ _ =>
7.17 + Const (@{const_name HOL.eq}, T) $ _ $ _ =>
7.18 if domain_type T = HOLogic.boolT then find_args bounds tm
7.19 else Thm.dest_fun2 tm
7.20 | Const (@{const_name Not}, _) $ _ => h bounds (Thm.dest_arg tm)
8.1 --- a/src/HOL/HOL.thy Sat Aug 28 20:24:40 2010 +0800
8.2 +++ b/src/HOL/HOL.thy Sat Aug 28 16:14:32 2010 +0200
8.3 @@ -61,14 +61,8 @@
8.4 disj :: "[bool, bool] => bool" (infixr "|" 30)
8.5 implies :: "[bool, bool] => bool" (infixr "-->" 25)
8.6
8.7 -setup Sign.root_path
8.8 + eq :: "['a, 'a] => bool" (infixl "=" 50)
8.9
8.10 -consts
8.11 - "op =" :: "['a, 'a] => bool" (infixl "=" 50)
8.12 -
8.13 -setup Sign.local_path
8.14 -
8.15 -consts
8.16 The :: "('a => bool) => 'a"
8.17 All :: "('a => bool) => bool" (binder "ALL " 10)
8.18 Ex :: "('a => bool) => bool" (binder "EX " 10)
8.19 @@ -78,7 +72,7 @@
8.20 subsubsection {* Additional concrete syntax *}
8.21
8.22 notation (output)
8.23 - "op =" (infix "=" 50)
8.24 + eq (infix "=" 50)
8.25
8.26 abbreviation
8.27 not_equal :: "['a, 'a] => bool" (infixl "~=" 50) where
8.28 @@ -89,15 +83,15 @@
8.29
8.30 notation (xsymbols)
8.31 Not ("\<not> _" [40] 40) and
8.32 - HOL.conj (infixr "\<and>" 35) and
8.33 - HOL.disj (infixr "\<or>" 30) and
8.34 - HOL.implies (infixr "\<longrightarrow>" 25) and
8.35 + conj (infixr "\<and>" 35) and
8.36 + disj (infixr "\<or>" 30) and
8.37 + implies (infixr "\<longrightarrow>" 25) and
8.38 not_equal (infix "\<noteq>" 50)
8.39
8.40 notation (HTML output)
8.41 Not ("\<not> _" [40] 40) and
8.42 - HOL.conj (infixr "\<and>" 35) and
8.43 - HOL.disj (infixr "\<or>" 30) and
8.44 + conj (infixr "\<and>" 35) and
8.45 + disj (infixr "\<or>" 30) and
8.46 not_equal (infix "\<noteq>" 50)
8.47
8.48 abbreviation (iff)
8.49 @@ -183,8 +177,8 @@
8.50 True_or_False: "(P=True) | (P=False)"
8.51
8.52 finalconsts
8.53 - "op ="
8.54 - HOL.implies
8.55 + eq
8.56 + implies
8.57 The
8.58
8.59 definition If :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" ("(if (_)/ then (_)/ else (_))" [0, 0, 10] 10) where
8.60 @@ -864,7 +858,7 @@
8.61
8.62 setup {*
8.63 let
8.64 - fun non_bool_eq (@{const_name "op ="}, Type (_, [T, _])) = T <> @{typ bool}
8.65 + fun non_bool_eq (@{const_name HOL.eq}, Type (_, [T, _])) = T <> @{typ bool}
8.66 | non_bool_eq _ = false;
8.67 val hyp_subst_tac' =
8.68 SUBGOAL (fn (goal, i) =>
8.69 @@ -930,7 +924,7 @@
8.70 (
8.71 val thy = @{theory}
8.72 type claset = Classical.claset
8.73 - val equality_name = @{const_name "op ="}
8.74 + val equality_name = @{const_name HOL.eq}
8.75 val not_name = @{const_name Not}
8.76 val notE = @{thm notE}
8.77 val ccontr = @{thm ccontr}
8.78 @@ -1746,8 +1740,8 @@
8.79
8.80 fun eq_codegen thy defs dep thyname b t gr =
8.81 (case strip_comb t of
8.82 - (Const (@{const_name "op ="}, Type (_, [Type ("fun", _), _])), _) => NONE
8.83 - | (Const (@{const_name "op ="}, _), [t, u]) =>
8.84 + (Const (@{const_name HOL.eq}, Type (_, [Type ("fun", _), _])), _) => NONE
8.85 + | (Const (@{const_name HOL.eq}, _), [t, u]) =>
8.86 let
8.87 val (pt, gr') = Codegen.invoke_codegen thy defs dep thyname false t gr;
8.88 val (pu, gr'') = Codegen.invoke_codegen thy defs dep thyname false u gr';
8.89 @@ -1756,7 +1750,7 @@
8.90 SOME (Codegen.parens
8.91 (Pretty.block [pt, Codegen.str " =", Pretty.brk 1, pu]), gr''')
8.92 end
8.93 - | (t as Const (@{const_name "op ="}, _), ts) => SOME (Codegen.invoke_codegen
8.94 + | (t as Const (@{const_name HOL.eq}, _), ts) => SOME (Codegen.invoke_codegen
8.95 thy defs dep thyname b (Codegen.eta_expand t ts 2) gr)
8.96 | _ => NONE);
8.97
8.98 @@ -1796,7 +1790,7 @@
8.99
8.100 setup {*
8.101 Code_Preproc.map_pre (fn simpset =>
8.102 - simpset addsimprocs [Simplifier.simproc_global_i @{theory} "equal" [@{term "op ="}]
8.103 + simpset addsimprocs [Simplifier.simproc_global_i @{theory} "equal" [@{term HOL.eq}]
8.104 (fn thy => fn _ => fn Const (_, T) => case strip_type T
8.105 of (Type _ :: _, _) => SOME @{thm eq_equal}
8.106 | _ => NONE)])
8.107 @@ -1944,7 +1938,7 @@
8.108 code_const "HOL.equal"
8.109 (Haskell infixl 4 "==")
8.110
8.111 -code_const "op ="
8.112 +code_const HOL.eq
8.113 (Haskell infixl 4 "==")
8.114
8.115 text {* undefined *}
9.1 --- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Sat Aug 28 20:24:40 2010 +0800
9.2 +++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Sat Aug 28 16:14:32 2010 +0200
9.3 @@ -53,7 +53,7 @@
9.4 F > False
9.5 ONE_ONE > HOL4Setup.ONE_ONE
9.6 ONTO > Fun.surj
9.7 - "=" > "op ="
9.8 + "=" > HOL.eq
9.9 "==>" > HOL.implies
9.10 "/\\" > HOL.conj
9.11 "\\/" > HOL.disj
10.1 --- a/src/HOL/Import/HOLLight/hollight.imp Sat Aug 28 20:24:40 2010 +0800
10.2 +++ b/src/HOL/Import/HOLLight/hollight.imp Sat Aug 28 16:14:32 2010 +0200
10.3 @@ -234,7 +234,7 @@
10.4 ">=" > "HOLLight.hollight.>="
10.5 ">" > "HOLLight.hollight.>"
10.6 "==>" > HOL.implies
10.7 - "=" > "op ="
10.8 + "=" > HOL.eq
10.9 "<=" > "HOLLight.hollight.<="
10.10 "<" > "HOLLight.hollight.<"
10.11 "/\\" > HOL.conj
11.1 --- a/src/HOL/Import/hol4rews.ML Sat Aug 28 20:24:40 2010 +0800
11.2 +++ b/src/HOL/Import/hol4rews.ML Sat Aug 28 16:14:32 2010 +0200
11.3 @@ -627,7 +627,7 @@
11.4 thy |> add_hol4_type_mapping "min" "bool" false @{type_name bool}
11.5 |> add_hol4_type_mapping "min" "fun" false "fun"
11.6 |> add_hol4_type_mapping "min" "ind" false @{type_name ind}
11.7 - |> add_hol4_const_mapping "min" "=" false @{const_name "op ="}
11.8 + |> add_hol4_const_mapping "min" "=" false @{const_name HOL.eq}
11.9 |> add_hol4_const_mapping "min" "==>" false @{const_name HOL.implies}
11.10 |> add_hol4_const_mapping "min" "@" false @{const_name "Eps"}
11.11 in
12.1 --- a/src/HOL/Import/proof_kernel.ML Sat Aug 28 20:24:40 2010 +0800
12.2 +++ b/src/HOL/Import/proof_kernel.ML Sat Aug 28 16:14:32 2010 +0200
12.3 @@ -1205,7 +1205,7 @@
12.4 fun non_trivial_term_consts t = fold_aterms
12.5 (fn Const (c, _) =>
12.6 if c = @{const_name Trueprop} orelse c = @{const_name All}
12.7 - orelse c = @{const_name HOL.implies} orelse c = @{const_name HOL.conj} orelse c = @{const_name "op ="}
12.8 + orelse c = @{const_name HOL.implies} orelse c = @{const_name HOL.conj} orelse c = @{const_name HOL.eq}
12.9 then I else insert (op =) c
12.10 | _ => I) t [];
12.11
12.12 @@ -1213,7 +1213,7 @@
12.13 let
12.14 fun add_consts (Const (c, _), cs) =
12.15 (case c of
12.16 - @{const_name "op ="} => insert (op =) "==" cs
12.17 + @{const_name HOL.eq} => insert (op =) "==" cs
12.18 | @{const_name HOL.implies} => insert (op =) "==>" cs
12.19 | @{const_name All} => cs
12.20 | "all" => cs
12.21 @@ -1476,10 +1476,10 @@
12.22 fun mk_COMB th1 th2 thy =
12.23 let
12.24 val (f,g) = case concl_of th1 of
12.25 - _ $ (Const(@{const_name "op ="},_) $ f $ g) => (f,g)
12.26 + _ $ (Const(@{const_name HOL.eq},_) $ f $ g) => (f,g)
12.27 | _ => raise ERR "mk_COMB" "First theorem not an equality"
12.28 val (x,y) = case concl_of th2 of
12.29 - _ $ (Const(@{const_name "op ="},_) $ x $ y) => (x,y)
12.30 + _ $ (Const(@{const_name HOL.eq},_) $ x $ y) => (x,y)
12.31 | _ => raise ERR "mk_COMB" "Second theorem not an equality"
12.32 val fty = type_of f
12.33 val (fd,fr) = dom_rng fty
12.34 @@ -1788,7 +1788,7 @@
12.35 val cv = cterm_of thy v
12.36 val th1 = implies_elim_all (beta_eta_thm th)
12.37 val (f,g) = case concl_of th1 of
12.38 - _ $ (Const(@{const_name "op ="},_) $ f $ g) => (Term.lambda v f,Term.lambda v g)
12.39 + _ $ (Const(@{const_name HOL.eq},_) $ f $ g) => (Term.lambda v f,Term.lambda v g)
12.40 | _ => raise ERR "mk_ABS" "Bad conclusion"
12.41 val (fd,fr) = dom_rng (type_of f)
12.42 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
13.1 --- a/src/HOL/Import/shuffler.ML Sat Aug 28 20:24:40 2010 +0800
13.2 +++ b/src/HOL/Import/shuffler.ML Sat Aug 28 16:14:32 2010 +0200
13.3 @@ -60,14 +60,14 @@
13.4
13.5 fun mk_meta_eq th =
13.6 (case concl_of th of
13.7 - Const(@{const_name Trueprop},_) $ (Const(@{const_name "op ="},_) $ _ $ _) => th RS eq_reflection
13.8 + Const(@{const_name Trueprop},_) $ (Const(@{const_name HOL.eq},_) $ _ $ _) => th RS eq_reflection
13.9 | Const("==",_) $ _ $ _ => th
13.10 | _ => raise THM("Not an equality",0,[th]))
13.11 handle _ => raise THM("Couldn't make meta equality",0,[th]) (* FIXME avoid handle _ *)
13.12
13.13 fun mk_obj_eq th =
13.14 (case concl_of th of
13.15 - Const(@{const_name Trueprop},_) $ (Const(@{const_name "op ="},_) $ _ $ _) => th
13.16 + Const(@{const_name Trueprop},_) $ (Const(@{const_name HOL.eq},_) $ _ $ _) => th
13.17 | Const("==",_) $ _ $ _ => th RS meta_eq_to_obj_eq
13.18 | _ => raise THM("Not an equality",0,[th]))
13.19 handle _ => raise THM("Couldn't make object equality",0,[th]) (* FIXME avoid handle _ *)
14.1 --- a/src/HOL/Library/OptionalSugar.thy Sat Aug 28 20:24:40 2010 +0800
14.2 +++ b/src/HOL/Library/OptionalSugar.thy Sat Aug 28 16:14:32 2010 +0200
14.3 @@ -32,7 +32,7 @@
14.4 (* deprecated, use thm with style instead, will be removed *)
14.5 (* aligning equations *)
14.6 notation (tab output)
14.7 - "op =" ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and
14.8 + "HOL.eq" ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and
14.9 "==" ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)")
14.10
14.11 (* Let *)
15.1 --- a/src/HOL/Library/reflection.ML Sat Aug 28 20:24:40 2010 +0800
15.2 +++ b/src/HOL/Library/reflection.ML Sat Aug 28 16:14:32 2010 +0200
15.3 @@ -82,7 +82,7 @@
15.4 fun rearrange congs =
15.5 let
15.6 fun P (_, th) =
15.7 - let val @{term "Trueprop"}$(Const (@{const_name "op ="},_) $l$_) = concl_of th
15.8 + let val @{term "Trueprop"}$(Const (@{const_name HOL.eq},_) $l$_) = concl_of th
15.9 in can dest_Var l end
15.10 val (yes,no) = List.partition P congs
15.11 in no @ yes end
16.1 --- a/src/HOL/Mutabelle/Mutabelle.thy Sat Aug 28 20:24:40 2010 +0800
16.2 +++ b/src/HOL/Mutabelle/Mutabelle.thy Sat Aug 28 16:14:32 2010 +0200
16.3 @@ -4,7 +4,7 @@
16.4 begin
16.5
16.6 ML {*
16.7 -val comms = [@{const_name "op ="}, @{const_name HOL.disj}, @{const_name HOL.conj}];
16.8 +val comms = [@{const_name HOL.eq}, @{const_name HOL.disj}, @{const_name HOL.conj}];
16.9
16.10 val forbidden =
16.11 [(@{const_name Power.power}, "'a"),
17.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML Sat Aug 28 20:24:40 2010 +0800
17.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Sat Aug 28 16:14:32 2010 +0200
17.3 @@ -187,7 +187,7 @@
17.4 val nitpick_mtd = ("nitpick", invoke_nitpick)
17.5 *)
17.6
17.7 -val comms = [@{const_name "op ="}, @{const_name HOL.disj}, @{const_name HOL.conj}]
17.8 +val comms = [@{const_name HOL.eq}, @{const_name HOL.disj}, @{const_name HOL.conj}]
17.9
17.10 val forbidden =
17.11 [(* (@{const_name "power"}, "'a"), *)
18.1 --- a/src/HOL/Nominal/nominal_datatype.ML Sat Aug 28 20:24:40 2010 +0800
18.2 +++ b/src/HOL/Nominal/nominal_datatype.ML Sat Aug 28 16:14:32 2010 +0200
18.3 @@ -183,7 +183,7 @@
18.4 end;
18.5
18.6 fun mk_not_sym ths = maps (fn th => case prop_of th of
18.7 - _ $ (Const (@{const_name Not}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _)) => [th, th RS not_sym]
18.8 + _ $ (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _)) => [th, th RS not_sym]
18.9 | _ => [th]) ths;
18.10
18.11 fun fresh_const T U = Const ("Nominal.fresh", T --> U --> HOLogic.boolT);
19.1 --- a/src/HOL/Nominal/nominal_thmdecls.ML Sat Aug 28 20:24:40 2010 +0800
19.2 +++ b/src/HOL/Nominal/nominal_thmdecls.ML Sat Aug 28 16:14:32 2010 +0200
19.3 @@ -147,7 +147,7 @@
19.4 else raise EQVT_FORM "Type Implication"
19.5 end
19.6 (* case: eqvt-lemma is of the equational form *)
19.7 - | (Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, _) $
19.8 + | (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $
19.9 (Const (@{const_name "perm"},typrm) $ Var (pi,typi) $ lhs) $ rhs)) =>
19.10 (if (apply_pi lhs (pi,typi)) = rhs
19.11 then [orig_thm]
20.1 --- a/src/HOL/Set.thy Sat Aug 28 20:24:40 2010 +0800
20.2 +++ b/src/HOL/Set.thy Sat Aug 28 16:14:32 2010 +0200
20.3 @@ -268,7 +268,7 @@
20.4
20.5 fun setcompr_tr [e, idts, b] =
20.6 let
20.7 - val eq = Syntax.const @{const_syntax "op ="} $ Bound (nvars idts) $ e;
20.8 + val eq = Syntax.const @{const_syntax HOL.eq} $ Bound (nvars idts) $ e;
20.9 val P = Syntax.const @{const_syntax HOL.conj} $ eq $ b;
20.10 val exP = ex_tr [idts, P];
20.11 in Syntax.const @{const_syntax Collect} $ Term.absdummy (dummyT, exP) end;
20.12 @@ -289,7 +289,7 @@
20.13 let
20.14 fun check (Const (@{const_syntax Ex}, _) $ Abs (_, _, P), n) = check (P, n + 1)
20.15 | check (Const (@{const_syntax HOL.conj}, _) $
20.16 - (Const (@{const_syntax "op ="}, _) $ Bound m $ e) $ P, n) =
20.17 + (Const (@{const_syntax HOL.eq}, _) $ Bound m $ e) $ P, n) =
20.18 n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso
20.19 subset (op =) (0 upto (n - 1), add_loose_bnos (e, 0, []))
20.20 | check _ = false;
21.1 --- a/src/HOL/Statespace/distinct_tree_prover.ML Sat Aug 28 20:24:40 2010 +0800
21.2 +++ b/src/HOL/Statespace/distinct_tree_prover.ML Sat Aug 28 16:14:32 2010 +0200
21.3 @@ -343,7 +343,7 @@
21.4 end handle Option => NONE)
21.5
21.6 fun distinctTree_tac names ctxt
21.7 - (Const (@{const_name Trueprop},_) $ (Const (@{const_name Not}, _) $ (Const (@{const_name "op ="}, _) $ x $ y)), i) =
21.8 + (Const (@{const_name Trueprop},_) $ (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, _) $ x $ y)), i) =
21.9 (case get_fst_success (neq_x_y ctxt x y) names of
21.10 SOME neq => rtac neq i
21.11 | NONE => no_tac)
21.12 @@ -356,7 +356,7 @@
21.13
21.14 fun distinct_simproc names =
21.15 Simplifier.simproc_global @{theory HOL} "DistinctTreeProver.distinct_simproc" ["x = y"]
21.16 - (fn thy => fn ss => fn (Const (@{const_name "op ="},_)$x$y) =>
21.17 + (fn thy => fn ss => fn (Const (@{const_name HOL.eq},_)$x$y) =>
21.18 case try Simplifier.the_context ss of
21.19 SOME ctxt => Option.map (fn neq => neq_to_eq_False OF [neq])
21.20 (get_fst_success (neq_x_y ctxt x y) names)
22.1 --- a/src/HOL/Statespace/state_fun.ML Sat Aug 28 20:24:40 2010 +0800
22.2 +++ b/src/HOL/Statespace/state_fun.ML Sat Aug 28 16:14:32 2010 +0200
22.3 @@ -285,7 +285,7 @@
22.4 then Bound 2
22.5 else raise TERM ("",[n]);
22.6 val sel' = lo $ d $ n' $ s;
22.7 - in (Const (@{const_name "op ="},Teq)$sel'$x',hd (binder_types Teq),nT,swap) end;
22.8 + in (Const (@{const_name HOL.eq},Teq)$sel'$x',hd (binder_types Teq),nT,swap) end;
22.9
22.10 fun dest_state (s as Bound 0) = s
22.11 | dest_state (s as (Const (sel,sT)$Bound 0)) =
22.12 @@ -295,10 +295,10 @@
22.13 | dest_state s =
22.14 raise TERM ("StateFun.ex_lookup_eq_simproc: not a record slector",[s]);
22.15
22.16 - fun dest_sel_eq (Const (@{const_name "op ="},Teq)$
22.17 + fun dest_sel_eq (Const (@{const_name HOL.eq},Teq)$
22.18 ((lo as (Const ("StateFun.lookup",lT)))$d$n$s)$X) =
22.19 (false,Teq,lT,lo,d,n,X,dest_state s)
22.20 - | dest_sel_eq (Const (@{const_name "op ="},Teq)$X$
22.21 + | dest_sel_eq (Const (@{const_name HOL.eq},Teq)$X$
22.22 ((lo as (Const ("StateFun.lookup",lT)))$d$n$s)) =
22.23 (true,Teq,lT,lo,d,n,X,dest_state s)
22.24 | dest_sel_eq _ = raise TERM ("",[]);
23.1 --- a/src/HOL/Statespace/state_space.ML Sat Aug 28 20:24:40 2010 +0800
23.2 +++ b/src/HOL/Statespace/state_space.ML Sat Aug 28 16:14:32 2010 +0200
23.3 @@ -223,7 +223,7 @@
23.4
23.5 fun distinctTree_tac ctxt
23.6 (Const (@{const_name Trueprop},_) $
23.7 - (Const (@{const_name Not}, _) $ (Const (@{const_name "op ="}, _) $ (x as Free _)$ (y as Free _))), i) =
23.8 + (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, _) $ (x as Free _)$ (y as Free _))), i) =
23.9 (case (neq_x_y ctxt x y) of
23.10 SOME neq => rtac neq i
23.11 | NONE => no_tac)
23.12 @@ -236,7 +236,7 @@
23.13
23.14 val distinct_simproc =
23.15 Simplifier.simproc_global @{theory HOL} "StateSpace.distinct_simproc" ["x = y"]
23.16 - (fn thy => fn ss => (fn (Const (@{const_name "op ="},_)$(x as Free _)$(y as Free _)) =>
23.17 + (fn thy => fn ss => (fn (Const (@{const_name HOL.eq},_)$(x as Free _)$(y as Free _)) =>
23.18 (case try Simplifier.the_context ss of
23.19 SOME ctxt => Option.map (fn neq => DistinctTreeProver.neq_to_eq_False OF [neq])
23.20 (neq_x_y ctxt x y)
24.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Sat Aug 28 20:24:40 2010 +0800
24.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Sat Aug 28 16:14:32 2010 +0200
24.3 @@ -416,7 +416,7 @@
24.4 fun prove_case_cong ((t, nchotomy), case_rewrites) =
24.5 let
24.6 val (Const ("==>", _) $ tm $ _) = t;
24.7 - val (Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, _) $ _ $ Ma)) = tm;
24.8 + val (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ Ma)) = tm;
24.9 val cert = cterm_of thy;
24.10 val nchotomy' = nchotomy RS spec;
24.11 val [v] = Term.add_vars (concl_of nchotomy') [];
25.1 --- a/src/HOL/Tools/Datatype/datatype_codegen.ML Sat Aug 28 20:24:40 2010 +0800
25.2 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Sat Aug 28 16:14:32 2010 +0200
25.3 @@ -96,7 +96,7 @@
25.4 fun mk_side const_name = Const (const_name, ty --> ty --> HOLogic.boolT)
25.5 $ Free ("x", ty) $ Free ("y", ty);
25.6 val def = HOLogic.mk_Trueprop (HOLogic.mk_eq
25.7 - (mk_side @{const_name HOL.equal}, mk_side @{const_name "op ="}));
25.8 + (mk_side @{const_name HOL.equal}, mk_side @{const_name HOL.eq}));
25.9 val def' = Syntax.check_term lthy def;
25.10 val ((_, (_, thm)), lthy') = Specification.definition
25.11 (NONE, (Attrib.empty_binding, def')) lthy;
26.1 --- a/src/HOL/Tools/Function/termination.ML Sat Aug 28 20:24:40 2010 +0800
26.2 +++ b/src/HOL/Tools/Function/termination.ML Sat Aug 28 16:14:32 2010 +0200
26.3 @@ -148,7 +148,7 @@
26.4 val cs = Function_Lib.dest_binop_list @{const_name Lattices.sup} rel
26.5 fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
26.6 let
26.7 - val (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ _)
26.8 + val (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ _)
26.9 = Term.strip_qnt_body @{const_name Ex} c
26.10 in cons r o cons l end
26.11 in
26.12 @@ -185,7 +185,7 @@
26.13 val vs = Term.strip_qnt_vars @{const_name Ex} c
26.14
26.15 (* FIXME: throw error "dest_call" for malformed terms *)
26.16 - val (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ Gam)
26.17 + val (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ Gam)
26.18 = Term.strip_qnt_body @{const_name Ex} c
26.19 val (p, l') = dest_inj sk l
26.20 val (q, r') = dest_inj sk r
27.1 --- a/src/HOL/Tools/Nitpick/minipick.ML Sat Aug 28 20:24:40 2010 +0800
27.2 +++ b/src/HOL/Tools/Nitpick/minipick.ML Sat Aug 28 16:14:32 2010 +0200
27.3 @@ -123,7 +123,7 @@
27.4 Exist (decls_for SRep card Ts T, to_F (T :: Ts) t')
27.5 | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
27.6 to_F Ts (t0 $ eta_expand Ts t1 1)
27.7 - | Const (@{const_name "op ="}, _) $ t1 $ t2 =>
27.8 + | Const (@{const_name HOL.eq}, _) $ t1 $ t2 =>
27.9 RelEq (to_R_rep Ts t1, to_R_rep Ts t2)
27.10 | Const (@{const_name ord_class.less_eq},
27.11 Type (@{type_name fun},
27.12 @@ -165,8 +165,8 @@
27.13 @{const Not} => to_R_rep Ts (eta_expand Ts t 1)
27.14 | Const (@{const_name All}, _) => to_R_rep Ts (eta_expand Ts t 1)
27.15 | Const (@{const_name Ex}, _) => to_R_rep Ts (eta_expand Ts t 1)
27.16 - | Const (@{const_name "op ="}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
27.17 - | Const (@{const_name "op ="}, _) => to_R_rep Ts (eta_expand Ts t 2)
27.18 + | Const (@{const_name HOL.eq}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
27.19 + | Const (@{const_name HOL.eq}, _) => to_R_rep Ts (eta_expand Ts t 2)
27.20 | Const (@{const_name ord_class.less_eq},
27.21 Type (@{type_name fun},
27.22 [Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ =>
28.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Aug 28 20:24:40 2010 +0800
28.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Aug 28 16:14:32 2010 +0200
28.3 @@ -408,7 +408,7 @@
28.4 (@{const_name True}, 0),
28.5 (@{const_name All}, 1),
28.6 (@{const_name Ex}, 1),
28.7 - (@{const_name "op ="}, 1),
28.8 + (@{const_name HOL.eq}, 1),
28.9 (@{const_name HOL.conj}, 2),
28.10 (@{const_name HOL.disj}, 2),
28.11 (@{const_name HOL.implies}, 2),
28.12 @@ -1275,7 +1275,7 @@
28.13 forall is_Var args andalso not (has_duplicates (op =) args)
28.14 | _ => false
28.15 fun do_eq (Const (@{const_name "=="}, _) $ t1 $ _) = do_lhs t1
28.16 - | do_eq (@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)) =
28.17 + | do_eq (@{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t1 $ _)) =
28.18 do_lhs t1
28.19 | do_eq _ = false
28.20 in do_eq end
28.21 @@ -1347,7 +1347,7 @@
28.22 @{const "==>"} $ _ $ t2 => term_under_def t2
28.23 | Const (@{const_name "=="}, _) $ t1 $ _ => term_under_def t1
28.24 | @{const Trueprop} $ t1 => term_under_def t1
28.25 - | Const (@{const_name "op ="}, _) $ t1 $ _ => term_under_def t1
28.26 + | Const (@{const_name HOL.eq}, _) $ t1 $ _ => term_under_def t1
28.27 | Abs (_, _, t') => term_under_def t'
28.28 | t1 $ _ => term_under_def t1
28.29 | _ => t
28.30 @@ -1371,7 +1371,7 @@
28.31 val (lhs, rhs) =
28.32 case t of
28.33 Const (@{const_name "=="}, _) $ t1 $ t2 => (t1, t2)
28.34 - | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ t2) =>
28.35 + | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t1 $ t2) =>
28.36 (t1, t2)
28.37 | _ => raise TERM ("Nitpick_HOL.normalized_rhs_of", [t])
28.38 val args = strip_comb lhs |> snd
28.39 @@ -1453,7 +1453,7 @@
28.40 | @{const "==>"} $ _ $ t2 => lhs_of_equation t2
28.41 | @{const Trueprop} $ t1 => lhs_of_equation t1
28.42 | Const (@{const_name All}, _) $ Abs (_, _, t1) => lhs_of_equation t1
28.43 - | Const (@{const_name "op ="}, _) $ t1 $ _ => SOME t1
28.44 + | Const (@{const_name HOL.eq}, _) $ t1 $ _ => SOME t1
28.45 | @{const HOL.implies} $ _ $ t2 => lhs_of_equation t2
28.46 | _ => NONE
28.47 fun is_constr_pattern _ (Bound _) = true
28.48 @@ -1807,7 +1807,7 @@
28.49 (betapply (t2, var_t))
28.50 end
28.51 | extensional_equal _ T t1 t2 =
28.52 - Const (@{const_name "op ="}, T --> T --> bool_T) $ t1 $ t2
28.53 + Const (@{const_name HOL.eq}, T --> T --> bool_T) $ t1 $ t2
28.54
28.55 fun equationalize_term ctxt tag t =
28.56 let
28.57 @@ -1816,7 +1816,7 @@
28.58 in
28.59 Logic.list_implies (prems,
28.60 case concl of
28.61 - @{const Trueprop} $ (Const (@{const_name "op ="}, Type (_, [T, _]))
28.62 + @{const Trueprop} $ (Const (@{const_name HOL.eq}, Type (_, [T, _]))
28.63 $ t1 $ t2) =>
28.64 @{const Trueprop} $ extensional_equal j T t1 t2
28.65 | @{const Trueprop} $ t' =>
28.66 @@ -2290,7 +2290,7 @@
28.67 | simps => simps
28.68 fun is_equational_fun_surely_complete hol_ctxt x =
28.69 case equational_fun_axioms hol_ctxt x of
28.70 - [@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)] =>
28.71 + [@{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t1 $ _)] =>
28.72 strip_comb t1 |> snd |> forall is_Var
28.73 | _ => false
28.74
29.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Sat Aug 28 20:24:40 2010 +0800
29.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Sat Aug 28 16:14:32 2010 +0200
29.3 @@ -590,7 +590,7 @@
29.4 if co then
29.5 Const (@{const_name The}, (T --> bool_T) --> T)
29.6 $ Abs (cyclic_co_val_name (), T,
29.7 - Const (@{const_name "op ="}, T --> T --> bool_T)
29.8 + Const (@{const_name HOL.eq}, T --> T --> bool_T)
29.9 $ Bound 0 $ abstract_over (var, t))
29.10 else
29.11 cyclic_atom ()
29.12 @@ -849,7 +849,7 @@
29.13 (** Model reconstruction **)
29.14
29.15 fun unfold_outer_the_binders (t as Const (@{const_name The}, _)
29.16 - $ Abs (s, T, Const (@{const_name "op ="}, _)
29.17 + $ Abs (s, T, Const (@{const_name HOL.eq}, _)
29.18 $ Bound 0 $ t')) =
29.19 betapply (Abs (s, T, t'), t) |> unfold_outer_the_binders
29.20 | unfold_outer_the_binders t = t
30.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Sat Aug 28 20:24:40 2010 +0800
30.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Sat Aug 28 16:14:32 2010 +0200
30.3 @@ -222,7 +222,7 @@
30.4 | fin_fun_body _ _ (t as Const (@{const_name None}, _)) = SOME t
30.5 | fin_fun_body dom_T ran_T
30.6 ((t0 as Const (@{const_name If}, _))
30.7 - $ (t1 as Const (@{const_name "op ="}, _) $ Bound 0 $ t1')
30.8 + $ (t1 as Const (@{const_name HOL.eq}, _) $ Bound 0 $ t1')
30.9 $ t2 $ t3) =
30.10 (if loose_bvar1 (t1', 0) then
30.11 NONE
30.12 @@ -650,7 +650,7 @@
30.13 Bound 0)))) accum
30.14 |>> mtype_of_mterm
30.15 end
30.16 - | @{const_name "op ="} => do_equals T accum
30.17 + | @{const_name HOL.eq} => do_equals T accum
30.18 | @{const_name The} =>
30.19 (trace_msg (K "*** The"); raise UNSOLVABLE ())
30.20 | @{const_name Eps} =>
30.21 @@ -760,7 +760,7 @@
30.22 do_term (incr_boundvars ~1 t1') accum
30.23 else
30.24 raise SAME ()
30.25 - | (t11 as Const (@{const_name "op ="}, _)) $ Bound 0 $ t13 =>
30.26 + | (t11 as Const (@{const_name HOL.eq}, _)) $ Bound 0 $ t13 =>
30.27 if not (loose_bvar1 (t13, 0)) then
30.28 do_term (incr_boundvars ~1 (t11 $ t13)) accum
30.29 else
30.30 @@ -876,7 +876,7 @@
30.31 do_term (@{const Not}
30.32 $ (HOLogic.eq_const (domain_type T0) $ t1
30.33 $ Abs (Name.uu, T1, @{const False}))) accum)
30.34 - | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
30.35 + | Const (x as (@{const_name HOL.eq}, _)) $ t1 $ t2 =>
30.36 do_equals x t1 t2
30.37 | Const (@{const_name Let}, _) $ t1 $ t2 =>
30.38 do_formula sn (betapply (t2, t1)) accum
30.39 @@ -973,7 +973,7 @@
30.40 do_conjunction t0 t1 t2 accum
30.41 | (t0 as Const (@{const_name All}, _)) $ Abs (s0, T1, t1) =>
30.42 do_all t0 s0 T1 t1 accum
30.43 - | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
30.44 + | Const (x as (@{const_name HOL.eq}, _)) $ t1 $ t2 =>
30.45 consider_general_equals mdata true x t1 t2 accum
30.46 | (t0 as @{const HOL.conj}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum
30.47 | (t0 as @{const HOL.implies}) $ t1 $ t2 => do_implies t0 t1 t2 accum
30.48 @@ -1069,7 +1069,7 @@
30.49 Abs (Name.uu, set_T', @{const True})
30.50 | _ => Const (s, T')
30.51 else if s = @{const_name "=="} orelse
30.52 - s = @{const_name "op ="} then
30.53 + s = @{const_name HOL.eq} then
30.54 let
30.55 val T =
30.56 case T' of
31.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Sat Aug 28 20:24:40 2010 +0800
31.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Sat Aug 28 16:14:32 2010 +0200
31.3 @@ -447,7 +447,7 @@
31.4 val t1 = incr_boundvars n t1
31.5 val t2 = incr_boundvars n t2
31.6 val xs = map Bound (n - 1 downto 0)
31.7 - val equation = Const (@{const_name "op ="},
31.8 + val equation = Const (@{const_name HOL.eq},
31.9 body_T --> body_T --> bool_T)
31.10 $ betapplys (t1, xs) $ betapplys (t2, xs)
31.11 val t =
31.12 @@ -515,9 +515,9 @@
31.13 do_description_operator The @{const_name undefined_fast_The} x t1
31.14 | (Const (x as (@{const_name Eps}, _)), [t1]) =>
31.15 do_description_operator Eps @{const_name undefined_fast_Eps} x t1
31.16 - | (Const (@{const_name "op ="}, T), [t1]) =>
31.17 + | (Const (@{const_name HOL.eq}, T), [t1]) =>
31.18 Op1 (SingletonSet, range_type T, Any, sub t1)
31.19 - | (Const (@{const_name "op ="}, T), [t1, t2]) => sub_equals T t1 t2
31.20 + | (Const (@{const_name HOL.eq}, T), [t1, t2]) => sub_equals T t1 t2
31.21 | (Const (@{const_name HOL.conj}, _), [t1, t2]) =>
31.22 Op2 (And, bool_T, Any, sub' t1, sub' t2)
31.23 | (Const (@{const_name HOL.disj}, _), [t1, t2]) =>
32.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Sat Aug 28 20:24:40 2010 +0800
32.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Sat Aug 28 16:14:32 2010 +0200
32.3 @@ -41,7 +41,7 @@
32.4 fun aux def (Const (@{const_name "=="}, _) $ t1 $ t2) =
32.5 aux def t1 andalso aux false t2
32.6 | aux def (@{const "==>"} $ t1 $ t2) = aux false t1 andalso aux def t2
32.7 - | aux def (Const (@{const_name "op ="}, _) $ t1 $ t2) =
32.8 + | aux def (Const (@{const_name HOL.eq}, _) $ t1 $ t2) =
32.9 aux def t1 andalso aux false t2
32.10 | aux def (@{const HOL.implies} $ t1 $ t2) = aux false t1 andalso aux def t2
32.11 | aux def (t1 $ t2) = aux def t1 andalso aux def t2
32.12 @@ -149,7 +149,7 @@
32.13 case t of
32.14 @{const Trueprop} $ t1 => box_var_in_def new_Ts old_Ts t1 z
32.15 | Const (s0, _) $ t1 $ _ =>
32.16 - if s0 = @{const_name "=="} orelse s0 = @{const_name "op ="} then
32.17 + if s0 = @{const_name "=="} orelse s0 = @{const_name HOL.eq} then
32.18 let
32.19 val (t', args) = strip_comb t1
32.20 val T' = fastype_of1 (new_Ts, do_term new_Ts old_Ts Neut t')
32.21 @@ -209,7 +209,7 @@
32.22 do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
32.23 | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
32.24 do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
32.25 - | Const (s0 as @{const_name "op ="}, T0) $ t1 $ t2 =>
32.26 + | Const (s0 as @{const_name HOL.eq}, T0) $ t1 $ t2 =>
32.27 do_equals new_Ts old_Ts s0 T0 t1 t2
32.28 | @{const HOL.conj} $ t1 $ t2 =>
32.29 @{const HOL.conj} $ do_term new_Ts old_Ts polar t1
32.30 @@ -332,7 +332,7 @@
32.31 do_eq_or_imp Ts true def t0 t1 t2 seen
32.32 | (t0 as @{const "==>"}) $ t1 $ t2 =>
32.33 if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen
32.34 - | (t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2 =>
32.35 + | (t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2 =>
32.36 do_eq_or_imp Ts true def t0 t1 t2 seen
32.37 | (t0 as @{const HOL.implies}) $ t1 $ t2 =>
32.38 do_eq_or_imp Ts false def t0 t1 t2 seen
32.39 @@ -399,7 +399,7 @@
32.40 aux_eq careful true t0 t1 t2
32.41 | aux careful ((t0 as @{const "==>"}) $ t1 $ t2) =
32.42 t0 $ aux false t1 $ aux careful t2
32.43 - | aux careful ((t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2) =
32.44 + | aux careful ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2) =
32.45 aux_eq careful true t0 t1 t2
32.46 | aux careful ((t0 as @{const HOL.implies}) $ t1 $ t2) =
32.47 t0 $ aux false t1 $ aux careful t2
32.48 @@ -464,9 +464,9 @@
32.49 and aux_implies prems zs t1 t2 =
32.50 case t1 of
32.51 Const (@{const_name "=="}, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2
32.52 - | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ Var z $ t') =>
32.53 + | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ Var z $ t') =>
32.54 aux_eq prems zs z t' t1 t2
32.55 - | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t' $ Var z) =>
32.56 + | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t' $ Var z) =>
32.57 aux_eq prems zs z t' t1 t2
32.58 | _ => aux (t1 :: prems) (Term.add_vars t1 zs) t2
32.59 and aux_eq prems zs z t' t1 t2 =
32.60 @@ -499,7 +499,7 @@
32.61 handle SAME () => do_term (t :: seen) ts
32.62 in
32.63 case t of
32.64 - Const (@{const_name "op ="}, _) $ t1 $ t2 => do_eq true t1 t2
32.65 + Const (@{const_name HOL.eq}, _) $ t1 $ t2 => do_eq true t1 t2
32.66 | _ => do_term (t :: seen) ts
32.67 end
32.68 in do_term end
32.69 @@ -653,7 +653,7 @@
32.70
32.71 fun params_in_equation (@{const "==>"} $ _ $ t2) = params_in_equation t2
32.72 | params_in_equation (@{const Trueprop} $ t1) = params_in_equation t1
32.73 - | params_in_equation (Const (@{const_name "op ="}, _) $ t1 $ _) =
32.74 + | params_in_equation (Const (@{const_name HOL.eq}, _) $ t1 $ _) =
32.75 snd (strip_comb t1)
32.76 | params_in_equation _ = []
32.77
33.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Sat Aug 28 20:24:40 2010 +0800
33.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Sat Aug 28 16:14:32 2010 +0200
33.3 @@ -179,7 +179,7 @@
33.4
33.5 fun translate_literal ctxt constant_table t =
33.6 case strip_comb t of
33.7 - (Const (@{const_name "op ="}, _), [l, r]) =>
33.8 + (Const (@{const_name HOL.eq}, _), [l, r]) =>
33.9 let
33.10 val l' = translate_term ctxt constant_table l
33.11 val r' = translate_term ctxt constant_table r
34.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Sat Aug 28 20:24:40 2010 +0800
34.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Sat Aug 28 16:14:32 2010 +0200
34.3 @@ -411,7 +411,7 @@
34.4 fun conjuncts t = conjuncts_aux t [];
34.5
34.6 fun is_equationlike_term (Const ("==", _) $ _ $ _) = true
34.7 - | is_equationlike_term (Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _)) = true
34.8 + | is_equationlike_term (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _)) = true
34.9 | is_equationlike_term _ = false
34.10
34.11 val is_equationlike = is_equationlike_term o prop_of
35.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Aug 28 20:24:40 2010 +0800
35.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Aug 28 16:14:32 2010 +0200
35.3 @@ -587,7 +587,7 @@
35.4
35.5 fun preprocess_elim ctxt elimrule =
35.6 let
35.7 - fun replace_eqs (Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, T) $ lhs $ rhs)) =
35.8 + fun replace_eqs (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, T) $ lhs $ rhs)) =
35.9 HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs)
35.10 | replace_eqs t = t
35.11 val thy = ProofContext.theory_of ctxt
36.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Sat Aug 28 20:24:40 2010 +0800
36.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Sat Aug 28 16:14:32 2010 +0200
36.3 @@ -111,7 +111,7 @@
36.4
36.5 fun mk_meta_equation th =
36.6 case prop_of th of
36.7 - Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _) => th RS @{thm eq_reflection}
36.8 + Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => th RS @{thm eq_reflection}
36.9 | _ => th
36.10
36.11 val meta_fun_cong = @{lemma "f == g ==> f x == g x" by simp}
36.12 @@ -217,7 +217,7 @@
36.13 @{const_name "==>"},
36.14 @{const_name Trueprop},
36.15 @{const_name Not},
36.16 - @{const_name "op ="},
36.17 + @{const_name HOL.eq},
36.18 @{const_name HOL.implies},
36.19 @{const_name All},
36.20 @{const_name Ex},
37.1 --- a/src/HOL/Tools/Qelim/cooper.ML Sat Aug 28 20:24:40 2010 +0800
37.2 +++ b/src/HOL/Tools/Qelim/cooper.ML Sat Aug 28 16:14:32 2010 +0200
37.3 @@ -122,8 +122,8 @@
37.4 ( case (term_of ct) of
37.5 Const(@{const_name HOL.conj},_)$_$_ => And (Thm.dest_binop ct)
37.6 | Const (@{const_name HOL.disj},_)$_$_ => Or (Thm.dest_binop ct)
37.7 -| Const (@{const_name "op ="},_)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox
37.8 -| Const (@{const_name Not},_) $ (Const (@{const_name "op ="},_)$y$_) =>
37.9 +| Const (@{const_name HOL.eq},_)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox
37.10 +| Const (@{const_name Not},_) $ (Const (@{const_name HOL.eq},_)$y$_) =>
37.11 if term_of x aconv y then NEq (funpow 2 Thm.dest_arg ct) else Nox
37.12 | Const (@{const_name Orderings.less}, _) $ y$ z =>
37.13 if term_of x aconv y then Lt (Thm.dest_arg ct)
37.14 @@ -274,7 +274,7 @@
37.15 | lin vs (Const (@{const_name Not},T)$t) = Const (@{const_name Not},T)$ (lin vs t)
37.16 | lin (vs as x::_) (Const(@{const_name Rings.dvd},_)$d$t) =
37.17 HOLogic.mk_binrel @{const_name Rings.dvd} (numeral1 abs d, lint vs t)
37.18 - | lin (vs as x::_) ((b as Const(@{const_name "op ="},_))$s$t) =
37.19 + | lin (vs as x::_) ((b as Const(@{const_name HOL.eq},_))$s$t) =
37.20 (case lint vs (subC$t$s) of
37.21 (t as a$(m$c$y)$r) =>
37.22 if x <> y then b$zero$t
37.23 @@ -345,7 +345,7 @@
37.24 case (term_of t) of
37.25 Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ =>
37.26 if x aconv y andalso member (op =)
37.27 - ["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
37.28 + [@{const_name HOL.eq}, @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
37.29 then (ins (dest_number c) acc,dacc) else (acc,dacc)
37.30 | Const(s,_)$_$(Const(@{const_name Groups.times},_)$c$y) =>
37.31 if x aconv y andalso member (op =)
37.32 @@ -387,7 +387,7 @@
37.33 | Const (@{const_name Not},_)$_ => Conv.arg_conv unit_conv t
37.34 | Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ =>
37.35 if x=y andalso member (op =)
37.36 - ["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
37.37 + [@{const_name HOL.eq}, @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
37.38 then cv (l div dest_number c) t else Thm.reflexive t
37.39 | Const(s,_)$_$(Const(@{const_name Groups.times},_)$c$y) =>
37.40 if x=y andalso member (op =)
38.1 --- a/src/HOL/Tools/Qelim/qelim.ML Sat Aug 28 20:24:40 2010 +0800
38.2 +++ b/src/HOL/Tools/Qelim/qelim.ML Sat Aug 28 16:14:32 2010 +0200
38.3 @@ -26,7 +26,7 @@
38.4 Const(s,T)$_$_ =>
38.5 if domain_type T = HOLogic.boolT
38.6 andalso member (op =) [@{const_name HOL.conj}, @{const_name HOL.disj},
38.7 - @{const_name HOL.implies}, @{const_name "op ="}] s
38.8 + @{const_name HOL.implies}, @{const_name HOL.eq}] s
38.9 then binop_conv (conv env) p
38.10 else atcv env p
38.11 | Const(@{const_name Not},_)$_ => arg_conv (conv env) p
39.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML Sat Aug 28 20:24:40 2010 +0800
39.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Sat Aug 28 16:14:32 2010 +0200
39.3 @@ -338,7 +338,7 @@
39.4 => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
39.5
39.6 (* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *)
39.7 -| (Const (@{const_name "op ="},_) $
39.8 +| (Const (@{const_name HOL.eq},_) $
39.9 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
39.10 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
39.11 => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}
39.12 @@ -350,7 +350,7 @@
39.13 => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
39.14
39.15 (* (op =) (Bex...) (Bex...) ----> (op =) (...) (...) *)
39.16 -| Const (@{const_name "op ="},_) $
39.17 +| Const (@{const_name HOL.eq},_) $
39.18 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
39.19 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
39.20 => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}
39.21 @@ -370,13 +370,13 @@
39.22 (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
39.23 => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt]
39.24
39.25 -| Const (@{const_name "op ="},_) $ (R $ _ $ _) $ (_ $ _ $ _) =>
39.26 +| Const (@{const_name HOL.eq},_) $ (R $ _ $ _) $ (_ $ _ $ _) =>
39.27 (rtac @{thm refl} ORELSE'
39.28 (equals_rsp_tac R ctxt THEN' RANGE [
39.29 quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]))
39.30
39.31 (* reflexivity of operators arising from Cong_tac *)
39.32 -| Const (@{const_name "op ="},_) $ _ $ _ => rtac @{thm refl}
39.33 +| Const (@{const_name HOL.eq},_) $ _ $ _ => rtac @{thm refl}
39.34
39.35 (* respectfulness of constants; in particular of a simple relation *)
39.36 | _ $ (Const _) $ (Const _) (* fun_rel, list_rel, etc but not equality *)
40.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML Sat Aug 28 20:24:40 2010 +0800
40.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML Sat Aug 28 16:14:32 2010 +0200
40.3 @@ -267,7 +267,7 @@
40.4 map_types (Envir.subst_type ty_inst) trm
40.5 end
40.6
40.7 -fun is_eq (Const (@{const_name "op ="}, _)) = true
40.8 +fun is_eq (Const (@{const_name HOL.eq}, _)) = true
40.9 | is_eq _ = false
40.10
40.11 fun mk_rel_compose (trm1, trm2) =
40.12 @@ -539,12 +539,12 @@
40.13 end
40.14
40.15 | (* equalities need to be replaced by appropriate equivalence relations *)
40.16 - (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) =>
40.17 + (Const (@{const_name HOL.eq}, ty), Const (@{const_name HOL.eq}, ty')) =>
40.18 if ty = ty' then rtrm
40.19 else equiv_relation ctxt (domain_type ty, domain_type ty')
40.20
40.21 | (* in this case we just check whether the given equivalence relation is correct *)
40.22 - (rel, Const (@{const_name "op ="}, ty')) =>
40.23 + (rel, Const (@{const_name HOL.eq}, ty')) =>
40.24 let
40.25 val rel_ty = fastype_of rel
40.26 val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty')
40.27 @@ -680,7 +680,7 @@
40.28 if T = T' then rtrm
40.29 else mk_repabs ctxt (T, T') rtrm
40.30
40.31 - | (_, Const (@{const_name "op ="}, _)) => rtrm
40.32 + | (_, Const (@{const_name HOL.eq}, _)) => rtrm
40.33
40.34 | (_, Const (_, T')) =>
40.35 let
41.1 --- a/src/HOL/Tools/SMT/smt_monomorph.ML Sat Aug 28 20:24:40 2010 +0800
41.2 +++ b/src/HOL/Tools/SMT/smt_monomorph.ML Sat Aug 28 16:14:32 2010 +0200
41.3 @@ -16,7 +16,7 @@
41.4
41.5 val ignored = member (op =) [
41.6 @{const_name All}, @{const_name Ex}, @{const_name Let}, @{const_name If},
41.7 - @{const_name "op ="}, @{const_name zero_class.zero},
41.8 + @{const_name HOL.eq}, @{const_name zero_class.zero},
41.9 @{const_name one_class.one}, @{const_name number_of}]
41.10
41.11 fun is_const f (n, T) = not (ignored n) andalso f T
42.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML Sat Aug 28 20:24:40 2010 +0800
42.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML Sat Aug 28 16:14:32 2010 +0200
42.3 @@ -252,7 +252,7 @@
42.4
42.5 fun norm_def ctxt thm =
42.6 (case Thm.prop_of thm of
42.7 - @{term Trueprop} $ (Const (@{const_name "op ="}, _) $ _ $ Abs _) =>
42.8 + @{term Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Abs _) =>
42.9 norm_def ctxt (thm RS @{thm fun_cong})
42.10 | Const (@{const_name "=="}, _) $ _ $ Abs _ =>
42.11 norm_def ctxt (thm RS @{thm meta_eq_to_obj_eq})
43.1 --- a/src/HOL/Tools/SMT/smtlib_interface.ML Sat Aug 28 20:24:40 2010 +0800
43.2 +++ b/src/HOL/Tools/SMT/smtlib_interface.ML Sat Aug 28 16:14:32 2010 +0200
43.3 @@ -162,12 +162,12 @@
43.4 | conn @{const_name HOL.conj} = SOME "and"
43.5 | conn @{const_name HOL.disj} = SOME "or"
43.6 | conn @{const_name HOL.implies} = SOME "implies"
43.7 - | conn @{const_name "op ="} = SOME "iff"
43.8 + | conn @{const_name HOL.eq} = SOME "iff"
43.9 | conn @{const_name If} = SOME "if_then_else"
43.10 | conn _ = NONE
43.11
43.12 fun pred @{const_name distinct} _ = SOME "distinct"
43.13 - | pred @{const_name "op ="} _ = SOME "="
43.14 + | pred @{const_name HOL.eq} _ = SOME "="
43.15 | pred @{const_name term_eq} _ = SOME "="
43.16 | pred @{const_name less} T = if_int_type T "<"
43.17 | pred @{const_name less_eq} T = if_int_type T "<="
44.1 --- a/src/HOL/Tools/SMT/z3_interface.ML Sat Aug 28 20:24:40 2010 +0800
44.2 +++ b/src/HOL/Tools/SMT/z3_interface.ML Sat Aug 28 16:14:32 2010 +0200
44.3 @@ -176,7 +176,7 @@
44.4 fun mk_nary _ cu [] = cu
44.5 | mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts)
44.6
44.7 -val eq = mk_inst_pair destT1 @{cpat "op ="}
44.8 +val eq = mk_inst_pair destT1 @{cpat HOL.eq}
44.9 fun mk_eq ct cu = Thm.mk_binop (instT' ct eq) ct cu
44.10
44.11 val if_term = mk_inst_pair (destT1 o destT2) @{cpat If}
45.1 --- a/src/HOL/Tools/SMT/z3_proof_literals.ML Sat Aug 28 20:24:40 2010 +0800
45.2 +++ b/src/HOL/Tools/SMT/z3_proof_literals.ML Sat Aug 28 16:14:32 2010 +0200
45.3 @@ -234,7 +234,7 @@
45.4 @{term Not} $ (@{term Not} $ t) => (T.compose dnegI, lookup t)
45.5 | @{term Not} $ (@{term "op = :: bool => _"} $ t $ (@{term Not} $ u)) =>
45.6 (T.compose negIffI, lookup (iff_const $ u $ t))
45.7 - | @{term Not} $ ((eq as Const (@{const_name "op ="}, _)) $ t $ u) =>
45.8 + | @{term Not} $ ((eq as Const (@{const_name HOL.eq}, _)) $ t $ u) =>
45.9 let fun rewr lit = lit COMP @{thm not_sym}
45.10 in (rewr, lookup (@{term Not} $ (eq $ u $ t))) end
45.11 | _ =>
46.1 --- a/src/HOL/Tools/SMT/z3_proof_tools.ML Sat Aug 28 20:24:40 2010 +0800
46.2 +++ b/src/HOL/Tools/SMT/z3_proof_tools.ML Sat Aug 28 16:14:32 2010 +0200
46.3 @@ -199,7 +199,7 @@
46.4 | @{term HOL.conj} $ _ $ _ => abstr2 cvs ct
46.5 | @{term HOL.disj} $ _ $ _ => abstr2 cvs ct
46.6 | @{term HOL.implies} $ _ $ _ => abstr2 cvs ct
46.7 - | Const (@{const_name "op ="}, _) $ _ $ _ => abstr2 cvs ct
46.8 + | Const (@{const_name HOL.eq}, _) $ _ $ _ => abstr2 cvs ct
46.9 | Const (@{const_name distinct}, _) $ _ =>
46.10 if ext_logic then abs_arg (abs_list abstr fresh_abstraction) cvs ct
46.11 else fresh_abstraction cvs ct
47.1 --- a/src/HOL/Tools/Sledgehammer/clausifier.ML Sat Aug 28 20:24:40 2010 +0800
47.2 +++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Sat Aug 28 16:14:32 2010 +0200
47.3 @@ -83,7 +83,7 @@
47.4 (Cf. "extensionalize_term" in "Sledgehammer_Translate".) *)
47.5 fun extensionalize_theorem th =
47.6 case prop_of th of
47.7 - _ $ (Const (@{const_name "op ="}, Type (_, [Type (@{type_name fun}, _), _]))
47.8 + _ $ (Const (@{const_name HOL.eq}, Type (_, [Type (@{type_name fun}, _), _]))
47.9 $ _ $ Abs (s, _, _)) => extensionalize_theorem (th RS fun_cong_all)
47.10 | _ => th
47.11
48.1 --- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML Sat Aug 28 20:24:40 2010 +0800
48.2 +++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Sat Aug 28 16:14:32 2010 +0200
48.3 @@ -94,7 +94,7 @@
48.4 val const_trans_table =
48.5 Symtab.make [(@{type_name Product_Type.prod}, "prod"),
48.6 (@{type_name Sum_Type.sum}, "sum"),
48.7 - (@{const_name "op ="}, "equal"),
48.8 + (@{const_name HOL.eq}, "equal"),
48.9 (@{const_name HOL.conj}, "and"),
48.10 (@{const_name HOL.disj}, "or"),
48.11 (@{const_name HOL.implies}, "implies"),
48.12 @@ -111,7 +111,7 @@
48.13
48.14 (* Invert the table of translations between Isabelle and ATPs. *)
48.15 val const_trans_table_inv =
48.16 - Symtab.update ("fequal", @{const_name "op ="})
48.17 + Symtab.update ("fequal", @{const_name HOL.eq})
48.18 (Symtab.make (map swap (Symtab.dest const_trans_table)))
48.19
48.20 val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
48.21 @@ -185,8 +185,8 @@
48.22 SOME c' => c'
48.23 | NONE => ascii_of c
48.24
48.25 -(* "op =" MUST BE "equal" because it's built into ATPs. *)
48.26 -fun make_fixed_const @{const_name "op ="} = "equal"
48.27 +(* HOL.eq MUST BE "equal" because it's built into ATPs. *)
48.28 +fun make_fixed_const @{const_name HOL.eq} = "equal"
48.29 | make_fixed_const c = const_prefix ^ lookup_const c
48.30
48.31 fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
49.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Sat Aug 28 20:24:40 2010 +0800
49.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Sat Aug 28 16:14:32 2010 +0200
49.3 @@ -224,7 +224,7 @@
49.4
49.5 fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
49.6
49.7 -fun smart_invert_const "fequal" = @{const_name "op ="}
49.8 +fun smart_invert_const "fequal" = @{const_name HOL.eq}
49.9 | smart_invert_const s = invert_const s
49.10
49.11 fun hol_type_from_metis_term _ (Metis.Term.Var v) =
49.12 @@ -264,7 +264,7 @@
49.13 end
49.14 | tm_to_tt (Metis.Term.Fn (fname, args)) = applic_to_tt (fname,args)
49.15 and applic_to_tt ("=",ts) =
49.16 - Term (list_comb(Const (@{const_name "op ="}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
49.17 + Term (list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
49.18 | applic_to_tt (a,ts) =
49.19 case strip_prefix_and_unascii const_prefix a of
49.20 SOME b =>
49.21 @@ -311,7 +311,7 @@
49.22 SOME w => mk_var(w, dummyT)
49.23 | NONE => mk_var(v, dummyT))
49.24 | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) =
49.25 - Const (@{const_name "op ="}, HOLogic.typeT)
49.26 + Const (@{const_name HOL.eq}, HOLogic.typeT)
49.27 | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
49.28 (case strip_prefix_and_unascii const_prefix x of
49.29 SOME c => Const (smart_invert_const c, dummyT)
49.30 @@ -325,7 +325,7 @@
49.31 cvt tm1 $ cvt tm2
49.32 | cvt (Metis.Term.Fn ("{}", [arg])) = cvt arg (*hBOOL*)
49.33 | cvt (Metis.Term.Fn ("=", [tm1,tm2])) =
49.34 - list_comb(Const (@{const_name "op ="}, HOLogic.typeT), map cvt [tm1,tm2])
49.35 + list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), map cvt [tm1,tm2])
49.36 | cvt (t as Metis.Term.Fn (x, [])) =
49.37 (case strip_prefix_and_unascii const_prefix x of
49.38 SOME c => Const (smart_invert_const c, dummyT)
49.39 @@ -480,7 +480,7 @@
49.40 val c_t = cterm_incr_types thy refl_idx i_t
49.41 in cterm_instantiate [(refl_x, c_t)] REFL_THM end;
49.42
49.43 -fun get_ty_arg_size _ (Const (@{const_name "op ="}, _)) = 0 (*equality has no type arguments*)
49.44 +fun get_ty_arg_size _ (Const (@{const_name HOL.eq}, _)) = 0 (*equality has no type arguments*)
49.45 | get_ty_arg_size thy (Const (c, _)) = (num_type_args thy c handle TYPE _ => 0)
49.46 | get_ty_arg_size _ _ = 0;
49.47
49.48 @@ -529,13 +529,13 @@
49.49 " isa-term: " ^ Syntax.string_of_term ctxt tm ^
49.50 " fol-term: " ^ Metis.Term.toString t)
49.51 fun path_finder FO tm ps _ = path_finder_FO tm ps
49.52 - | path_finder HO (tm as Const(@{const_name "op ="},_) $ _ $ _) (p::ps) _ =
49.53 + | path_finder HO (tm as Const(@{const_name HOL.eq},_) $ _ $ _) (p::ps) _ =
49.54 (*equality: not curried, as other predicates are*)
49.55 if p=0 then path_finder_HO tm (0::1::ps) (*select first operand*)
49.56 else path_finder_HO tm (p::ps) (*1 selects second operand*)
49.57 | path_finder HO tm (_ :: ps) (Metis.Term.Fn ("{}", [_])) =
49.58 path_finder_HO tm ps (*if not equality, ignore head to skip hBOOL*)
49.59 - | path_finder FT (tm as Const(@{const_name "op ="}, _) $ _ $ _) (p::ps)
49.60 + | path_finder FT (tm as Const(@{const_name HOL.eq}, _) $ _ $ _) (p::ps)
49.61 (Metis.Term.Fn ("=", [t1,t2])) =
49.62 (*equality: not curried, as other predicates are*)
49.63 if p=0 then path_finder_FT tm (0::1::ps)
50.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Sat Aug 28 20:24:40 2010 +0800
50.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Sat Aug 28 16:14:32 2010 +0200
50.3 @@ -121,7 +121,7 @@
50.4 handled specially via "fequal". *)
50.5 val boring_consts =
50.6 [@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let},
50.7 - @{const_name "op ="}]
50.8 + @{const_name HOL.eq}]
50.9
50.10 (* Add a pconstant to the table, but a [] entry means a standard
50.11 connective, which we ignore.*)
50.12 @@ -177,7 +177,7 @@
50.13 | @{const HOL.disj} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
50.14 | @{const HOL.implies} $ t1 $ t2 =>
50.15 do_formula (flip pos) t1 #> do_formula pos t2
50.16 - | Const (@{const_name "op ="}, Type (_, [T, _])) $ t1 $ t2 =>
50.17 + | Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t1 $ t2 =>
50.18 fold (do_term_or_formula T) [t1, t2]
50.19 | Const (@{const_name If}, Type (_, [_, Type (_, [T, _])]))
50.20 $ t1 $ t2 $ t3 =>
50.21 @@ -557,7 +557,7 @@
50.22 | (_, @{const Not} $ t1) => do_formula (not pos) t1
50.23 | (true, @{const HOL.disj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
50.24 | (false, @{const HOL.conj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
50.25 - | (true, Const (@{const_name "op ="}, _) $ t1 $ t2) => do_equals t1 t2
50.26 + | (true, Const (@{const_name HOL.eq}, _) $ t1 $ t2) => do_equals t1 t2
50.27 | (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2
50.28 | _ => false
50.29 in do_formula true end
51.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Sat Aug 28 20:24:40 2010 +0800
51.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Sat Aug 28 16:14:32 2010 +0200
51.3 @@ -315,7 +315,7 @@
51.4 | _ => raise FO_TERM us
51.5 else case strip_prefix_and_unascii const_prefix a of
51.6 SOME "equal" =>
51.7 - list_comb (Const (@{const_name "op ="}, HOLogic.typeT),
51.8 + list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT),
51.9 map (aux NONE []) us)
51.10 | SOME b =>
51.11 let
51.12 @@ -527,7 +527,7 @@
51.13 | is_bad_free _ _ = false
51.14
51.15 (* Vampire is keen on producing these. *)
51.16 -fun is_trivial_formula (@{const Not} $ (Const (@{const_name "op ="}, _)
51.17 +fun is_trivial_formula (@{const Not} $ (Const (@{const_name HOL.eq}, _)
51.18 $ t1 $ t2)) = (t1 aconv t2)
51.19 | is_trivial_formula _ = false
51.20
52.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Sat Aug 28 20:24:40 2010 +0800
52.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Sat Aug 28 16:14:32 2010 +0200
52.3 @@ -73,7 +73,7 @@
52.4 | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2
52.5 | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2
52.6 | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2
52.7 - | Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
52.8 + | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
52.9 do_conn bs AIff t1 t2
52.10 | _ => (fn ts => do_term bs (Envir.eta_contract t)
52.11 |>> AAtom ||> union (op =) ts)
52.12 @@ -97,7 +97,7 @@
52.13 | aux j (t as Const (s, Type (_, [Type (_, [_, T']),
52.14 Type (_, [_, res_T])]))
52.15 $ t2 $ Abs (var_s, var_T, t')) =
52.16 - if s = @{const_name "op ="} orelse s = @{const_name "=="} then
52.17 + if s = @{const_name HOL.eq} orelse s = @{const_name "=="} then
52.18 let val var_t = Var ((var_s, j), var_T) in
52.19 Const (s, T' --> T' --> res_T)
52.20 $ betapply (t2, var_t) $ subst_bound (var_t, t')
52.21 @@ -128,7 +128,7 @@
52.22 | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
52.23 | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
52.24 | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
52.25 - | (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])))
52.26 + | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
52.27 $ t1 $ t2 =>
52.28 t0 $ aux Ts t1 $ aux Ts t2
52.29 | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
53.1 --- a/src/HOL/Tools/TFL/dcterm.ML Sat Aug 28 20:24:40 2010 +0800
53.2 +++ b/src/HOL/Tools/TFL/dcterm.ML Sat Aug 28 16:14:32 2010 +0200
53.3 @@ -127,7 +127,7 @@
53.4
53.5 val dest_neg = dest_monop @{const_name Not}
53.6 val dest_pair = dest_binop @{const_name Pair}
53.7 -val dest_eq = dest_binop @{const_name "op ="}
53.8 +val dest_eq = dest_binop @{const_name HOL.eq}
53.9 val dest_imp = dest_binop @{const_name HOL.implies}
53.10 val dest_conj = dest_binop @{const_name HOL.conj}
53.11 val dest_disj = dest_binop @{const_name HOL.disj}
54.1 --- a/src/HOL/Tools/TFL/post.ML Sat Aug 28 20:24:40 2010 +0800
54.2 +++ b/src/HOL/Tools/TFL/post.ML Sat Aug 28 16:14:32 2010 +0200
54.3 @@ -67,7 +67,7 @@
54.4 val P_imp_P_eq_True = @{thm eqTrueI} RS eq_reflection;
54.5 fun mk_meta_eq r = case concl_of r of
54.6 Const("==",_)$_$_ => r
54.7 - | _ $(Const(@{const_name "op ="},_)$_$_) => r RS eq_reflection
54.8 + | _ $(Const(@{const_name HOL.eq},_)$_$_) => r RS eq_reflection
54.9 | _ => r RS P_imp_P_eq_True
54.10
54.11 (*Is this the best way to invoke the simplifier??*)
55.1 --- a/src/HOL/Tools/TFL/usyntax.ML Sat Aug 28 20:24:40 2010 +0800
55.2 +++ b/src/HOL/Tools/TFL/usyntax.ML Sat Aug 28 16:14:32 2010 +0200
55.3 @@ -244,7 +244,7 @@
55.4 end
55.5 | dest_abs _ _ = raise USYN_ERR "dest_abs" "not an abstraction";
55.6
55.7 -fun dest_eq(Const(@{const_name "op ="},_) $ M $ N) = {lhs=M, rhs=N}
55.8 +fun dest_eq(Const(@{const_name HOL.eq},_) $ M $ N) = {lhs=M, rhs=N}
55.9 | dest_eq _ = raise USYN_ERR "dest_eq" "not an equality";
55.10
55.11 fun dest_imp(Const(@{const_name HOL.implies},_) $ M $ N) = {ant=M, conseq=N}
56.1 --- a/src/HOL/Tools/cnf_funcs.ML Sat Aug 28 20:24:40 2010 +0800
56.2 +++ b/src/HOL/Tools/cnf_funcs.ML Sat Aug 28 16:14:32 2010 +0200
56.3 @@ -98,7 +98,7 @@
56.4 | is_atom (Const (@{const_name HOL.conj}, _) $ _ $ _) = false
56.5 | is_atom (Const (@{const_name HOL.disj}, _) $ _ $ _) = false
56.6 | is_atom (Const (@{const_name HOL.implies}, _) $ _ $ _) = false
56.7 - | is_atom (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ _ $ _) = false
56.8 + | is_atom (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ _ $ _) = false
56.9 | is_atom (Const (@{const_name Not}, _) $ _) = false
56.10 | is_atom _ = true;
56.11
56.12 @@ -205,7 +205,7 @@
56.13 in
56.14 make_nnf_imp OF [thm1, thm2]
56.15 end
56.16 - | make_nnf_thm thy (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ x $ y) =
56.17 + | make_nnf_thm thy (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ x $ y) =
56.18 let
56.19 val thm1 = make_nnf_thm thy x
56.20 val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
56.21 @@ -239,7 +239,7 @@
56.22 in
56.23 make_nnf_not_imp OF [thm1, thm2]
56.24 end
56.25 - | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ x $ y)) =
56.26 + | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ x $ y)) =
56.27 let
56.28 val thm1 = make_nnf_thm thy x
56.29 val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
57.1 --- a/src/HOL/Tools/groebner.ML Sat Aug 28 20:24:40 2010 +0800
57.2 +++ b/src/HOL/Tools/groebner.ML Sat Aug 28 16:14:32 2010 +0200
57.3 @@ -409,7 +409,7 @@
57.4 | _ => false;
57.5 fun is_eq t =
57.6 case term_of t of
57.7 - (Const(@{const_name "op ="},_)$_$_) => true
57.8 + (Const(@{const_name HOL.eq},_)$_$_) => true
57.9 | _ => false;
57.10
57.11 fun end_itlist f l =
57.12 @@ -923,7 +923,7 @@
57.13
57.14 fun find_term bounds tm =
57.15 (case term_of tm of
57.16 - Const (@{const_name "op ="}, T) $ _ $ _ =>
57.17 + Const (@{const_name HOL.eq}, T) $ _ $ _ =>
57.18 if domain_type T = HOLogic.boolT then find_args bounds tm
57.19 else dest_arg tm
57.20 | Const (@{const_name Not}, _) $ _ => find_term bounds (dest_arg tm)
57.21 @@ -985,7 +985,7 @@
57.22
57.23 local
57.24 fun lhs t = case term_of t of
57.25 - Const(@{const_name "op ="},_)$_$_ => Thm.dest_arg1 t
57.26 + Const(@{const_name HOL.eq},_)$_$_ => Thm.dest_arg1 t
57.27 | _=> raise CTERM ("ideal_tac - lhs",[t])
57.28 fun exitac NONE = no_tac
57.29 | exitac (SOME y) = rtac (instantiate' [SOME (ctyp_of_term y)] [NONE,SOME y] exI) 1
58.1 --- a/src/HOL/Tools/hologic.ML Sat Aug 28 20:24:40 2010 +0800
58.2 +++ b/src/HOL/Tools/hologic.ML Sat Aug 28 16:14:32 2010 +0200
58.3 @@ -236,10 +236,10 @@
58.4 fun dest_not (Const ("HOL.Not", _) $ t) = t
58.5 | dest_not t = raise TERM ("dest_not", [t]);
58.6
58.7 -fun eq_const T = Const ("op =", T --> T --> boolT);
58.8 +fun eq_const T = Const ("HOL.eq", T --> T --> boolT);
58.9 fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
58.10
58.11 -fun dest_eq (Const ("op =", _) $ lhs $ rhs) = (lhs, rhs)
58.12 +fun dest_eq (Const ("HOL.eq", _) $ lhs $ rhs) = (lhs, rhs)
58.13 | dest_eq t = raise TERM ("dest_eq", [t])
58.14
58.15 fun all_const T = Const ("HOL.All", [T --> boolT] ---> boolT);
59.1 --- a/src/HOL/Tools/inductive.ML Sat Aug 28 20:24:40 2010 +0800
59.2 +++ b/src/HOL/Tools/inductive.ML Sat Aug 28 16:14:32 2010 +0200
59.3 @@ -182,7 +182,7 @@
59.4 in
59.5 case concl_of thm of
59.6 Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq)
59.7 - | _ $ (Const (@{const_name "op ="}, _) $ _ $ _) => eq2mono thm
59.8 + | _ $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => eq2mono thm
59.9 | _ $ (Const (@{const_name Orderings.less_eq}, _) $ _ $ _) =>
59.10 dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
59.11 (resolve_tac [@{thm le_funI}, @{thm le_boolI'}])) thm))
60.1 --- a/src/HOL/Tools/inductive_codegen.ML Sat Aug 28 20:24:40 2010 +0800
60.2 +++ b/src/HOL/Tools/inductive_codegen.ML Sat Aug 28 16:14:32 2010 +0200
60.3 @@ -52,7 +52,7 @@
60.4 fun thyname_of s = (case optmod of
60.5 NONE => Codegen.thyname_of_const thy s | SOME s => s);
60.6 in (case Option.map strip_comb (try HOLogic.dest_Trueprop (concl_of thm)) of
60.7 - SOME (Const (@{const_name "op ="}, _), [t, _]) =>
60.8 + SOME (Const (@{const_name HOL.eq}, _), [t, _]) =>
60.9 (case head_of t of
60.10 Const (s, _) =>
60.11 CodegenData.put {intros = intros, graph = graph,
60.12 @@ -188,7 +188,7 @@
60.13 end)) (AList.lookup op = modes name)
60.14
60.15 in (case strip_comb t of
60.16 - (Const (@{const_name "op ="}, Type (_, [T, _])), _) =>
60.17 + (Const (@{const_name HOL.eq}, Type (_, [T, _])), _) =>
60.18 [Mode ((([], [1]), false), [1], []), Mode ((([], [2]), false), [2], [])] @
60.19 (if is_eqT T then [Mode ((([], [1, 2]), false), [1, 2], [])] else [])
60.20 | (Const (name, _), args) => the_default default (mk_modes name args)
60.21 @@ -344,7 +344,7 @@
60.22 end;
60.23
60.24 fun modename module s (iss, is) gr =
60.25 - let val (id, gr') = if s = @{const_name "op ="} then (("", "equal"), gr)
60.26 + let val (id, gr') = if s = @{const_name HOL.eq} then (("", "equal"), gr)
60.27 else mk_const_id module s gr
60.28 in (space_implode "__"
60.29 (mk_qual_id module id ::
60.30 @@ -363,7 +363,7 @@
60.31 | compile_expr thy defs dep module brack modes (SOME (Mode ((mode, _), _, ms)), t) gr =
60.32 (case strip_comb t of
60.33 (Const (name, _), args) =>
60.34 - if name = @{const_name "op ="} orelse AList.defined op = modes name then
60.35 + if name = @{const_name HOL.eq} orelse AList.defined op = modes name then
60.36 let
60.37 val (args1, args2) = chop (length ms) args;
60.38 val ((ps, mode_id), gr') = gr |> fold_map
60.39 @@ -581,7 +581,7 @@
60.40
60.41 fun dest_prem (_ $ (Const (@{const_name Set.member}, _) $ t $ u)) =
60.42 Prem ([t], Envir.beta_eta_contract u, true)
60.43 - | dest_prem (_ $ ((eq as Const (@{const_name "op ="}, _)) $ t $ u)) =
60.44 + | dest_prem (_ $ ((eq as Const (@{const_name HOL.eq}, _)) $ t $ u)) =
60.45 Prem ([t, u], eq, false)
60.46 | dest_prem (_ $ t) =
60.47 (case strip_comb t of
61.1 --- a/src/HOL/Tools/inductive_set.ML Sat Aug 28 20:24:40 2010 +0800
61.2 +++ b/src/HOL/Tools/inductive_set.ML Sat Aug 28 16:14:32 2010 +0200
61.3 @@ -265,7 +265,7 @@
61.4
61.5 fun add ctxt thm (tab as {to_set_simps, to_pred_simps, set_arities, pred_arities}) =
61.6 case prop_of thm of
61.7 - Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, Type (_, [T, _])) $ lhs $ rhs) =>
61.8 + Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, Type (_, [T, _])) $ lhs $ rhs) =>
61.9 (case body_type T of
61.10 @{typ bool} =>
61.11 let
62.1 --- a/src/HOL/Tools/int_arith.ML Sat Aug 28 20:24:40 2010 +0800
62.2 +++ b/src/HOL/Tools/int_arith.ML Sat Aug 28 16:14:32 2010 +0200
62.3 @@ -51,7 +51,7 @@
62.4
62.5 fun check (Const (@{const_name Groups.one}, @{typ int})) = false
62.6 | check (Const (@{const_name Groups.one}, _)) = true
62.7 - | check (Const (s, _)) = member (op =) [@{const_name "op ="},
62.8 + | check (Const (s, _)) = member (op =) [@{const_name HOL.eq},
62.9 @{const_name Groups.times}, @{const_name Groups.uminus},
62.10 @{const_name Groups.minus}, @{const_name Groups.plus},
62.11 @{const_name Groups.zero},
63.1 --- a/src/HOL/Tools/lin_arith.ML Sat Aug 28 20:24:40 2010 +0800
63.2 +++ b/src/HOL/Tools/lin_arith.ML Sat Aug 28 16:14:32 2010 +0200
63.3 @@ -229,7 +229,7 @@
63.4 case rel of
63.5 @{const_name Orderings.less} => SOME (p, i, "<", q, j)
63.6 | @{const_name Orderings.less_eq} => SOME (p, i, "<=", q, j)
63.7 - | "op =" => SOME (p, i, "=", q, j)
63.8 + | @{const_name HOL.eq} => SOME (p, i, "=", q, j)
63.9 | _ => NONE
63.10 end handle Rat.DIVZERO => NONE;
63.11
63.12 @@ -427,7 +427,7 @@
63.13 val t2' = incr_boundvars 1 t2
63.14 val t1_lt_t2 = Const (@{const_name Orderings.less},
63.15 split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
63.16 - val t1_eq_t2_plus_d = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
63.17 + val t1_eq_t2_plus_d = Const (@{const_name HOL.eq}, split_type --> split_type --> HOLogic.boolT) $ t1' $
63.18 (Const (@{const_name Groups.plus},
63.19 split_type --> split_type --> split_type) $ t2' $ d)
63.20 val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
63.21 @@ -447,7 +447,7 @@
63.22 (map (incr_boundvars 1) rev_terms)
63.23 val terms2 = map (subst_term [(split_term, zero_nat)]) rev_terms
63.24 val t1' = incr_boundvars 1 t1
63.25 - val t1_eq_nat_n = Const (@{const_name "op ="}, HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $
63.26 + val t1_eq_nat_n = Const (@{const_name HOL.eq}, HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $
63.27 (Const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) $ n)
63.28 val t1_lt_zero = Const (@{const_name Orderings.less},
63.29 HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int
63.30 @@ -471,13 +471,13 @@
63.31 (map (incr_boundvars 2) rev_terms)
63.32 val t1' = incr_boundvars 2 t1
63.33 val t2' = incr_boundvars 2 t2
63.34 - val t2_eq_zero = Const (@{const_name "op ="},
63.35 + val t2_eq_zero = Const (@{const_name HOL.eq},
63.36 split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
63.37 - val t2_neq_zero = HOLogic.mk_not (Const (@{const_name "op ="},
63.38 + val t2_neq_zero = HOLogic.mk_not (Const (@{const_name HOL.eq},
63.39 split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
63.40 val j_lt_t2 = Const (@{const_name Orderings.less},
63.41 split_type --> split_type--> HOLogic.boolT) $ j $ t2'
63.42 - val t1_eq_t2_times_i_plus_j = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
63.43 + val t1_eq_t2_times_i_plus_j = Const (@{const_name HOL.eq}, split_type --> split_type --> HOLogic.boolT) $ t1' $
63.44 (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
63.45 (Const (@{const_name Groups.times},
63.46 split_type --> split_type --> split_type) $ t2' $ i) $ j)
63.47 @@ -503,13 +503,13 @@
63.48 (map (incr_boundvars 2) rev_terms)
63.49 val t1' = incr_boundvars 2 t1
63.50 val t2' = incr_boundvars 2 t2
63.51 - val t2_eq_zero = Const (@{const_name "op ="},
63.52 + val t2_eq_zero = Const (@{const_name HOL.eq},
63.53 split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
63.54 - val t2_neq_zero = HOLogic.mk_not (Const (@{const_name "op ="},
63.55 + val t2_neq_zero = HOLogic.mk_not (Const (@{const_name HOL.eq},
63.56 split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
63.57 val j_lt_t2 = Const (@{const_name Orderings.less},
63.58 split_type --> split_type--> HOLogic.boolT) $ j $ t2'
63.59 - val t1_eq_t2_times_i_plus_j = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
63.60 + val t1_eq_t2_times_i_plus_j = Const (@{const_name HOL.eq}, split_type --> split_type --> HOLogic.boolT) $ t1' $
63.61 (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
63.62 (Const (@{const_name Groups.times},
63.63 split_type --> split_type --> split_type) $ t2' $ i) $ j)
63.64 @@ -541,7 +541,7 @@
63.65 (map (incr_boundvars 2) rev_terms)
63.66 val t1' = incr_boundvars 2 t1
63.67 val t2' = incr_boundvars 2 t2
63.68 - val t2_eq_zero = Const (@{const_name "op ="},
63.69 + val t2_eq_zero = Const (@{const_name HOL.eq},
63.70 split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
63.71 val zero_lt_t2 = Const (@{const_name Orderings.less},
63.72 split_type --> split_type --> HOLogic.boolT) $ zero $ t2'
63.73 @@ -555,7 +555,7 @@
63.74 split_type --> split_type--> HOLogic.boolT) $ j $ t2'
63.75 val t2_lt_j = Const (@{const_name Orderings.less},
63.76 split_type --> split_type--> HOLogic.boolT) $ t2' $ j
63.77 - val t1_eq_t2_times_i_plus_j = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
63.78 + val t1_eq_t2_times_i_plus_j = Const (@{const_name HOL.eq}, split_type --> split_type --> HOLogic.boolT) $ t1' $
63.79 (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
63.80 (Const (@{const_name Groups.times},
63.81 split_type --> split_type --> split_type) $ t2' $ i) $ j)
63.82 @@ -595,7 +595,7 @@
63.83 (map (incr_boundvars 2) rev_terms)
63.84 val t1' = incr_boundvars 2 t1
63.85 val t2' = incr_boundvars 2 t2
63.86 - val t2_eq_zero = Const (@{const_name "op ="},
63.87 + val t2_eq_zero = Const (@{const_name HOL.eq},
63.88 split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
63.89 val zero_lt_t2 = Const (@{const_name Orderings.less},
63.90 split_type --> split_type --> HOLogic.boolT) $ zero $ t2'
63.91 @@ -609,7 +609,7 @@
63.92 split_type --> split_type--> HOLogic.boolT) $ j $ t2'
63.93 val t2_lt_j = Const (@{const_name Orderings.less},
63.94 split_type --> split_type--> HOLogic.boolT) $ t2' $ j
63.95 - val t1_eq_t2_times_i_plus_j = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
63.96 + val t1_eq_t2_times_i_plus_j = Const (@{const_name HOL.eq}, split_type --> split_type --> HOLogic.boolT) $ t1' $
63.97 (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
63.98 (Const (@{const_name Groups.times},
63.99 split_type --> split_type --> split_type) $ t2' $ i) $ j)
64.1 --- a/src/HOL/Tools/meson.ML Sat Aug 28 20:24:40 2010 +0800
64.2 +++ b/src/HOL/Tools/meson.ML Sat Aug 28 16:14:32 2010 +0200
64.3 @@ -183,7 +183,7 @@
64.4 fun signed_lits th = signed_lits_aux (HOLogic.dest_Trueprop (concl_of th)) ([],[]);
64.5
64.6 (*Literals like X=X are tautologous*)
64.7 -fun taut_poslit (Const(@{const_name "op ="},_) $ t $ u) = t aconv u
64.8 +fun taut_poslit (Const(@{const_name HOL.eq},_) $ t $ u) = t aconv u
64.9 | taut_poslit (Const(@{const_name True},_)) = true
64.10 | taut_poslit _ = false;
64.11
64.12 @@ -213,7 +213,7 @@
64.13 case HOLogic.dest_Trueprop (concl_of th) of
64.14 (Const (@{const_name HOL.disj}, _) $ (Const (@{const_name HOL.disj}, _) $ _ $ _) $ _) =>
64.15 refl_clause_aux n (th RS disj_assoc) (*isolate an atom as first disjunct*)
64.16 - | (Const (@{const_name HOL.disj}, _) $ (Const(@{const_name Not},_) $ (Const(@{const_name "op ="},_) $ t $ u)) $ _) =>
64.17 + | (Const (@{const_name HOL.disj}, _) $ (Const(@{const_name Not},_) $ (Const(@{const_name HOL.eq},_) $ t $ u)) $ _) =>
64.18 if eliminable(t,u)
64.19 then refl_clause_aux (n-1) (th RS not_refl_disj_D) (*Var inequation: delete*)
64.20 else refl_clause_aux (n-1) (th RS disj_comm) (*not between Vars: ignore*)
64.21 @@ -222,7 +222,7 @@
64.22
64.23 fun notequal_lits_count (Const (@{const_name HOL.disj}, _) $ P $ Q) =
64.24 notequal_lits_count P + notequal_lits_count Q
64.25 - | notequal_lits_count (Const(@{const_name Not},_) $ (Const(@{const_name "op ="},_) $ _ $ _)) = 1
64.26 + | notequal_lits_count (Const(@{const_name Not},_) $ (Const(@{const_name HOL.eq},_) $ _ $ _)) = 1
64.27 | notequal_lits_count _ = 0;
64.28
64.29 (*Simplify a clause by applying reflexivity to its negated equality literals*)
64.30 @@ -280,7 +280,7 @@
64.31 | signed_nclauses b (Const(@{const_name HOL.implies},_) $ t $ u) =
64.32 if b then prod (signed_nclauses (not b) t) (signed_nclauses b u)
64.33 else sum (signed_nclauses (not b) t) (signed_nclauses b u)
64.34 - | signed_nclauses b (Const(@{const_name "op ="}, Type ("fun", [T, _])) $ t $ u) =
64.35 + | signed_nclauses b (Const(@{const_name HOL.eq}, Type ("fun", [T, _])) $ t $ u) =
64.36 if T = HOLogic.boolT then (*Boolean equality is if-and-only-if*)
64.37 if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u))
64.38 (prod (signed_nclauses (not b) u) (signed_nclauses b t))
65.1 --- a/src/HOL/Tools/nat_arith.ML Sat Aug 28 20:24:40 2010 +0800
65.2 +++ b/src/HOL/Tools/nat_arith.ML Sat Aug 28 16:14:32 2010 +0200
65.3 @@ -62,7 +62,7 @@
65.4 (struct
65.5 open CommonCancelSums;
65.6 val mk_bal = HOLogic.mk_eq;
65.7 - val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
65.8 + val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT;
65.9 val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel"};
65.10 end);
65.11
66.1 --- a/src/HOL/Tools/nat_numeral_simprocs.ML Sat Aug 28 20:24:40 2010 +0800
66.2 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML Sat Aug 28 16:14:32 2010 +0200
66.3 @@ -168,7 +168,7 @@
66.4 (open CancelNumeralsCommon
66.5 val prove_conv = Arith_Data.prove_conv
66.6 val mk_bal = HOLogic.mk_eq
66.7 - val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
66.8 + val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT
66.9 val bal_add1 = @{thm nat_eq_add_iff1} RS trans
66.10 val bal_add2 = @{thm nat_eq_add_iff2} RS trans
66.11 );
66.12 @@ -300,7 +300,7 @@
66.13 (open CancelNumeralFactorCommon
66.14 val prove_conv = Arith_Data.prove_conv
66.15 val mk_bal = HOLogic.mk_eq
66.16 - val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
66.17 + val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT
66.18 val cancel = @{thm nat_mult_eq_cancel1} RS trans
66.19 val neg_exchanges = false
66.20 )
66.21 @@ -380,7 +380,7 @@
66.22 (open CancelFactorCommon
66.23 val prove_conv = Arith_Data.prove_conv
66.24 val mk_bal = HOLogic.mk_eq
66.25 - val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
66.26 + val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT
66.27 fun simp_conv _ _ = SOME @{thm nat_mult_eq_cancel_disj}
66.28 );
66.29
67.1 --- a/src/HOL/Tools/numeral_simprocs.ML Sat Aug 28 20:24:40 2010 +0800
67.2 +++ b/src/HOL/Tools/numeral_simprocs.ML Sat Aug 28 16:14:32 2010 +0200
67.3 @@ -222,7 +222,7 @@
67.4 (open CancelNumeralsCommon
67.5 val prove_conv = Arith_Data.prove_conv
67.6 val mk_bal = HOLogic.mk_eq
67.7 - val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
67.8 + val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT
67.9 val bal_add1 = @{thm eq_add_iff1} RS trans
67.10 val bal_add2 = @{thm eq_add_iff2} RS trans
67.11 );
67.12 @@ -401,7 +401,7 @@
67.13 (open CancelNumeralFactorCommon
67.14 val prove_conv = Arith_Data.prove_conv
67.15 val mk_bal = HOLogic.mk_eq
67.16 - val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
67.17 + val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT
67.18 val cancel = @{thm mult_cancel_left} RS trans
67.19 val neg_exchanges = false
67.20 )
67.21 @@ -516,7 +516,7 @@
67.22 (open CancelFactorCommon
67.23 val prove_conv = Arith_Data.prove_conv
67.24 val mk_bal = HOLogic.mk_eq
67.25 - val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
67.26 + val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT
67.27 fun simp_conv _ _ = SOME @{thm mult_cancel_left}
67.28 );
67.29
67.30 @@ -606,7 +606,7 @@
67.31 local
67.32 val zr = @{cpat "0"}
67.33 val zT = ctyp_of_term zr
67.34 - val geq = @{cpat "op ="}
67.35 + val geq = @{cpat HOL.eq}
67.36 val eqT = Thm.dest_ctyp (ctyp_of_term geq) |> hd
67.37 val add_frac_eq = mk_meta_eq @{thm "add_frac_eq"}
67.38 val add_frac_num = mk_meta_eq @{thm "add_frac_num"}
67.39 @@ -676,7 +676,7 @@
67.40 val T = ctyp_of_term c
67.41 val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
67.42 in SOME (mk_meta_eq th) end
67.43 - | Const(@{const_name "op ="},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
67.44 + | Const(@{const_name HOL.eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
67.45 let
67.46 val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
67.47 val _ = map is_number [a,b,c]
67.48 @@ -697,7 +697,7 @@
67.49 val T = ctyp_of_term c
67.50 val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
67.51 in SOME (mk_meta_eq th) end
67.52 - | Const(@{const_name "op ="},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
67.53 + | Const(@{const_name HOL.eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
67.54 let
67.55 val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
67.56 val _ = map is_number [a,b,c]
68.1 --- a/src/HOL/Tools/recfun_codegen.ML Sat Aug 28 20:24:40 2010 +0800
68.2 +++ b/src/HOL/Tools/recfun_codegen.ML Sat Aug 28 16:14:32 2010 +0200
68.3 @@ -40,7 +40,7 @@
68.4 end
68.5 | avoid_value thy thms = thms;
68.6
68.7 -fun get_equations thy defs (raw_c, T) = if raw_c = @{const_name "op ="} then ([], "") else
68.8 +fun get_equations thy defs (raw_c, T) = if raw_c = @{const_name HOL.eq} then ([], "") else
68.9 let
68.10 val c = AxClass.unoverload_const thy (raw_c, T);
68.11 val raw_thms = Code.get_cert thy (Code_Preproc.preprocess_functrans thy) c
69.1 --- a/src/HOL/Tools/record.ML Sat Aug 28 20:24:40 2010 +0800
69.2 +++ b/src/HOL/Tools/record.ML Sat Aug 28 16:14:32 2010 +0200
69.3 @@ -1342,7 +1342,7 @@
69.4 val eq_simproc =
69.5 Simplifier.simproc_global @{theory HOL} "record_eq_simp" ["r = s"]
69.6 (fn thy => fn _ => fn t =>
69.7 - (case t of Const (@{const_name "op ="}, Type (_, [T, _])) $ _ $ _ =>
69.8 + (case t of Const (@{const_name HOL.eq}, Type (_, [T, _])) $ _ $ _ =>
69.9 (case rec_id ~1 T of
69.10 "" => NONE
69.11 | name =>
69.12 @@ -1405,12 +1405,12 @@
69.13 else raise TERM ("", [x]);
69.14 val sel' = Const (sel, Tsel) $ Bound 0;
69.15 val (l, r) = if lr then (sel', x') else (x', sel');
69.16 - in Const (@{const_name "op ="}, Teq) $ l $ r end
69.17 + in Const (@{const_name HOL.eq}, Teq) $ l $ r end
69.18 else raise TERM ("", [Const (sel, Tsel)]);
69.19
69.20 - fun dest_sel_eq (Const (@{const_name "op ="}, Teq) $ (Const (sel, Tsel) $ Bound 0) $ X) =
69.21 + fun dest_sel_eq (Const (@{const_name HOL.eq}, Teq) $ (Const (sel, Tsel) $ Bound 0) $ X) =
69.22 (true, Teq, (sel, Tsel), X)
69.23 - | dest_sel_eq (Const (@{const_name "op ="}, Teq) $ X $ (Const (sel, Tsel) $ Bound 0)) =
69.24 + | dest_sel_eq (Const (@{const_name HOL.eq}, Teq) $ X $ (Const (sel, Tsel) $ Bound 0)) =
69.25 (false, Teq, (sel, Tsel), X)
69.26 | dest_sel_eq _ = raise TERM ("", []);
69.27 in
69.28 @@ -1845,7 +1845,7 @@
69.29 val eq =
69.30 (HOLogic.mk_Trueprop o HOLogic.mk_eq)
69.31 (Const (@{const_name HOL.equal}, extT --> extT --> HOLogic.boolT),
69.32 - Const (@{const_name "op ="}, extT --> extT --> HOLogic.boolT));
69.33 + Const (@{const_name HOL.eq}, extT --> extT --> HOLogic.boolT));
69.34 fun tac eq_def =
69.35 Class.intro_classes_tac []
69.36 THEN (Simplifier.rewrite_goals_tac [Simpdata.mk_eq eq_def])
70.1 --- a/src/HOL/Tools/refute.ML Sat Aug 28 20:24:40 2010 +0800
70.2 +++ b/src/HOL/Tools/refute.ML Sat Aug 28 16:14:32 2010 +0200
70.3 @@ -647,7 +647,7 @@
70.4 | Const (@{const_name Hilbert_Choice.Eps}, _) => t
70.5 | Const (@{const_name All}, _) => t
70.6 | Const (@{const_name Ex}, _) => t
70.7 - | Const (@{const_name "op ="}, _) => t
70.8 + | Const (@{const_name HOL.eq}, _) => t
70.9 | Const (@{const_name HOL.conj}, _) => t
70.10 | Const (@{const_name HOL.disj}, _) => t
70.11 | Const (@{const_name HOL.implies}, _) => t
70.12 @@ -823,7 +823,7 @@
70.13 end
70.14 | Const (@{const_name All}, T) => collect_type_axioms T axs
70.15 | Const (@{const_name Ex}, T) => collect_type_axioms T axs
70.16 - | Const (@{const_name "op ="}, T) => collect_type_axioms T axs
70.17 + | Const (@{const_name HOL.eq}, T) => collect_type_axioms T axs
70.18 | Const (@{const_name HOL.conj}, _) => axs
70.19 | Const (@{const_name HOL.disj}, _) => axs
70.20 | Const (@{const_name HOL.implies}, _) => axs
70.21 @@ -1850,16 +1850,16 @@
70.22 end
70.23 | Const (@{const_name Ex}, _) =>
70.24 SOME (interpret thy model args (eta_expand t 1))
70.25 - | Const (@{const_name "op ="}, _) $ t1 $ t2 => (* similar to "==" (Pure) *)
70.26 + | Const (@{const_name HOL.eq}, _) $ t1 $ t2 => (* similar to "==" (Pure) *)
70.27 let
70.28 val (i1, m1, a1) = interpret thy model args t1
70.29 val (i2, m2, a2) = interpret thy m1 a1 t2
70.30 in
70.31 SOME (make_equality (i1, i2), m2, a2)
70.32 end
70.33 - | Const (@{const_name "op ="}, _) $ t1 =>
70.34 + | Const (@{const_name HOL.eq}, _) $ t1 =>
70.35 SOME (interpret thy model args (eta_expand t 1))
70.36 - | Const (@{const_name "op ="}, _) =>
70.37 + | Const (@{const_name HOL.eq}, _) =>
70.38 SOME (interpret thy model args (eta_expand t 2))
70.39 | Const (@{const_name HOL.conj}, _) $ t1 $ t2 =>
70.40 (* 3-valued logic *)
71.1 --- a/src/HOL/Tools/simpdata.ML Sat Aug 28 20:24:40 2010 +0800
71.2 +++ b/src/HOL/Tools/simpdata.ML Sat Aug 28 16:14:32 2010 +0200
71.3 @@ -10,7 +10,7 @@
71.4 structure Quantifier1 = Quantifier1Fun
71.5 (struct
71.6 (*abstract syntax*)
71.7 - fun dest_eq ((c as Const(@{const_name "op ="},_)) $ s $ t) = SOME (c, s, t)
71.8 + fun dest_eq ((c as Const(@{const_name HOL.eq},_)) $ s $ t) = SOME (c, s, t)
71.9 | dest_eq _ = NONE;
71.10 fun dest_conj ((c as Const(@{const_name HOL.conj},_)) $ s $ t) = SOME (c, s, t)
71.11 | dest_conj _ = NONE;
71.12 @@ -44,7 +44,7 @@
71.13 fun mk_eq th = case concl_of th
71.14 (*expects Trueprop if not == *)
71.15 of Const (@{const_name "=="},_) $ _ $ _ => th
71.16 - | _ $ (Const (@{const_name "op ="}, _) $ _ $ _) => mk_meta_eq th
71.17 + | _ $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => mk_meta_eq th
71.18 | _ $ (Const (@{const_name Not}, _) $ _) => th RS @{thm Eq_FalseI}
71.19 | _ => th RS @{thm Eq_TrueI}
71.20
72.1 --- a/src/HOL/ex/Meson_Test.thy Sat Aug 28 20:24:40 2010 +0800
72.2 +++ b/src/HOL/ex/Meson_Test.thy Sat Aug 28 16:14:32 2010 +0200
72.3 @@ -10,7 +10,7 @@
72.4 below and constants declared in HOL!
72.5 *}
72.6
72.7 -hide_const (open) implies union inter subset sum quotient
72.8 +hide_const (open) eq implies union inter subset sum quotient
72.9
72.10 text {*
72.11 Test data for the MESON proof procedure
73.1 --- a/src/HOL/ex/SVC_Oracle.thy Sat Aug 28 20:24:40 2010 +0800
73.2 +++ b/src/HOL/ex/SVC_Oracle.thy Sat Aug 28 16:14:32 2010 +0200
73.3 @@ -94,7 +94,7 @@
73.4 | fm ((c as Const(@{const_name Not}, _)) $ p) = c $ (fm p)
73.5 | fm ((c as Const(@{const_name True}, _))) = c
73.6 | fm ((c as Const(@{const_name False}, _))) = c
73.7 - | fm (t as Const(@{const_name "op ="}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
73.8 + | fm (t as Const(@{const_name HOL.eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
73.9 | fm (t as Const(@{const_name Orderings.less}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
73.10 | fm (t as Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
73.11 | fm t = replace t
74.1 --- a/src/HOL/ex/svc_funcs.ML Sat Aug 28 20:24:40 2010 +0800
74.2 +++ b/src/HOL/ex/svc_funcs.ML Sat Aug 28 16:14:32 2010 +0200
74.3 @@ -95,7 +95,7 @@
74.4 | Const(@{const_name Not}, _) => apply c (map tag ts)
74.5 | Const(@{const_name True}, _) => (c, false)
74.6 | Const(@{const_name False}, _) => (c, false)
74.7 - | Const(@{const_name "op ="}, Type ("fun", [T,_])) =>
74.8 + | Const(@{const_name HOL.eq}, Type ("fun", [T,_])) =>
74.9 if T = HOLogic.boolT then
74.10 (*biconditional: with int/nat comparisons below?*)
74.11 let val [t1,t2] = ts
74.12 @@ -200,7 +200,7 @@
74.13 Buildin("AND", (*unfolding uses both polarities*)
74.14 [Buildin("=>", [fm (not pos) p, fm pos q]),
74.15 Buildin("=>", [fm (not pos) q, fm pos p])])
74.16 - | fm pos (t as Const(@{const_name "op ="}, Type ("fun", [T,_])) $ x $ y) =
74.17 + | fm pos (t as Const(@{const_name HOL.eq}, Type ("fun", [T,_])) $ x $ y) =
74.18 let val tx = tm x and ty = tm y
74.19 in if pos orelse T = HOLogic.realT then
74.20 Buildin("=", [tx, ty])
75.1 --- a/src/HOLCF/Tools/Domain/domain_library.ML Sat Aug 28 20:24:40 2010 +0800
75.2 +++ b/src/HOLCF/Tools/Domain/domain_library.ML Sat Aug 28 16:14:32 2010 +0200
75.3 @@ -190,9 +190,9 @@
75.4
75.5 fun mk_All (x,P) = %%:"all" $ mk_lam(x,P); (* meta universal quantification *)
75.6
75.7 -infixr 0 ===>; fun S ===> T = %%:"==>" $ S $ T;
75.8 -infix 0 ==; fun S == T = %%:"==" $ S $ T;
75.9 -infix 1 ===; fun S === T = %%:"op =" $ S $ T;
75.10 +infixr 0 ===>; fun S ===> T = %%: "==>" $ S $ T;
75.11 +infix 0 ==; fun S == T = %%: "==" $ S $ T;
75.12 +infix 1 ===; fun S === T = %%: @{const_name HOL.eq} $ S $ T;
75.13 infix 1 ~=; fun S ~= T = HOLogic.mk_not (S === T);
75.14
75.15 infix 9 ` ; fun f ` x = %%: @{const_name Rep_CFun} $ f $ x;