# HG changeset patch
# User wenzelm
# Date 1026836769 -7200
# Node ID a2c4faad4d3551893d8515565fedcea17b52e997
# Parent  d3c7d05d88398e9f29e6175305b31c39138cf38e
adapted to locale defs;

diff -r d3c7d05d8839 -r a2c4faad4d35 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Jul 16 18:25:48 2002 +0200
+++ b/src/HOL/Finite_Set.thy	Tue Jul 16 18:26:09 2002 +0200
@@ -720,7 +720,8 @@
     fold f e A \<cdot> fold f e B = fold f e (A Un B) \<cdot> fold f e (A Int B)"
   apply (induct set: Finites)
    apply simp
-  apply (simp add: AC LC.fold_insert insert_absorb Int_insert_left)
+  apply (simp add: AC ACe.axioms ACe_axioms_def
+    LC_axioms_def LC.fold_insert insert_absorb Int_insert_left)
   done
 
 lemma (in ACe) fold_Un_disjoint:
@@ -744,13 +745,15 @@
     have "fold (f \<circ> g) e (insert x F \<union> B) = fold (f \<circ> g) e (insert x (F \<union> B))"
       by simp
     also have "... = (f \<circ> g) x (fold (f \<circ> g) e (F \<union> B))"
-      by (rule LC.fold_insert) (insert b insert, auto simp add: left_commute)  (* FIXME import of fold_insert (!?) *)
+      by (rule LC.fold_insert)
+        (insert b insert, auto simp add: left_commute intro: LC_axioms.intro)
     also from insert have "fold (f \<circ> g) e (F \<union> B) =
       fold (f \<circ> g) e F \<cdot> fold (f \<circ> g) e B" by blast
     also have "(f \<circ> g) x ... = (f \<circ> g) x (fold (f \<circ> g) e F) \<cdot> fold (f \<circ> g) e B"
       by (simp add: AC)
     also have "(f \<circ> g) x (fold (f \<circ> g) e F) = fold (f \<circ> g) e (insert x F)"
-      by (rule LC.fold_insert [symmetric]) (insert b insert, auto simp add: left_commute)
+      by (rule LC.fold_insert [symmetric]) (insert b insert,
+	auto simp add: left_commute intro: LC_axioms.intro)
     finally show ?case .
   qed
 qed
@@ -775,7 +778,8 @@
 
 lemma setsum_insert [simp]:
     "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
-  by (simp add: setsum_def LC.fold_insert plus_ac0_left_commute)
+  by (simp add: setsum_def
+    LC_axioms_def LC.fold_insert plus_ac0_left_commute)
 
 lemma setsum_0: "setsum (\<lambda>i. 0) A = 0"
   apply (case_tac "finite A")
diff -r d3c7d05d8839 -r a2c4faad4d35 src/HOL/MicroJava/BV/LBVComplete.thy
--- a/src/HOL/MicroJava/BV/LBVComplete.thy	Tue Jul 16 18:25:48 2002 +0200
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy	Tue Jul 16 18:26:09 2002 +0200
@@ -31,7 +31,7 @@
   apply force
   done
 
-locale lbvc = lbv + 
+locale (open) lbvc = lbv + 
   fixes phi :: "'a list" ("\<phi>")
   fixes c   :: "'a list" 
   defines cert_def: "c \<equiv> make_cert step \<phi> \<bottom>"
diff -r d3c7d05d8839 -r a2c4faad4d35 src/HOL/MicroJava/BV/LBVCorrect.thy
--- a/src/HOL/MicroJava/BV/LBVCorrect.thy	Tue Jul 16 18:25:48 2002 +0200
+++ b/src/HOL/MicroJava/BV/LBVCorrect.thy	Tue Jul 16 18:26:09 2002 +0200
@@ -8,7 +8,7 @@
 
 theory LBVCorrect = LBVSpec + Typing_Framework:
 
-locale lbvs = lbv +
+locale (open) lbvs = lbv +
   fixes s0  :: 'a
   fixes c   :: "'a list"
   fixes ins :: "'b list"
diff -r d3c7d05d8839 -r a2c4faad4d35 src/HOL/MicroJava/BV/LBVSpec.thy
--- a/src/HOL/MicroJava/BV/LBVSpec.thy	Tue Jul 16 18:25:48 2002 +0200
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy	Tue Jul 16 18:26:09 2002 +0200
@@ -51,7 +51,7 @@
   "bottom r B \<equiv> \<forall>x. B <=_r x"
 
 
-locale lbv = semilat +
+locale (open) lbv = semilat +
   fixes T :: "'a" ("\<top>") 
   fixes B :: "'a" ("\<bottom>") 
   fixes step :: "'a step_type" 
diff -r d3c7d05d8839 -r a2c4faad4d35 src/HOL/MicroJava/BV/Semilat.thy
--- a/src/HOL/MicroJava/BV/Semilat.thy	Tue Jul 16 18:25:48 2002 +0200
+++ b/src/HOL/MicroJava/BV/Semilat.thy	Tue Jul 16 18:26:09 2002 +0200
@@ -63,7 +63,7 @@
  some_lub :: "('a*'a)set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
 "some_lub r x y == SOME z. is_lub r x y z";
 
-locale semilat =
+locale (open) semilat =
   fixes A :: "'a set"
     and r :: "'a ord"
     and f :: "'a binop"
diff -r d3c7d05d8839 -r a2c4faad4d35 src/HOL/NumberTheory/IntFact.thy
--- a/src/HOL/NumberTheory/IntFact.thy	Tue Jul 16 18:25:48 2002 +0200
+++ b/src/HOL/NumberTheory/IntFact.thy	Tue Jul 16 18:26:09 2002 +0200
@@ -40,7 +40,7 @@
 lemma setprod_insert [simp]:
     "finite A ==> a \<notin> A ==> setprod (insert a A) = a * setprod A"
   apply (unfold setprod_def)
-  apply (simp add: zmult_left_commute LC.fold_insert)
+  apply (simp add: zmult_left_commute LC.fold_insert [OF LC_axioms.intro])
   done