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