--- a/src/HOL/MicroJava/J/WellType.ML Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/WellType.ML Thu Sep 21 10:42:49 2000 +0200
@@ -5,15 +5,15 @@
*)
Goal
-"\\<lbrakk> method (G,C) sig = Some (md,rT,b); wf_prog wf_mb G; G\\<turnstile>T''\\<preceq>C C\\<rbrakk>\
-\ \\<Longrightarrow> \\<exists>md' rT' b'. method (G,T'') sig = Some (md',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT";
+"[| method (G,C) sig = Some (md,rT,b); wf_prog wf_mb G; G\\<turnstile>T''\\<preceq>C C|]\
+\ ==> \\<exists>md' rT' b'. method (G,T'') sig = Some (md',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT";
by( dtac subcls_widen_methd 1);
by Auto_tac;
qed "widen_methd";
Goal
-"\\<lbrakk>method (G,C) sig = Some (md,rT,b); G\\<turnstile>T''\\<preceq>C C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
+"[|method (G,C) sig = Some (md,rT,b); G\\<turnstile>T''\\<preceq>C C; wf_prog wf_mb G|] ==> \
\ \\<exists>T' rT' b. method (G,T'') sig = Some (T',rT',b) \\<and> \
\ G\\<turnstile>rT'\\<preceq>rT \\<and> G\\<turnstile>T''\\<preceq>C T' \\<and> wf_mhead G sig rT' \\<and> wf_mb G T' (sig,rT',b)";
by( datac widen_methd 2 1);
@@ -25,25 +25,25 @@
qed "Call_lemma";
-Goal "wf_prog wf_mb G \\<Longrightarrow> method (G,Object) sig = None";
+Goal "wf_prog wf_mb G ==> method (G,Object) sig = None";
by (Asm_simp_tac 1);
qed "method_Object";
Addsimps [method_Object];
Goalw [max_spec_def]
- "x \\<in> max_spec G C sig \\<Longrightarrow> x \\<in> appl_methds G C sig";
+ "x \\<in> max_spec G C sig ==> x \\<in> appl_methds G C sig";
by (Fast_tac 1);
qed"max_spec2appl_meths";
Goalw [appl_methds_def]
-"((md,rT),pTs')\\<in>appl_methds G C (mn, pTs) \\<Longrightarrow> \
+"((md,rT),pTs')\\<in>appl_methds G C (mn, pTs) ==> \
\ \\<exists>D b. md = Class D \\<and> method (G,C) (mn, pTs') = Some (D,rT,b) \
\ \\<and> list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'";
by (Fast_tac 1);
qed "appl_methsD";
val is_type_typeof = prove_goal thy
- "(\\<forall>a. v \\<noteq> Addr a) \\<longrightarrow> (\\<exists>T. typeof t v = Some T \\<and> is_type G T)" (K [
+ "(\\<forall>a. v \\<noteq> Addr a) --> (\\<exists>T. typeof t v = Some T \\<and> is_type G T)" (K [
rtac val_.induct 1,
Fast_tac 5,
ALLGOALS Simp_tac]) RS mp;