comment delimiter fixed
authorwebertj
Fri, 10 Mar 2006 17:24:16 +0100
changeset 19237 f51301fafdc2
parent 19236 150e8b0fb991
child 19238 a2a4e6838bfc
comment delimiter fixed
src/HOL/ex/nbe.thy
--- 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
-
-