src/HOL/Sum_Type.thy
changeset 19008 14c1b2f5dda4
parent 17084 fb0a80aef0be
child 20380 14f9f2a1caa6
     1.1 --- a/src/HOL/Sum_Type.thy	Fri Feb 10 02:22:59 2006 +0100
     1.2 +++ b/src/HOL/Sum_Type.thy	Fri Feb 10 09:09:07 2006 +0100
     1.3 @@ -227,5 +227,11 @@
     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