src/HOL/Bali/Trans.thy
changeset 23747 b07cff284683
parent 21765 89275a3ed7be
child 28524 644b62cf678f
equal deleted inserted replaced
23746:a455e69c31cc 23747:b07cff284683
    66 
    66 
    67 translations
    67 translations
    68   "Ref a" == "Lit (Addr a)"
    68   "Ref a" == "Lit (Addr a)"
    69   "SKIP"  == "Lit Unit"
    69   "SKIP"  == "Lit Unit"
    70 
    70 
    71 inductive2
    71 inductive
    72   step :: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>1 _"[61,82,82] 81)
    72   step :: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>1 _"[61,82,82] 81)
    73   for G :: prog
    73   for G :: prog
    74 where
    74 where
    75 
    75 
    76 (* evaluation of expression *)
    76 (* evaluation of expression *)