| changeset 20380 | 14f9f2a1caa6 |
| parent 19008 | 14c1b2f5dda4 |
| child 20588 | c847c56edf0c |
--- a/src/HOL/Sum_Type.thy Mon Aug 14 13:46:05 2006 +0200 +++ b/src/HOL/Sum_Type.thy Mon Aug 14 13:46:06 2006 +0200 @@ -227,11 +227,4 @@ val basic_monos = thms "basic_monos"; *} -subsection {* Codegenerator setup *} - -code_alias - "+" "Sum_Type.sum" - "Inr" "Sum_Type.Inr" - "Inl" "Sum_Type.Inl" - end