src/HOL/MicroJava/J/Eval.ML

--- a/src/HOL/MicroJava/J/Eval.ML	Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/Eval.ML	Thu Sep 21 10:42:49 2000 +0200
@@ -4,44 +4,44 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-Goal "\\<lbrakk>new_Addr (heap s) = (a,x); \
-\      s' = c_hupd (heap s(a\\<mapsto>(C,init_vars (fields (G,C))))) (x,s)\\<rbrakk> \\<Longrightarrow> \
-\      G\\<turnstile>Norm s -NewC C\\<succ>Addr a\\<rightarrow> s'";
+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'";
 by (hyp_subst_tac 1);
 br eval_evals_exec.NewC 1;
 by Auto_tac;
 qed "NewCI";
 
-Goal "\\<And>s s'. (G\\<turnstile>(x,s) -e \\<succ>  v \\<rightarrow> (x',s') \\<longrightarrow> x'=None \\<longrightarrow> x=None) \\<and> \
-\             (G\\<turnstile>(x,s) -es[\\<succ>]vs\\<rightarrow> (x',s') \\<longrightarrow> x'=None \\<longrightarrow> x=None) \\<and> \
-\             (G\\<turnstile>(x,s) -c       \\<rightarrow> (x',s') \\<longrightarrow> x'=None \\<longrightarrow> x=None)";
+Goal "!!s s'. (G\\<turnstile>(x,s) -e \\<succ>  v -> (x',s') --> x'=None --> x=None) \\<and> \
+\             (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(rewtac c_hupd_def);
 by(ALLGOALS Asm_full_simp_tac);
 qed "eval_evals_exec_no_xcpt";
 
-val eval_no_xcpt = prove_goal thy "\\<And>X. G\\<turnstile>(x,s) -e\\<succ>v\\<rightarrow> (None,s') \\<Longrightarrow> x=None" (K [
+val eval_no_xcpt = prove_goal thy "!!X. G\\<turnstile>(x,s) -e\\<succ>v-> (None,s') ==> x=None" (K [
 	dtac (eval_evals_exec_no_xcpt RS conjunct1 RS mp) 1,
 	Fast_tac 1]);
-val evals_no_xcpt = prove_goal thy "\\<And>X. G\\<turnstile>(x,s) -e[\\<succ>]v\\<rightarrow> (None,s') \\<Longrightarrow> x=None" (K [
+val evals_no_xcpt = prove_goal thy "!!X. G\\<turnstile>(x,s) -e[\\<succ>]v-> (None,s') ==> x=None" (K [
 	dtac (eval_evals_exec_no_xcpt RS conjunct2 RS conjunct1 RS mp) 1,
 	Fast_tac 1]);
 
 val eval_evals_exec_xcpt = prove_goal thy 
-"\\<And>s s'. (G\\<turnstile>(x,s) -e \\<succ>  v \\<rightarrow> (x',s') \\<longrightarrow> x=Some xc \\<longrightarrow> x'=Some xc \\<and> s'=s) \\<and> \
-\        (G\\<turnstile>(x,s) -es[\\<succ>]vs\\<rightarrow> (x',s') \\<longrightarrow> x=Some xc \\<longrightarrow> x'=Some xc \\<and> s'=s) \\<and> \
-\        (G\\<turnstile>(x,s) -c       \\<rightarrow> (x',s') \\<longrightarrow> x=Some xc \\<longrightarrow> x'=Some xc \\<and> s'=s)"
+"!!s s'. (G\\<turnstile>(x,s) -e \\<succ>  v -> (x',s') --> x=Some xc --> x'=Some xc \\<and> s'=s) \\<and> \
+\        (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)"
  (K [
 	split_all_tac 1,
 	rtac eval_evals_exec.induct 1,
 	rewtac c_hupd_def,
 	ALLGOALS Asm_full_simp_tac]);
 val eval_xcpt = prove_goal thy 
-"\\<And>X. G\\<turnstile>(Some xc,s) -e\\<succ>v\\<rightarrow> (x',s') \\<Longrightarrow> x'=Some xc \\<and>  s'=s" (K [
+"!!X. G\\<turnstile>(Some xc,s) -e\\<succ>v-> (x',s') ==> x'=Some xc \\<and>  s'=s" (K [
 	dtac (eval_evals_exec_xcpt RS conjunct1 RS mp) 1,
 	Fast_tac 1]);
 val exec_xcpt = prove_goal thy 
-"\\<And>X. G\\<turnstile>(Some xc,s) -s0\\<rightarrow> (x',s') \\<Longrightarrow> x'=Some xc \\<and>  s'=s" (K [
+"!!X. G\\<turnstile>(Some xc,s) -s0-> (x',s') ==> x'=Some xc \\<and>  s'=s" (K [
 	dtac (eval_evals_exec_xcpt RS conjunct2 RS conjunct2 RS mp) 1,
 	Fast_tac 1]);