src/HOL/HOL.thy
changeset 26739 947b6013e863
parent 26732 6ea9de67e576
child 26747 f32fa5f5bdd1
     1.1 --- a/src/HOL/HOL.thy	Tue Apr 22 13:35:26 2008 +0200
     1.2 +++ b/src/HOL/HOL.thy	Tue Apr 22 22:00:25 2008 +0200
     1.3 @@ -1659,8 +1659,6 @@
     1.4  
     1.5  subsection {* Code generator basic setup -- see further @{text Code_Setup.thy} *}
     1.6  
     1.7 -setup "CodeName.setup #> CodeTarget.setup #> Nbe.setup"
     1.8 -
     1.9  code_datatype Trueprop "prop"
    1.10  
    1.11  code_datatype "TYPE('a\<Colon>{})"
    1.12 @@ -1699,6 +1697,9 @@
    1.13  
    1.14  setup {*
    1.15    CodeUnit.add_const_alias @{thm equals_eq}
    1.16 +  #> CodeName.setup
    1.17 +  #> CodeTarget.setup
    1.18 +  #> Nbe.setup @{sort eq} [(@{const_name eq_class.eq}, @{const_name "op ="})]
    1.19  *}
    1.20  
    1.21  lemma [code func]: