# HG changeset patch
# User webertj
# Date 1142007856 -3600
# Node ID f51301fafdc23720ec0c2fb9c48d4b87983862ed
# Parent  150e8b0fb9914fe27cb59d87e6bf2880b861b8db
comment delimiter fixed

diff -r 150e8b0fb991 -r f51301fafdc2 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
-
-