changeset 19235 | 868129805da8 |
parent 19202 | 0b9eb4b0ad98 |
child 19237 | f51301fafdc2 |
--- a/src/HOL/ex/nbe.thy Fri Mar 10 16:05:34 2006 +0100 +++ b/src/HOL/ex/nbe.thy Fri Mar 10 16:21:49 2006 +0100 @@ -99,15 +99,15 @@ norm_by_eval "(%((x,y),(u,v)). add (add x y) (add u v)) ((Z,Z),(Z,Z))" norm_by_eval "last[a,b,c]" -text {* +( won't work since it relies on polymorphically used ad-hoc overloaded function: norm_by_eval "max 0 (0::nat)" -*} +*) -text {* +text (* Numerals still take their time\<dots> -*} +*) end