author | webertj |
Fri, 10 Mar 2006 17:24:16 +0100 | |
changeset 19237 | f51301fafdc2 |
parent 19236 | 150e8b0fb991 |
child 19238 | a2a4e6838bfc |
--- a/src/HOL/ex/nbe.thy Fri Mar 10 16:31:50 2006 +0100 +++ b/src/HOL/ex/nbe.thy Fri Mar 10 17:24:16 2006 +0100 @@ -7,7 +7,7 @@ imports Main begin -ML"reset quick_and_dirty" +ML "reset quick_and_dirty" declare disj_assoc[code] @@ -99,7 +99,7 @@ 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]" -( +(* won't work since it relies on polymorphically used ad-hoc overloaded function: norm_by_eval "max 0 (0::nat)" @@ -110,5 +110,3 @@ *) end - -