merged
authorbulwahn
Sat May 16 20:18:26 2009 +0200 (2009-05-16)
changeset 311759b1e7159f4e5
parent 31174 f1f1e9b53c81
parent 31168 138eae508556
child 31176 92e0ed53db25
merged
     1.1 --- a/src/HOL/MicroJava/BV/BVExample.thy	Sat May 16 20:17:59 2009 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/BVExample.thy	Sat May 16 20:18:26 2009 +0200
     1.3 @@ -69,10 +69,9 @@
     1.4  lemma subcls1:
     1.5    "subcls1 E = (\<lambda>C D. (C, D) \<in> {(list_name,Object), (test_name,Object), (Xcpt NullPointer, Object),
     1.6                  (Xcpt ClassCast, Object), (Xcpt OutOfMemory, Object)})"
     1.7 -apply (simp add: subcls1_def2)
     1.8 +apply (simp add: subcls1_def2 del:singleton_conj_conv2)
     1.9  apply (simp add: name_defs class_defs system_defs E_def class_def)
    1.10 -apply (auto simp: expand_fun_eq name_defs[symmetric] class_defs split:split_if_asm)
    1.11 -apply(simp add:name_defs)+
    1.12 +apply (auto simp: expand_fun_eq split: split_if_asm)
    1.13  done
    1.14  
    1.15  text {* The subclass relation is acyclic; hence its converse is well founded: *}