| changeset 28562 | 4e74209f113e |
| parent 28346 | b8390cd56b8f |
| child 29936 | d3dfb67f0f59 |
--- a/src/HOL/Library/Code_Integer.thy Fri Oct 10 06:45:50 2008 +0200 +++ b/src/HOL/Library/Code_Integer.thy Fri Oct 10 06:45:53 2008 +0200 @@ -92,7 +92,7 @@ text {* Evaluation *} -lemma [code func, code func del]: +lemma [code, code del]: "(Code_Eval.term_of \<Colon> int \<Rightarrow> term) = Code_Eval.term_of" .. code_const "Code_Eval.term_of \<Colon> int \<Rightarrow> term"