src/HOL/ex/LocaleTest2.thy

 end
 
 
 interpretation dlo < dlat
 (* TODO: definition syntax is unavailable *)
-proof unfold_locales
+proof
   fix x y
   from total have "is_inf x y (if x \<sqsubseteq> y then x else y)" by (auto simp: is_inf_def)
   then show "EX inf. is_inf x y inf" by blast
 next
   fix x y
   from total have "is_sup x y (if x \<sqsubseteq> y then y else x)" by (auto simp: is_sup_def)
   then show "EX sup. is_sup x y sup" by blast
 qed
 
 interpretation dlo < ddlat
-proof unfold_locales
+proof
   fix x y z
   show "x \<sqinter> (y \<squnion> z) = x \<sqinter> y \<squnion> x \<sqinter> z" (is "?l = ?r")
     txt {* Jacobson I, p.\ 462 *}
   proof -
     { assume c: "y \<sqsubseteq> x" "z \<sqsubseteq> x"

 interpretation int: dpo ["op <= :: [int, int] => bool"]
   where "(dpo.less (op <=) (x::int) y) = (x < y)"
   txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
 proof -
   show "dpo (op <= :: [int, int] => bool)"
-    by unfold_locales auto
+    proof qed auto
   then interpret int: dpo ["op <= :: [int, int] => bool"] .
     txt {* Gives interpreted version of @{text less_def} (without condition). *}
   show "(dpo.less (op <=) (x::int) y) = (x < y)"
     by (unfold int.less_def) auto
 qed

     apply (unfold int.is_sup_def)
     by auto
 qed
 
 interpretation int: dlo ["op <= :: [int, int] => bool"]
-  by unfold_locales arith
+  proof qed arith
 
 text {* Interpreted theorems from the locales, involving defined terms. *}
 
 thm int.less_def text {* from dpo *}
 thm int.meet_left text {* from dlat *}

 interpretation nat: dpo ["op <= :: [nat, nat] => bool"]
   where "dpo.less (op <=) (x::nat) y = (x < y)"
   txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
 proof -
   show "dpo (op <= :: [nat, nat] => bool)"
-    by unfold_locales auto
+    proof qed auto
   then interpret nat: dpo ["op <= :: [nat, nat] => bool"] .
     txt {* Gives interpreted version of @{text less_def} (without condition). *}
   show "dpo.less (op <=) (x::nat) y = (x < y)"
     apply (unfold nat.less_def)
     apply auto

     apply (unfold nat.is_sup_def)
     by auto
 qed
 
 interpretation nat: dlo ["op <= :: [nat, nat] => bool"]
-  by unfold_locales arith
+  proof qed arith
 
 text {* Interpreted theorems from the locales, involving defined terms. *}
 
 thm nat.less_def text {* from dpo *}
 thm nat.meet_left text {* from dlat *}

 interpretation nat_dvd: dpo ["op dvd :: [nat, nat] => bool"]
   where "dpo.less (op dvd) (x::nat) y = (x dvd y & x ~= y)"
   txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
 proof -
   show "dpo (op dvd :: [nat, nat] => bool)"
-    by unfold_locales (auto simp: dvd_def)
+    proof qed (auto simp: dvd_def)
   then interpret nat_dvd: dpo ["op dvd :: [nat, nat] => bool"] .
     txt {* Gives interpreted version of @{text less_def} (without condition). *}
   show "dpo.less (op dvd) (x::nat) y = (x dvd y & x ~= y)"
     apply (unfold nat_dvd.less_def)
     apply auto

 
 interpretation Dfun: Dmonoid ["op o" "id :: 'a => 'a"]
   where "Dmonoid.unit (op o) id f = bij (f::'a => 'a)"
 (*    and "Dmonoid.inv (op o) id" = "inv :: ('a => 'a) => ('a => 'a)" *)
 proof -
-  show "Dmonoid op o (id :: 'a => 'a)" by unfold_locales (simp_all add: o_assoc)
+  show "Dmonoid op o (id :: 'a => 'a)" proof qed (simp_all add: o_assoc)
   note Dmonoid = this
 (*
   from this interpret Dmonoid ["op o" "id :: 'a => 'a"] .
 *)
   show "Dmonoid.unit (op o) (id :: 'a => 'a) f = bij f"

   by rule simp
 
 interpretation Dfun: Dgrp ["op o" "id :: unit => unit"]
   where "Dmonoid.inv (op o) id f = inv (f :: unit => unit)"
 proof -
-  have "Dmonoid op o (id :: 'a => 'a)" by unfold_locales (simp_all add: o_assoc)
+  have "Dmonoid op o (id :: 'a => 'a)" ..
   note Dmonoid = this
 
   show "Dgrp (op o) (id :: unit => unit)"
 apply unfold_locales
 apply (unfold Dmonoid.unit_def [OF Dmonoid])