# HG changeset patch
# User paulson
# Date 1143795213 -7200
# Node ID fb5e19d26d5efe21249e7052248465c9ea3533b9
# Parent  9e82f341a71b797c633c7e9e821620aa603d089a
removed some illegal characters: they were crashing SML/NJ

diff -r 9e82f341a71b -r fb5e19d26d5e src/HOL/ex/SVC_Oracle.ML
--- a/src/HOL/ex/SVC_Oracle.ML	Fri Mar 31 10:52:20 2006 +0200
+++ b/src/HOL/ex/SVC_Oracle.ML	Fri Mar 31 10:53:33 2006 +0200
@@ -8,7 +8,7 @@
 The following code merely CALLS the oracle;
   the soundness-critical functions are at HOL/Tools/svc_funcs.ML
 
-Based upon the work of Søren T. Heilmann
+Based upon the work of Soren T. Heilmann
 *)
 
 
diff -r 9e82f341a71b -r fb5e19d26d5e src/HOL/ex/svc_funcs.ML
--- a/src/HOL/ex/svc_funcs.ML	Fri Mar 31 10:52:20 2006 +0200
+++ b/src/HOL/ex/svc_funcs.ML	Fri Mar 31 10:53:33 2006 +0200
@@ -5,7 +5,7 @@
 
 Translation functions for the interface to SVC
 
-Based upon the work of Søren T. Heilmann
+Based upon the work of Soren T. Heilmann
 
 Integers and naturals are translated as follows:
   In a positive context, replace x<y by x+1<=y
diff -r 9e82f341a71b -r fb5e19d26d5e src/ZF/Resid/ROOT.ML
--- a/src/ZF/Resid/ROOT.ML	Fri Mar 31 10:52:20 2006 +0200
+++ b/src/ZF/Resid/ROOT.ML	Fri Mar 31 10:53:33 2006 +0200
@@ -8,7 +8,7 @@
 
 By Ole Rasmussen, following the Coq proof given in
 
-Gérard Huet.  Residual Theory in Lambda-Calculus: A Formal Development.
+Gerard Huet.  Residual Theory in Lambda-Calculus: A Formal Development.
 J. Functional Programming 4(3) 1994, 371-394.
 *)