# HG changeset patch
# User berghofe
# Date 980771490 -3600
# Node ID e7ffc23a05f6429200e74643fea0cf45ad63582a
# Parent  87f8a7644f9188c222cf9130845a6ae0f5249289
Completely split rule eval_evals_exec.induct before applying it.

diff -r 87f8a7644f91 -r e7ffc23a05f6 src/HOL/MicroJava/J/Eval.ML
--- a/src/HOL/MicroJava/J/Eval.ML	Mon Jan 29 13:28:15 2001 +0100
+++ b/src/HOL/MicroJava/J/Eval.ML	Mon Jan 29 13:31:30 2001 +0100
@@ -4,6 +4,8 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
+val eval_evals_exec_induct = complete_split_rule eval_evals_exec.induct;
+
 Goal "[|new_Addr (heap s) = (a,x); \
 \      s' = c_hupd (heap s(a\\<mapsto>(C,init_vars (fields (G,C))))) (x,s)|] ==> \
 \      G\\<turnstile>Norm s -NewC C\\<succ>Addr a-> s'";
@@ -16,7 +18,7 @@
 \             (G\\<turnstile>(x,s) -es[\\<succ>]vs-> (x',s') --> x'=None --> x=None) \\<and> \
 \             (G\\<turnstile>(x,s) -c       -> (x',s') --> x'=None --> x=None)";
 by(split_all_tac 1);
-by(rtac eval_evals_exec.induct 1);
+by(rtac eval_evals_exec_induct 1);
 by(rewtac c_hupd_def);
 by(ALLGOALS Asm_full_simp_tac);
 qed "eval_evals_exec_no_xcpt";
@@ -36,7 +38,7 @@
 \        (G\\<turnstile>(x,s) -es[\\<succ>]vs-> (x',s') --> x=Some xc --> x'=Some xc \\<and> s'=s) \\<and> \
 \        (G\\<turnstile>(x,s) -c       -> (x',s') --> x=Some xc --> x'=Some xc \\<and> s'=s)";
 by (split_all_tac 1);
-by (rtac eval_evals_exec.induct 1);
+by (rtac eval_evals_exec_induct 1);
 by (rewtac c_hupd_def);
 by (ALLGOALS Asm_full_simp_tac);
 qed "eval_evals_exec_xcpt";
diff -r 87f8a7644f91 -r e7ffc23a05f6 src/HOL/MicroJava/J/JTypeSafe.ML
--- a/src/HOL/MicroJava/J/JTypeSafe.ML	Mon Jan 29 13:28:15 2001 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.ML	Mon Jan 29 13:31:30 2001 +0100
@@ -173,7 +173,7 @@
 \ (G\\<turnstile>(x,(h,l)) -c       -> (x', (h',l')) --> \
 \     (\\<forall>lT.    (h ,l )::\\<preceq>(G,lT) -->       (G,lT)\\<turnstile>c  \\<surd> --> \
 \     h\\<le>|h' \\<and> (h',l')::\\<preceq>(G,lT)))";
-by( rtac eval_evals_exec.induct 1);
+by( rtac eval_evals_exec_induct 1);
 by( rewtac c_hupd_def);
 
 (* several simplifications, XcptE, XcptEs, XcptS, Skip, Nil?? *)