Pure equality is a regular cpde operation
authorhaftmann
Mon Sep 20 18:43:18 2010 +0200 (2010-09-20)
changeset 3956687a5704673f0
parent 39565 f4f87c6e2fad
child 39567 5ee997fbe5cc
Pure equality is a regular cpde operation
src/HOL/HOL.thy
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/HOL/HOL.thy	Mon Sep 20 15:25:32 2010 +0200
     1.2 +++ b/src/HOL/HOL.thy	Mon Sep 20 18:43:18 2010 +0200
     1.3 @@ -742,7 +742,7 @@
     1.4    then show False by (rule notE)
     1.5  qed
     1.6  
     1.7 -lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)"
     1.8 +lemma atomize_eq [atomize, code]: "(x == y) == Trueprop (x = y)"
     1.9  proof
    1.10    assume "x == y"
    1.11    show "x = y" by (unfold `x == y`) (rule refl)
     2.1 --- a/src/Tools/Code/code_thingol.ML	Mon Sep 20 15:25:32 2010 +0200
     2.2 +++ b/src/Tools/Code/code_thingol.ML	Mon Sep 20 18:43:18 2010 +0200
     2.3 @@ -275,6 +275,7 @@
     2.4         of SOME (tyco, _) => Codegen.thyname_of_type thy tyco
     2.5          | NONE => Codegen.thyname_of_const thy c);
     2.6    fun purify_base "==>" = "follows"
     2.7 +    | purify_base "==" = "meta_eq"
     2.8      | purify_base s = Name.desymbolize false s;
     2.9    fun namify thy get_basename get_thyname name =
    2.10      let