src/HOL/HOL.thy
changeset 38864 4abe644fcea5
parent 38857 97775f3e8722
child 38866 8ffb9f541285
     1.1 --- a/src/HOL/HOL.thy	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/HOL.thy	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -61,14 +61,8 @@
     1.4    disj          :: "[bool, bool] => bool"           (infixr "|" 30)
     1.5    implies       :: "[bool, bool] => bool"           (infixr "-->" 25)
     1.6  
     1.7 -setup Sign.root_path
     1.8 +  eq            :: "['a, 'a] => bool"               (infixl "=" 50)
     1.9  
    1.10 -consts
    1.11 -  "op ="        :: "['a, 'a] => bool"               (infixl "=" 50)
    1.12 -
    1.13 -setup Sign.local_path
    1.14 -
    1.15 -consts
    1.16    The           :: "('a => bool) => 'a"
    1.17    All           :: "('a => bool) => bool"           (binder "ALL " 10)
    1.18    Ex            :: "('a => bool) => bool"           (binder "EX " 10)
    1.19 @@ -78,7 +72,7 @@
    1.20  subsubsection {* Additional concrete syntax *}
    1.21  
    1.22  notation (output)
    1.23 -  "op ="  (infix "=" 50)
    1.24 +  eq  (infix "=" 50)
    1.25  
    1.26  abbreviation
    1.27    not_equal :: "['a, 'a] => bool"  (infixl "~=" 50) where
    1.28 @@ -89,15 +83,15 @@
    1.29  
    1.30  notation (xsymbols)
    1.31    Not  ("\<not> _" [40] 40) and
    1.32 -  HOL.conj  (infixr "\<and>" 35) and
    1.33 -  HOL.disj  (infixr "\<or>" 30) and
    1.34 -  HOL.implies  (infixr "\<longrightarrow>" 25) and
    1.35 +  conj  (infixr "\<and>" 35) and
    1.36 +  disj  (infixr "\<or>" 30) and
    1.37 +  implies  (infixr "\<longrightarrow>" 25) and
    1.38    not_equal  (infix "\<noteq>" 50)
    1.39  
    1.40  notation (HTML output)
    1.41    Not  ("\<not> _" [40] 40) and
    1.42 -  HOL.conj  (infixr "\<and>" 35) and
    1.43 -  HOL.disj  (infixr "\<or>" 30) and
    1.44 +  conj  (infixr "\<and>" 35) and
    1.45 +  disj  (infixr "\<or>" 30) and
    1.46    not_equal  (infix "\<noteq>" 50)
    1.47  
    1.48  abbreviation (iff)
    1.49 @@ -183,8 +177,8 @@
    1.50    True_or_False:  "(P=True) | (P=False)"
    1.51  
    1.52  finalconsts
    1.53 -  "op ="
    1.54 -  HOL.implies
    1.55 +  eq
    1.56 +  implies
    1.57    The
    1.58  
    1.59  definition If :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" ("(if (_)/ then (_)/ else (_))" [0, 0, 10] 10) where
    1.60 @@ -864,7 +858,7 @@
    1.61  
    1.62  setup {*
    1.63  let
    1.64 -  fun non_bool_eq (@{const_name "op ="}, Type (_, [T, _])) = T <> @{typ bool}
    1.65 +  fun non_bool_eq (@{const_name HOL.eq}, Type (_, [T, _])) = T <> @{typ bool}
    1.66      | non_bool_eq _ = false;
    1.67    val hyp_subst_tac' =
    1.68      SUBGOAL (fn (goal, i) =>
    1.69 @@ -930,7 +924,7 @@
    1.70  (
    1.71    val thy = @{theory}
    1.72    type claset = Classical.claset
    1.73 -  val equality_name = @{const_name "op ="}
    1.74 +  val equality_name = @{const_name HOL.eq}
    1.75    val not_name = @{const_name Not}
    1.76    val notE = @{thm notE}
    1.77    val ccontr = @{thm ccontr}
    1.78 @@ -1746,8 +1740,8 @@
    1.79  
    1.80  fun eq_codegen thy defs dep thyname b t gr =
    1.81      (case strip_comb t of
    1.82 -       (Const (@{const_name "op ="}, Type (_, [Type ("fun", _), _])), _) => NONE
    1.83 -     | (Const (@{const_name "op ="}, _), [t, u]) =>
    1.84 +       (Const (@{const_name HOL.eq}, Type (_, [Type ("fun", _), _])), _) => NONE
    1.85 +     | (Const (@{const_name HOL.eq}, _), [t, u]) =>
    1.86            let
    1.87              val (pt, gr') = Codegen.invoke_codegen thy defs dep thyname false t gr;
    1.88              val (pu, gr'') = Codegen.invoke_codegen thy defs dep thyname false u gr';
    1.89 @@ -1756,7 +1750,7 @@
    1.90              SOME (Codegen.parens
    1.91                (Pretty.block [pt, Codegen.str " =", Pretty.brk 1, pu]), gr''')
    1.92            end
    1.93 -     | (t as Const (@{const_name "op ="}, _), ts) => SOME (Codegen.invoke_codegen
    1.94 +     | (t as Const (@{const_name HOL.eq}, _), ts) => SOME (Codegen.invoke_codegen
    1.95           thy defs dep thyname b (Codegen.eta_expand t ts 2) gr)
    1.96       | _ => NONE);
    1.97  
    1.98 @@ -1796,7 +1790,7 @@
    1.99  
   1.100  setup {*
   1.101    Code_Preproc.map_pre (fn simpset =>
   1.102 -    simpset addsimprocs [Simplifier.simproc_global_i @{theory} "equal" [@{term "op ="}]
   1.103 +    simpset addsimprocs [Simplifier.simproc_global_i @{theory} "equal" [@{term HOL.eq}]
   1.104        (fn thy => fn _ => fn Const (_, T) => case strip_type T
   1.105          of (Type _ :: _, _) => SOME @{thm eq_equal}
   1.106           | _ => NONE)])
   1.107 @@ -1944,7 +1938,7 @@
   1.108  code_const "HOL.equal"
   1.109    (Haskell infixl 4 "==")
   1.110  
   1.111 -code_const "op ="
   1.112 +code_const HOL.eq
   1.113    (Haskell infixl 4 "==")
   1.114  
   1.115  text {* undefined *}