# HG changeset patch
# User kleing
# Date 965998428 -7200
# Node ID b295382e1549dbb65266d7801ef75a53dd4b0823
# Parent  d955914193e0caa329e45044fe85c19ee43db9cf
added bind_thm for widen_RefT etc.

diff -r d955914193e0 -r b295382e1549 src/HOL/MicroJava/J/TypeRel.ML
--- a/src/HOL/MicroJava/J/TypeRel.ML	Fri Aug 11 14:52:52 2000 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.ML	Fri Aug 11 14:53:48 2000 +0200
@@ -83,12 +83,15 @@
 
 val widen_RefT = prove_typerel "G\\<turnstile>RefT R\\<preceq>T \\<Longrightarrow> \\<exists>t. T=RefT t" 
 	[prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S=RefT R \\<longrightarrow> (\\<exists>t. T=RefT t)"];
+bind_thm ("widen_RefT", widen_RefT);
 
 val widen_RefT2 = prove_typerel "G\\<turnstile>S\\<preceq>RefT R \\<Longrightarrow> \\<exists>t. S=RefT t" 
 	[prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> T=RefT R \\<longrightarrow> (\\<exists>t. S=RefT t)"];
+bind_thm ("widen_RefT2", widen_RefT2);
 
 val widen_Class = prove_typerel "G\\<turnstile>Class C\\<preceq>T \\<Longrightarrow> \\<exists>D. T=Class D"
  [ prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S = Class C \\<longrightarrow> (\\<exists>D. T=Class D)"];
+bind_thm ("widen_Class", widen_Class);
 
 Goal "(G\\<turnstile>Class C\\<preceq>RefT NullT) = False"; 
 br iffI 1;