--- a/src/HOL/Bali/TypeRel.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Bali/TypeRel.thy Sun Nov 20 21:05:23 2011 +0100
@@ -60,7 +60,7 @@
(* direct subinterface in Decl.thy, cf. 9.1.3 *)
(* direct subclass in Decl.thy, cf. 8.1.3 *)
-lemmas subcls_direct = subcls1I [THEN r_into_rtrancl, standard]
+lemmas subcls_direct = subcls1I [THEN r_into_rtrancl]
lemma subcls_direct1:
"\<lbrakk>class G C = Some c; C \<noteq> Object;D=super c\<rbrakk> \<Longrightarrow> G\<turnstile>C\<preceq>\<^sub>C D"
@@ -554,9 +554,9 @@
done
lemmas subint_antisym =
- subint1_acyclic [THEN acyclic_impl_antisym_rtrancl, standard]
+ subint1_acyclic [THEN acyclic_impl_antisym_rtrancl]
lemmas subcls_antisym =
- subcls1_acyclic [THEN acyclic_impl_antisym_rtrancl, standard]
+ subcls1_acyclic [THEN acyclic_impl_antisym_rtrancl]
lemma widen_antisym: "\<lbrakk>G\<turnstile>S\<preceq>T; G\<turnstile>T\<preceq>S; ws_prog G\<rbrakk> \<Longrightarrow> S=T"
by (fast elim: widen_antisym_lemma subint_antisym [THEN antisymD]