--- a/src/FOL/simpdata.ML Thu Sep 16 16:25:32 1993 +0200
+++ b/src/FOL/simpdata.ML Thu Sep 16 16:55:17 1993 +0200
@@ -84,13 +84,17 @@
open Simplifier Induction;
+infix addcongs;
+fun ss addcongs congs =
+ ss addeqcongs (congs RL [eq_reflection,iff_reflection]);
+
val IFOL_ss = empty_ss
setmksimps mk_rew_rules
setsolver
(fn prems => resolve_tac (TrueI::refl::iff_refl::notFalseI::prems))
setsubgoaler asm_simp_tac
addsimps IFOL_rews
- addcongs [imp_cong RS iff_reflection];
+ addcongs [imp_cong];
(*Classical version...*)
fun prove_fun s =