# HG changeset patch
# User wenzelm
# Date 970591459 -7200
# Node ID 412a3ced6efd097bdcfb27cacbc275c6d912c3c2
# Parent  d1c2bef01e2f81859a45c881ec1fa88723ead6c7
eliminated \<oplus>;

diff -r d1c2bef01e2f -r 412a3ced6efd src/HOL/MicroJava/J/Example.ML
--- 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;
diff -r d1c2bef01e2f -r 412a3ced6efd src/HOL/MicroJava/J/JBasis.ML
--- 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,
diff -r d1c2bef01e2f -r 412a3ced6efd src/HOL/MicroJava/J/TypeRel.thy
--- 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)"
diff -r d1c2bef01e2f -r 412a3ced6efd src/HOL/MicroJava/J/WellForm.ML
--- 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]