author | haftmann |
Fri, 10 Mar 2006 16:21:49 +0100 | |
changeset 19235 | 868129805da8 |
parent 19234 | 054332e39e0a |
child 19236 | 150e8b0fb991 |
--- 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