# HG changeset patch
# User wenzelm
# Date 1333814909 -7200
# Node ID a360406f1fcbc2a071c6fbdbae043e47a84151d9
# Parent  d760049b2d189797fab1959185f58807976713cf
tuned proofs;

diff -r d760049b2d18 -r a360406f1fcb src/HOL/MicroJava/J/State.thy
--- a/src/HOL/MicroJava/J/State.thy	Sat Apr 07 17:55:35 2012 +0200
+++ b/src/HOL/MicroJava/J/State.thy	Sat Apr 07 18:08:29 2012 +0200
@@ -190,9 +190,12 @@
 apply simp
 done
 
-instantiation loc' :: equal begin
+instantiation loc' :: equal
+begin
+
 definition "HOL.equal (l :: loc') l' \<longleftrightarrow> l = l'"
-instance proof qed(simp add: equal_loc'_def)
+instance by default (simp add: equal_loc'_def)
+
 end
 
 end
diff -r d760049b2d18 -r a360406f1fcb src/HOL/MicroJava/J/Type.thy
--- a/src/HOL/MicroJava/J/Type.thy	Sat Apr 07 17:55:35 2012 +0200
+++ b/src/HOL/MicroJava/J/Type.thy	Sat Apr 07 18:08:29 2012 +0200
@@ -8,23 +8,40 @@
 theory Type imports JBasis begin
 
 typedecl cnam 
-instantiation cnam :: equal begin
+
+instantiation cnam :: equal
+begin
+
 definition "HOL.equal (cn :: cnam) cn' \<longleftrightarrow> cn = cn'"
-instance proof qed(simp add: equal_cnam_def)
+instance by default (simp add: equal_cnam_def)
+
 end
+
 text {* These instantiations only ensure that the merge in theory @{text "MicroJava"} succeeds. FIXME *}
-instantiation cnam :: typerep begin
+
+instantiation cnam :: typerep
+begin
+
 definition "typerep_class.typerep \<equiv> \<lambda>_ :: cnam itself. Typerep.Typerep (STR ''Type.cnam'') []"
-instance proof qed
+instance ..
+
 end
-instantiation cnam :: term_of begin
+
+instantiation cnam :: term_of
+begin
+
 definition "term_of_class.term_of (C :: cnam) \<equiv> 
   Code_Evaluation.Const (STR ''dummy_cnam'') (Typerep.Typerep (STR ''Type.cnam'') [])"
-instance proof qed
+instance ..
+
 end
-instantiation cnam :: partial_term_of begin
+
+instantiation cnam :: partial_term_of
+begin
+
 definition "partial_term_of_class.partial_term_of (C :: cnam itself) n = undefined"
-instance proof qed
+instance ..
+
 end
 
  -- "exceptions"
@@ -41,41 +58,73 @@
   | Cname cnam 
 
 typedecl vnam   -- "variable or field name"
-instantiation vnam :: equal begin
+
+instantiation vnam :: equal
+begin
+
 definition "HOL.equal (vn :: vnam) vn' \<longleftrightarrow> vn = vn'"
-instance proof qed(simp add: equal_vnam_def)
+instance by default (simp add: equal_vnam_def)
+
 end
-instantiation vnam :: typerep begin
+
+instantiation vnam :: typerep
+begin
+
 definition "typerep_class.typerep \<equiv> \<lambda>_ :: vnam itself. Typerep.Typerep (STR ''Type.vnam'') []"
-instance proof qed
+instance ..
+
 end
-instantiation vnam :: term_of begin
+
+instantiation vnam :: term_of
+begin
+
 definition "term_of_class.term_of (V :: vnam) \<equiv> 
   Code_Evaluation.Const (STR ''dummy_vnam'') (Typerep.Typerep (STR ''Type.vnam'') [])"
-instance proof qed
+instance ..
+
 end
-instantiation vnam :: partial_term_of begin
+
+instantiation vnam :: partial_term_of
+begin
+
 definition "partial_term_of_class.partial_term_of (V :: vnam itself) n = undefined"
-instance proof qed
+instance ..
+
 end
 
 typedecl mname  -- "method name"
-instantiation mname :: equal begin
+
+instantiation mname :: equal
+begin
+
 definition "HOL.equal (M :: mname) M' \<longleftrightarrow> M = M'"
-instance proof qed(simp add: equal_mname_def)
+instance by default (simp add: equal_mname_def)
+
 end
-instantiation mname :: typerep begin
+
+instantiation mname :: typerep
+begin
+
 definition "typerep_class.typerep \<equiv> \<lambda>_ :: mname itself. Typerep.Typerep (STR ''Type.mname'') []"
-instance proof qed
+instance ..
+
 end
-instantiation mname :: term_of begin
+
+instantiation mname :: term_of
+begin
+
 definition "term_of_class.term_of (M :: mname) \<equiv> 
   Code_Evaluation.Const (STR ''dummy_mname'') (Typerep.Typerep (STR ''Type.mname'') [])"
-instance proof qed
+instance ..
+
 end
-instantiation mname :: partial_term_of begin
+
+instantiation mname :: partial_term_of
+begin
+
 definition "partial_term_of_class.partial_term_of (M :: mname itself) n = undefined"
-instance proof qed
+instance ..
+
 end
 
 -- "names for @{text This} pointer and local/field variables"