removed some illegal characters: they were crashing SML/NJ
authorpaulson
Fri Mar 31 10:53:33 2006 +0200 (2006-03-31)
changeset 19336fb5e19d26d5e
parent 19335 9e82f341a71b
child 19337 146b25b893bb
removed some illegal characters: they were crashing SML/NJ
src/HOL/ex/SVC_Oracle.ML
src/HOL/ex/svc_funcs.ML
src/ZF/Resid/ROOT.ML
     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