# HG changeset patch
# User nipkow
# Date 887993811 -3600
# Node ID 70a50c2a920fb149c8ff7378a53cd8fd1cb5ebec
# Parent  ac6cf9f18653990280bf0c5edb332241a4df384d
Congruence rules use == in premises now.

diff -r ac6cf9f18653 -r 70a50c2a920f src/HOL/Integ/Bin.ML
--- a/src/HOL/Integ/Bin.ML	Fri Feb 20 17:56:39 1998 +0100
+++ b/src/HOL/Integ/Bin.ML	Fri Feb 20 17:56:51 1998 +0100
@@ -230,7 +230,6 @@
   by (ALLGOALS(asm_simp_tac 
                (simpset() addsimps[zminus_zadd_distrib RS sym, 
                                 znat_add RS sym]))); 
-  by (stac eq_False_conv 1); 
   by (rtac notI 1); 
   by (dres_inst_tac [("f","(% z. z +  $# Suc (Suc (n + n)))")] arg_cong 1); 
   by (Asm_full_simp_tac 1); 
diff -r ac6cf9f18653 -r 70a50c2a920f src/HOL/MiniML/Instance.ML
--- a/src/HOL/MiniML/Instance.ML	Fri Feb 20 17:56:39 1998 +0100
+++ b/src/HOL/MiniML/Instance.ML	Fri Feb 20 17:56:51 1998 +0100
@@ -220,15 +220,8 @@
 by (type_scheme.induct_tac "sch" 1);
   by (Simp_tac 1);
  by (Simp_tac 1);
- by (SELECT_GOAL Safe_tac 1);
- by (eres_inst_tac [("x","TVar n -> TVar n")] allE 1);
- by (Asm_full_simp_tac 1);
  by (Fast_tac 1);
 by (Asm_full_simp_tac 1);
-by (rtac iffI 1);
- by (eres_inst_tac [("x","bound_typ_inst S type_scheme1 -> bound_typ_inst S type_scheme2")] allE 1);
- by (Asm_full_simp_tac 1);
- by (Fast_tac 1);
 by (Fast_tac 1);
 qed "le_FVar";
 Addsimps [le_FVar];