--- 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
*)
--- 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
--- 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.
*)