Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/MicroJava/BV/JType.thy
changeset 10630 f89c3fc4fde1
parent 10612 779af7c58743
child 10797 028d22926a41 
--- a/src/HOL/MicroJava/BV/JType.thy	Thu Dec 07 17:59:24 2000 +0100
+++ b/src/HOL/MicroJava/BV/JType.thy	Thu Dec 07 18:22:17 2000 +0100
@@ -44,7 +44,7 @@
 
 lemma is_tyI:
   "[| is_type G T; wf_prog wf_mb G |] ==> is_ty G T"
-  by (auto simp add: is_ty_def dest: subcls_C_Object 
+  by (auto simp add: is_ty_def intro: subcls_C_Object 
            split: ty.splits ref_ty.splits)
 
 lemma is_type_conv:
isabelle