--- a/src/HOL/MicroJava/J/Example.ML Tue Oct 03 18:40:25 2000 +0200
+++ b/src/HOL/MicroJava/J/Example.ML Tue Oct 03 18:44:19 2000 +0200
@@ -1,4 +1,3 @@
-open Example;
AddIs [widen.null];
@@ -130,7 +129,7 @@
qed "method_Base";
Addsimps [method_Base];
-Goal "method (tprg, Ext) = (method (tprg, Base) \\<oplus> map_of \
+Goal "method (tprg, Ext) = (method (tprg, Base) ++ map_of \
\ [((foo, [Class Base]), Ext , (Class Ext, foo_Ext))])";
br trans 1;
br method_rec_ 1;
--- a/src/HOL/MicroJava/J/JBasis.ML Tue Oct 03 18:40:25 2000 +0200
+++ b/src/HOL/MicroJava/J/JBasis.ML Tue Oct 03 18:44:19 2000 +0200
@@ -140,7 +140,7 @@
(* More about Maps *)
-val override_SomeD = prove_goalw thy [override_def] "(s \\<oplus> t) k = Some x ==> \
+val override_SomeD = prove_goalw thy [override_def] "(s ++ t) k = Some x ==> \
\ t k = Some x | t k = None \\<and> s k = Some x" (fn prems => [
cut_facts_tac prems 1,
case_tac "\\<exists>x. t k = Some x" 1,
--- a/src/HOL/MicroJava/J/TypeRel.thy Tue Oct 03 18:40:25 2000 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.thy Tue Oct 03 18:44:19 2000 +0200
@@ -52,7 +52,7 @@
"method (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None => empty
| Some (sc,fs,ms) => (case sc of None => empty | Some D =>
if is_class G D then method (G,D)
- else arbitrary) \\<oplus>
+ else arbitrary) ++
map_of (map (\\<lambda>(s, m ).
(s,(C,m))) ms))
else arbitrary)"
--- a/src/HOL/MicroJava/J/WellForm.ML Tue Oct 03 18:40:25 2000 +0200
+++ b/src/HOL/MicroJava/J/WellForm.ML Tue Oct 03 18:44:19 2000 +0200
@@ -97,7 +97,7 @@
Goal "[|wf ((subcls1 G)^-1); \\<forall>D fs ms. class G C = Some (Some D,fs,ms) --> is_class G D|] ==> method (G,C) = \
\ (case class G C of None => empty | Some (sc,fs,ms) => \
-\ (case sc of None => empty | Some D => method (G,D)) \\<oplus> \
+\ (case sc of None => empty | Some D => method (G,D)) ++ \
\ map_of (map (\\<lambda>(s,m). (s,(C,m))) ms))";
by( stac (method_TC RS (wf_subcls1_rel RS (hd method.simps))) 1);
by( asm_simp_tac (simpset() addsplits[option.split]) 1);
@@ -106,7 +106,7 @@
Goal "wf_prog wf_mb G ==> method (G,C) = \
\ (case class G C of None => empty | Some (sc,fs,ms) => \
-\ (case sc of None => empty | Some D => method (G,D)) \\<oplus> \
+\ (case sc of None => empty | Some D => method (G,D)) ++ \
\ map_of (map (\\<lambda>(s,m). (s,(C,m))) ms))";
by(rtac method_rec_lemma 1);
by( clarsimp_tac (claset(), simpset() addsimps [wf_subcls1,empty_def]