src/HOL/Bali/Trans.thy
changeset 23747 b07cff284683
parent 21765 89275a3ed7be
child 28524 644b62cf678f
     1.1 --- a/src/HOL/Bali/Trans.thy	Wed Jul 11 11:14:51 2007 +0200
     1.2 +++ b/src/HOL/Bali/Trans.thy	Wed Jul 11 11:16:34 2007 +0200
     1.3 @@ -68,7 +68,7 @@
     1.4    "Ref a" == "Lit (Addr a)"
     1.5    "SKIP"  == "Lit Unit"
     1.6  
     1.7 -inductive2
     1.8 +inductive
     1.9    step :: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>1 _"[61,82,82] 81)
    1.10    for G :: prog
    1.11  where