# HG changeset patch
# User webertj
# Date 1142009633 -3600
# Node ID a2a4e6838bfcf543f16e475f401f3fd106bd6558
# Parent  f51301fafdc23720ec0c2fb9c48d4b87983862ed
text delimiter fixed

diff -r f51301fafdc2 -r a2a4e6838bfc src/HOL/ex/nbe.thy
--- a/src/HOL/ex/nbe.thy	Fri Mar 10 17:24:16 2006 +0100
+++ b/src/HOL/ex/nbe.thy	Fri Mar 10 17:53:53 2006 +0100
@@ -105,8 +105,8 @@
   norm_by_eval "max 0 (0::nat)"
 *)
 
-text (*
+text {*
   Numerals still take their time\<dots>
-*)
+*}
 
 end