--- a/src/HOL/Bali/Trans.thy Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Bali/Trans.thy Wed Feb 10 00:45:16 2010 +0100
@@ -60,13 +60,13 @@
by (simp)
declare the_var_AVar_def [simp del]
-syntax (xsymbols)
- Ref :: "loc \<Rightarrow> expr"
- SKIP :: "expr"
+abbreviation
+ Ref :: "loc \<Rightarrow> expr"
+ where "Ref a == Lit (Addr a)"
-translations
- "Ref a" == "Lit (Addr a)"
- "SKIP" == "Lit Unit"
+abbreviation
+ SKIP :: "expr"
+ where "SKIP == Lit Unit"
inductive
step :: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>1 _"[61,82,82] 81)