     1.1 --- a/src/HOL/ex/Predicate_Compile.thy	Mon May 11 09:18:42 2009 +0200
     1.2 +++ b/src/HOL/ex/Predicate_Compile.thy	Mon May 11 09:39:53 2009 +0200
     1.3 @@ -49,6 +49,7 @@
     1.4  code_pred append
     1.5    using assms by (rule append.cases)
     1.6  
     1.7 +thm append_codegen
     1.8  thm append_cases
     1.9  
    1.10
changeset 31107	657386d94f14
parent 31106	9a1178204dc0
child 31108	0ce5f53fc65d