--- a/src/ZF/Coind/Static.thy Sat Dec 29 18:35:27 2001 +0100
+++ b/src/ZF/Coind/Static.thy Sat Dec 29 18:36:12 2001 +0100
@@ -54,11 +54,12 @@
type_intros te_appI Exp.intros Ty.intros
-inductive_cases elab_constE [elim!]: "<te,e_const(c),t> \<in> ElabRel"
-inductive_cases elab_varE [elim!]: "<te,e_var(x),t> \<in> ElabRel"
-inductive_cases elab_fnE [elim]: "<te,e_fn(x,e),t> \<in> ElabRel"
-inductive_cases elab_fixE [elim!]: "<te,e_fix(f,x,e),t> \<in> ElabRel"
-inductive_cases elab_appE [elim]: "<te,e_app(e1,e2),t> \<in> ElabRel"
+inductive_cases
+ elab_constE [elim!]: "<te,e_const(c),t> \<in> ElabRel"
+ and elab_varE [elim!]: "<te,e_var(x),t> \<in> ElabRel"
+ and elab_fnE [elim]: "<te,e_fn(x,e),t> \<in> ElabRel"
+ and elab_fixE [elim!]: "<te,e_fix(f,x,e),t> \<in> ElabRel"
+ and elab_appE [elim]: "<te,e_app(e1,e2),t> \<in> ElabRel"
declare ElabRel.dom_subset [THEN subsetD, dest]