--- a/src/HOL/Bali/DefiniteAssignment.thy Wed Jul 11 11:14:51 2007 +0200
+++ b/src/HOL/Bali/DefiniteAssignment.thy Wed Jul 11 11:16:34 2007 +0200
@@ -533,7 +533,7 @@
distinguish boolean and other expressions.
*}
-inductive2
+inductive
da :: "env \<Rightarrow> lname set \<Rightarrow> term \<Rightarrow> assigned \<Rightarrow> bool" ("_\<turnstile> _ \<guillemotright>_\<guillemotright> _" [65,65,65,65] 71)
where
Skip: "Env\<turnstile> B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>"
@@ -823,7 +823,7 @@
ML_setup {*
change_simpset (fn ss => ss delloop "split_all_tac");
*}
-inductive_cases2 da_elim_cases [cases set]:
+inductive_cases da_elim_cases [cases set]:
"Env\<turnstile> B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A"
"Env\<turnstile> B \<guillemotright>In1r Skip\<guillemotright> A"
"Env\<turnstile> B \<guillemotright>\<langle>Expr e\<rangle>\<guillemotright> A"