# HG changeset patch
# User kleing
# Date 950644975 -3600
# Node ID 635339ef2dca70795b87ee6e6396cd037861e308
# Parent  efb3c8253d90cc02b88af9ad520bd0d3da26d487
cosmetics

diff -r efb3c8253d90 -r 635339ef2dca src/HOL/MicroJava/BV/LBVSpec.ML
--- a/src/HOL/MicroJava/BV/LBVSpec.ML	Tue Feb 15 19:41:44 2000 +0100
+++ b/src/HOL/MicroJava/BV/LBVSpec.ML	Tue Feb 15 21:02:55 2000 +0100
@@ -76,32 +76,6 @@
  by (Asm_full_simp_tac 1);
  by (pair_tac "s2" 1);
  by (Force_tac 1);
-(* ---- 
- by (exhaust_tac "cert!Suc pc" 1);
-  by (exhaust_tac "cert!pc" 1);
-   by (Force_tac 1);
- by (res_inst_tac [("x","fst aa")] exI 1);
- by (res_inst_tac [("x","snd aa")] exI 1);
-  by (force_tac (claset(), simpset() addsimps [wtl_inst_option_def]) 1);
- by (exhaust_tac "cert!pc" 1);
-  by (force_tac (claset(), simpset() addsimps [wtl_inst_option_def]) 1);
- by (Asm_full_simp_tac 1);
-  by (force_tac (claset(), simpset() addsimps [wtl_inst_option_def]) 1);
- 
-
-  by (exhaust_tac "cert!pc" 1);
-   by (force_tac (claset(), simpset() addsimps [wtl_inst_option_def]) 1);
-   by (force_tac (claset(), simpset() addsimps [wtl_inst_option_def]) 1);
-   by (force_tac (claset(), simpset() addsimps [wtl_inst_option_def]) 1);
-
-
- by (res_inst_tac [("x","x")] exI 1);
- by (res_inst_tac [("x","y")] exI 1);
- by (exhaust_tac "cert!pc" 1);
-  by (exhaust_tac "cert!Suc pc" 1);
-   by (Force_tac 1);
-  by (force_tac (claset(), simpset() addsimps [wtl_inst_option_def]) 1);
- ------- *)
 by (Clarify_tac 1);
 by (Asm_full_simp_tac 1);
 by (Clarify_tac 1);