src/HOL/Sum_Type.thy
changeset 20380 14f9f2a1caa6
parent 19008 14c1b2f5dda4
child 20588 c847c56edf0c
     1.1 --- a/src/HOL/Sum_Type.thy	Mon Aug 14 13:46:05 2006 +0200
     1.2 +++ b/src/HOL/Sum_Type.thy	Mon Aug 14 13:46:06 2006 +0200
     1.3 @@ -227,11 +227,4 @@
     1.4  val basic_monos = thms "basic_monos";
     1.5  *}
     1.6  
     1.7 -subsection {* Codegenerator setup *}
     1.8 -
     1.9 -code_alias
    1.10 -  "+" "Sum_Type.sum"
    1.11 -  "Inr" "Sum_Type.Inr"
    1.12 -  "Inl" "Sum_Type.Inl"
    1.13 -
    1.14  end