1.1 --- a/src/HOL/ex/SVC_Oracle.ML Fri Mar 31 10:52:20 2006 +0200
1.2 +++ b/src/HOL/ex/SVC_Oracle.ML Fri Mar 31 10:53:33 2006 +0200
1.3 @@ -8,7 +8,7 @@
1.4 The following code merely CALLS the oracle;
1.5 the soundness-critical functions are at HOL/Tools/svc_funcs.ML
1.6
1.7 -Based upon the work of Søren T. Heilmann
1.8 +Based upon the work of Soren T. Heilmann
1.9 *)
1.10
1.11

2.1 --- a/src/HOL/ex/svc_funcs.ML Fri Mar 31 10:52:20 2006 +0200
2.2 +++ b/src/HOL/ex/svc_funcs.ML Fri Mar 31 10:53:33 2006 +0200
2.3 @@ -5,7 +5,7 @@
2.4
2.5 Translation functions for the interface to SVC
2.6
2.7 -Based upon the work of Søren T. Heilmann
2.8 +Based upon the work of Soren T. Heilmann
2.9
2.10 Integers and naturals are translated as follows:
2.11 In a positive context, replace x<y by x+1<=y

3.1 --- a/src/ZF/Resid/ROOT.ML Fri Mar 31 10:52:20 2006 +0200
3.2 +++ b/src/ZF/Resid/ROOT.ML Fri Mar 31 10:53:33 2006 +0200
3.3 @@ -8,7 +8,7 @@
3.4
3.5 By Ole Rasmussen, following the Coq proof given in
3.6
3.7 -Gérard Huet. Residual Theory in Lambda-Calculus: A Formal Development.
3.8 +Gerard Huet. Residual Theory in Lambda-Calculus: A Formal Development.
3.9 J. Functional Programming 4(3) 1994, 371-394.
3.10 *)
3.11