# HG changeset patch
# User nipkow
# Date 929026019 -7200
# Node ID 4267539284be5891c05b275ae2f012383f32069c
# Parent  de4d358bf01e7b49d3f15833bfed2e526af69111
unclosed comment.

diff -r de4d358bf01e -r 4267539284be src/HOL/Hoare/Examples.ML
--- a/src/HOL/Hoare/Examples.ML	Thu Jun 10 12:36:19 1999 +0200
+++ b/src/HOL/Hoare/Examples.ML	Thu Jun 10 16:46:59 1999 +0200
@@ -75,7 +75,7 @@
 
 (** Square root **)
 
-(* the easy way: *
+(* the easy way: *)
 
 Goal "|- VARS x r. \
 \ {u = 1 & w = 1 & r = 0} \