Interpretation equations applied to attributes

--- a/src/FOL/ex/LocaleTest.thy	Fri Apr 20 16:54:57 2007 +0200
+++ b/src/FOL/ex/LocaleTest.thy	Fri Apr 20 16:55:38 2007 +0200
@@ -192,8 +192,7 @@
 
 theorem True
 proof -
-  fix alpha::i and beta::'a and gamma::o
-  (* FIXME: omitting type of beta leads to error later at interpret i6 *)
+  fix alpha::i and beta and gamma::o
   have alpha_A: "IA(alpha)" by unfold_locales simp
   interpret i5: IA [alpha] .  (* subsumed *)
   print_interps IA  (* output: <no prefix>, i1 *)
@@ -802,6 +801,8 @@
 locale Da = fixes a :: o
   assumes true: a
 
+text {* In the following examples, @{term "~ a"} is the defined concept. *}
+
 lemma (in Da) not_false: "~ a <-> False"
   apply simp apply (rule true) done
 
@@ -834,4 +835,25 @@
 lemma "False <-> False" apply (rule D1.not_false2) done
 lemma "~x & x <-> False" apply (rule D2.not_false2) done
 
+(* Unfolding in attributes *)
+
+locale Db = Da +
+  fixes b :: o
+  assumes a_iff_b: "~a <-> b"
+
+lemmas (in Db) not_false_b = not_false [unfolded a_iff_b]
+
+interpretation D2: Db ["x | ~ x" "~ (x <-> x)"]
+  apply unfold_locales apply fast done
+
+thm D2.not_false_b
+lemma "~(x <-> x) <-> False" apply (rule D2.not_false_b) done
+
+(* Subscription and attributes *)
+
+lemmas (in Db) not_false_b2 = not_false [unfolded a_iff_b]
+
+thm D2.not_false_b2
+lemma "~(x <-> x) <-> False" apply (rule D2.not_false_b2) done
+
 end

--- a/src/HOL/ex/LocaleTest2.thy	Fri Apr 20 16:54:57 2007 +0200
+++ b/src/HOL/ex/LocaleTest2.thy	Fri Apr 20 16:55:38 2007 +0200
@@ -109,14 +109,14 @@
 interpretation Dclass: Dmonoid ["op +" "0::'a::ab_group_add"]
   where "Dmonoid.inv (op +) (0::'a::ab_group_add)" = "uminus"
 proof -
-  show "Dmonoid (op +) (0::'b::ab_group_add)" by unfold_locales auto
+  show "Dmonoid (op +) (0::'a::ab_group_add)" by unfold_locales auto
   note Dclass = this (* should have this as an assumption in further goals *)
   {
     fix x
-    have "Dmonoid.inv (op +) (0::'b::ab_group_add) x = - x"
+    have "Dmonoid.inv (op +) (0::'a::ab_group_add) x = - x"
       by (auto simp: Dmonoid.inv_def [OF Dclass] equals_zero_I [symmetric])
   }
-  then show "Dmonoid.inv (op +) (0::'b::ab_group_add) == uminus"
+  then show "Dmonoid.inv (op +) (0::'a::ab_group_add) == uminus"
     by (rule_tac eq_reflection) (fast intro: ext)
 qed