--- a/src/HOL/MicroJava/J/Conform.ML Wed Aug 30 21:47:39 2000 +0200
+++ b/src/HOL/MicroJava/J/Conform.ML Wed Aug 30 21:48:01 2000 +0200
@@ -92,6 +92,7 @@
rtac val_.induct 1,
ALLGOALS Simp_tac,
ALLGOALS (fast_tac (HOL_cs addIs [widen_trans]))]) RS mp RS mp;
+bind_thm ("conf_widen", conf_widen);
val conf_hext' = prove_goalw thy [conf_def]
"\\<And>h. h\\<le>|h' \\<Longrightarrow> (\\<forall>v T. G,h\\<turnstile>v\\<Colon>\\<preceq>T \\<longrightarrow> G,h'\\<turnstile>v\\<Colon>\\<preceq>T)" (K [
@@ -103,6 +104,7 @@
dtac hext_objD 1,
Auto_tac]);
val conf_hext = conf_hext' RS spec RS spec RS mp;
+bind_thm ("conf_hext", conf_hext);
val new_locD = prove_goalw thy [conf_def]
"\\<lbrakk>h a = None; G,h\\<turnstile>Addr t\\<Colon>\\<preceq>T\\<rbrakk> \\<Longrightarrow> t\\<noteq>a" (fn prems => [
--- a/src/HOL/MicroJava/J/WellForm.ML Wed Aug 30 21:47:39 2000 +0200
+++ b/src/HOL/MicroJava/J/WellForm.ML Wed Aug 30 21:48:01 2000 +0200
@@ -246,6 +246,8 @@
val widen_cfs_fields = prove_goal thy "\\<And>X. \\<lbrakk>field (G,C) fn = Some (fd, fT);\
\ G\\<turnstile>C'\\<preceq>C C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> map_of (fields (G,C')) (fn, fd) = Some fT" (K[
fast_tac (HOL_cs addIs [widen_fields_mono, cfs_fields_lemma]) 1]);
+bind_thm ("widen_cfs_fields",widen_cfs_fields);
+
Goal "wf_prog wf_mb G \\<Longrightarrow> method (G,C) sig = Some (md,mh,m)\
\ \\<longrightarrow> G\\<turnstile>C\\<preceq>C md \\<and> wf_mdecl wf_mb G md (sig,(mh,m))";