# HG changeset patch
# User kleing
# Date 948721691 -3600
# Node ID 037172b3623ce96e8b3a70dba983925e17746826
# Parent  1e4cb069b19d7367bc7208262d323170493446d5
reflexivity simp rules

diff -r 1e4cb069b19d -r 037172b3623c src/HOL/MicroJava/BV/Convert.ML
--- a/src/HOL/MicroJava/BV/Convert.ML	Fri Jan 21 10:45:40 2000 +0100
+++ b/src/HOL/MicroJava/BV/Convert.ML	Mon Jan 24 14:48:11 2000 +0100
@@ -4,6 +4,24 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
+
+Goalw[sup_ty_opt_def] "G \\<turnstile> t <=o t";
+by (exhaust_tac "t" 1);
+by Auto_tac;
+qed "sup_ty_opt_refl";
+Addsimps [sup_ty_opt_refl];
+
+Goalw[sup_loc_def] "G \\<turnstile> t <=l t";
+by (induct_tac "t" 1);
+by Auto_tac;
+qed "sup_loc_refl";
+Addsimps [sup_loc_refl];
+
+Goalw[sup_state_def] "G \\<turnstile> s <=s s";
+by Auto_tac;
+qed "sup_state_refl";
+Addsimps [sup_state_refl];
+
 val widen_PrimT_conv1 =
  prove_typerel "(G \\<turnstile> PrimT x \\<preceq> T) = (T = PrimT x)"
  [ prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S = PrimT x \\<longrightarrow> T = PrimT x"];
@@ -37,3 +55,4 @@
 by(simp_tac (simpset() addsimps [list_all2_Cons1]) 1);
 qed "sup_loc_Cons";
 AddIffs [sup_loc_Cons];
+