| changeset 19336 | fb5e19d26d5e |
| parent 19277 | f7602e74d948 |
| child 20853 | 3ff5a2e05810 |
--- 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