# HG changeset patch
# User nipkow
# Date 1008595638 -3600
# Node ID 1b9db2581fe26077644f080d0863f0276a221863
# Parent  4ad978c8f5507c9bf8b326e0746e873913430cad
mods due to changed 1-point simprocs (quantifier1).

diff -r 4ad978c8f550 -r 1b9db2581fe2 src/FOL/IsaMakefile
--- a/src/FOL/IsaMakefile	Mon Dec 17 14:24:11 2001 +0100
+++ b/src/FOL/IsaMakefile	Mon Dec 17 14:27:18 2001 +0100
@@ -29,7 +29,7 @@
 $(OUT)/FOL: $(OUT)/Pure $(SRC)/Provers/blast.ML	$(SRC)/Provers/make_elim.ML \
   $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
   $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/ind.ML $(SRC)/Provers/induct_method.ML \
-  $(SRC)/Provers/simplifier.ML $(SRC)/Provers/splitter.ML \
+  $(SRC)/Provers/simplifier.ML $(SRC)/Provers/splitter.ML $(SRC)/Provers/quantifier1.ML\
   FOL.ML FOL.thy FOL_lemmas1.ML FOL_lemmas2.ML IFOL.ML IFOL.thy \
   IFOL_lemmas.ML ROOT.ML blastdata.ML cladata.ML document/root.tex \
   fologic.ML hypsubstdata.ML intprover.ML simpdata.ML
diff -r 4ad978c8f550 -r 1b9db2581fe2 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Mon Dec 17 14:24:11 2001 +0100
+++ b/src/FOL/simpdata.ML	Mon Dec 17 14:27:18 2001 +0100
@@ -225,6 +225,14 @@
 val iff_allI = allI RS
     prove_goal (the_context()) "ALL x. P(x) <-> Q(x) ==> (ALL x. P(x)) <-> (ALL x. Q(x))"
                (fn prems => [cut_facts_tac prems 1, Blast_tac 1])
+val iff_exI = allI RS
+    prove_goal (the_context()) "ALL x. P(x) <-> Q(x) ==> (EX x. P(x)) <-> (EX x. Q(x))"
+               (fn prems => [cut_facts_tac prems 1, Blast_tac 1])
+
+val all_comm = prove_goal (the_context()) "(ALL x y. P(x,y)) <-> (ALL y x. P(x,y))"
+               (fn _ => [Blast_tac 1])
+val ex_comm = prove_goal (the_context()) "(EX x y. P(x,y)) <-> (EX y x. P(x,y))"
+               (fn _ => [Blast_tac 1])
 in
 
 (** make simplification procedures for quantifier elimination **)
@@ -242,6 +250,7 @@
   (*rules*)
   val iff_reflection = iff_reflection
   val iffI = iffI
+  val iff_trans = iff_trans
   val conjI= conjI
   val conjE= conjE
   val impI = impI
@@ -250,6 +259,9 @@
   val exI  = exI
   val exE  = exE
   val iff_allI = iff_allI
+  val iff_exI = iff_exI
+  val all_comm = all_comm
+  val ex_comm = ex_comm
 end);
 
 end;
@@ -257,10 +269,10 @@
 local
 
 val ex_pattern =
-  read_cterm (Theory.sign_of (the_context ())) ("EX x. P(x) & Q(x)", FOLogic.oT)
+  read_cterm (Theory.sign_of (the_context ())) ("EX x. P(x)", FOLogic.oT)
 
 val all_pattern =
-  read_cterm (Theory.sign_of (the_context ())) ("ALL x. P(x) --> Q(x)", FOLogic.oT)
+  read_cterm (Theory.sign_of (the_context ())) ("ALL x. P(x)", FOLogic.oT)
 
 in
 val defEX_regroup =