# HG changeset patch
# User paulson
# Date 906122046 -7200
# Node ID 42d13691be86fdab248a4e5fdae0707cd9b7e990
# Parent  48036910ab7ef60edf17d2ab159232157391dd38
Pruning of parameters and True assumptions

diff -r 48036910ab7e -r 42d13691be86 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Fri Sep 18 14:33:20 1998 +0200
+++ b/src/FOL/simpdata.ML	Fri Sep 18 14:34:06 1998 +0200
@@ -6,6 +6,15 @@
 Simplification data for FOL
 *)
 
+(* Elimination of True from asumptions: *)
+
+val True_implies_equals = prove_goal IFOL.thy
+ "(True ==> PROP P) == PROP P"
+(K [rtac equal_intr_rule 1, atac 2,
+          METAHYPS (fn prems => resolve_tac prems 1) 1,
+          rtac TrueI 1]);
+
+
 (*** Rewrite rules ***)
 
 fun int_prove_fun s = 
@@ -282,6 +291,10 @@
 fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
 
 
+val meta_simps =
+   [triv_forall_equality,  (* prunes params *)
+    True_implies_equals];  (* prune asms `True' *)
+
 val IFOL_simps =
    [refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @ 
     imp_simps @ iff_simps @ quant_simps;
@@ -305,8 +318,10 @@
 
 
 (*intuitionistic simprules only*)
-val IFOL_ss = FOL_basic_ss addsimps (IFOL_simps @ int_ex_simps @ int_all_simps)
-			   addcongs [imp_cong];
+val IFOL_ss = 
+    FOL_basic_ss addsimps (meta_simps @ IFOL_simps @ 
+			   int_ex_simps @ int_all_simps)
+                 addcongs [imp_cong];
 
 val cla_simps = 
     [de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2,