--- a/src/HOL/NanoJava/Example.thy Wed Feb 10 23:53:46 2010 +0100
+++ b/src/HOL/NanoJava/Example.thy Thu Feb 11 00:45:02 2010 +0100
@@ -50,11 +50,14 @@
consts suc :: mname
add :: mname
consts any :: vname
-syntax dummy:: expr ("<>")
- one :: expr
-translations
- "<>" == "LAcc any"
- "one" == "{Nat}new Nat..suc(<>)"
+
+abbreviation
+ dummy :: expr ("<>")
+ where "<> == LAcc any"
+
+abbreviation
+ one :: expr
+ where "one == {Nat}new Nat..suc(<>)"
text {* The following properties could be derived from a more complete
program model, which we leave out for laziness. *}