# HG changeset patch
# User kleing
# Date 967664881 -7200
# Node ID 88366d7332ff8bf156c868885f3908915bdb14ba
# Parent  1024a2d80ac016781aeb5d71d00b5b0914397a0e
added some bind_thm

diff -r 1024a2d80ac0 -r 88366d7332ff src/HOL/MicroJava/J/Conform.ML
--- 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 => [
diff -r 1024a2d80ac0 -r 88366d7332ff src/HOL/MicroJava/J/WellForm.ML
--- 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))";