src/HOL/Bali/Evaln.thy
changeset 23747 b07cff284683
parent 23350 50c5b0912a0c
child 24019 67bde7cfcf10
     1.1 --- a/src/HOL/Bali/Evaln.thy	Wed Jul 11 11:14:51 2007 +0200
     1.2 +++ b/src/HOL/Bali/Evaln.thy	Wed Jul 11 11:16:34 2007 +0200
     1.3 @@ -28,7 +28,7 @@
     1.4  for welltyped, and definitely assigned terms.
     1.5  *}
     1.6  
     1.7 -inductive2
     1.8 +inductive
     1.9    evaln	:: "[prog, state, term, nat, vals, state] \<Rightarrow> bool"
    1.10      ("_\<turnstile>_ \<midarrow>_\<succ>\<midarrow>_\<rightarrow> '(_, _')" [61,61,80,61,0,0] 60)
    1.11    and evarn :: "[prog, state, var, vvar, nat, state] \<Rightarrow> bool"
    1.12 @@ -201,9 +201,9 @@
    1.13  ML_setup {*
    1.14  change_simpset (fn ss => ss delloop "split_all_tac");
    1.15  *}
    1.16 -inductive_cases2 evaln_cases: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v, s')"
    1.17 +inductive_cases evaln_cases: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v, s')"
    1.18  
    1.19 -inductive_cases2 evaln_elim_cases:
    1.20 +inductive_cases evaln_elim_cases:
    1.21  	"G\<turnstile>(Some xc, s) \<midarrow>t                        \<succ>\<midarrow>n\<rightarrow> (v, s')"
    1.22  	"G\<turnstile>Norm s \<midarrow>In1r Skip                      \<succ>\<midarrow>n\<rightarrow> (x, s')"
    1.23          "G\<turnstile>Norm s \<midarrow>In1r (Jmp j)                   \<succ>\<midarrow>n\<rightarrow> (x, s')"