postprocessing of equality
authorhaftmann
Fri Apr 04 13:40:21 2008 +0200 (2008-04-04)
changeset 26555046e63c9165c
parent 26554 5ee45391576e
child 26556 90b02960c8ce
postprocessing of equality
src/HOL/HOL.thy
src/HOL/ex/NormalForm.thy
     1.1 --- a/src/HOL/HOL.thy	Thu Apr 03 23:55:11 2008 +0200
     1.2 +++ b/src/HOL/HOL.thy	Fri Apr 04 13:40:21 2008 +0200
     1.3 @@ -1673,10 +1673,13 @@
     1.4  lemma equals_eq [code inline, code func]: "op = \<equiv> eq"
     1.5    by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq)
     1.6  
     1.7 +declare equals_eq [symmetric, code post]
     1.8 +
     1.9  end
    1.10  
    1.11  setup {*
    1.12 -  CodeUnit.add_const_alias @{thm equals_eq}
    1.13 +  Sign.hide_names_i true ("const", ["HOL.eq"])
    1.14 +  #> CodeUnit.add_const_alias @{thm equals_eq}
    1.15  *}
    1.16  
    1.17  lemma [code func]:
     2.1 --- a/src/HOL/ex/NormalForm.thy	Thu Apr 03 23:55:11 2008 +0200
     2.2 +++ b/src/HOL/ex/NormalForm.thy	Fri Apr 04 13:40:21 2008 +0200
     2.3 @@ -8,8 +8,6 @@
     2.4  imports Main "~~/src/HOL/Real/Rational"
     2.5  begin
     2.6  
     2.7 -declare equals_eq [symmetric, code post]
     2.8 -
     2.9  lemma "True" by normalization
    2.10  lemma "p \<longrightarrow> True" by normalization
    2.11  declare disj_assoc [code func]