src/HOL/Bali/Trans.thy
changeset 35067 af4c18c30593
parent 32960 69916a850301
child 35069 09154b995ed8
     1.1 --- a/src/HOL/Bali/Trans.thy	Tue Feb 09 16:07:09 2010 +0100
     1.2 +++ b/src/HOL/Bali/Trans.thy	Wed Feb 10 00:45:16 2010 +0100
     1.3 @@ -60,13 +60,13 @@
     1.4  by (simp)
     1.5  declare the_var_AVar_def [simp del]
     1.6  
     1.7 -syntax (xsymbols)
     1.8 -  Ref  :: "loc \<Rightarrow> expr"
     1.9 -  SKIP :: "expr"
    1.10 +abbreviation
    1.11 +  Ref :: "loc \<Rightarrow> expr"
    1.12 +  where "Ref a == Lit (Addr a)"
    1.13  
    1.14 -translations
    1.15 -  "Ref a" == "Lit (Addr a)"
    1.16 -  "SKIP"  == "Lit Unit"
    1.17 +abbreviation
    1.18 +  SKIP :: "expr"
    1.19 +  where "SKIP == Lit Unit"
    1.20  
    1.21  inductive
    1.22    step :: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>1 _"[61,82,82] 81)