# HG changeset patch
# User wenzelm
# Date 1003521608 -7200
# Node ID b2a9853ec6ddd7110acff5a20df20e5c38d1acf8
# Parent  805b0c13607e0137c3ddde33b72b2d7732db9393
got rid of Provers/split_paired_all.ML;

diff -r 805b0c13607e -r b2a9853ec6dd src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Oct 19 21:59:33 2001 +0200
+++ b/src/HOL/IsaMakefile	Fri Oct 19 22:00:08 2001 +0200
@@ -74,8 +74,7 @@
   $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
   $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/induct_method.ML \
   $(SRC)/Provers/make_elim.ML $(SRC)/Provers/simplifier.ML \
-  $(SRC)/Provers/split_paired_all.ML $(SRC)/Provers/splitter.ML \
-  $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML \
+  $(SRC)/Provers/splitter.ML $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML \
   $(SRC)/TFL/rules.ML $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML \
   $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML Calculation.thy \
   Datatype.thy Datatype_Universe.ML Datatype_Universe.thy Divides.ML \
@@ -92,7 +91,7 @@
   Lfp.thy List.ML List.thy Main.ML Main.thy Map.ML Map.thy Nat.ML \
   Nat.thy NatArith.ML NatArith.thy NatDef.ML NatDef.thy Numeral.thy \
   Option.ML Option.thy Power.ML Power.thy PreList.thy \
-  Product_Type_lemmas.ML Product_Type.thy ROOT.ML Recdef.thy Record.thy \
+  Product_Type.ML Product_Type.thy ROOT.ML Recdef.thy Record.thy \
   Relation.ML Relation.thy Relation_Power.ML Relation_Power.thy \
   SVC_Oracle.ML SVC_Oracle.thy Set.ML Set.thy SetInterval.ML \
   SetInterval.thy String.thy Sum_Type.ML Sum_Type.thy \
diff -r 805b0c13607e -r b2a9853ec6dd src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Fri Oct 19 21:59:33 2001 +0200
+++ b/src/HOL/ROOT.ML	Fri Oct 19 22:00:08 2001 +0200
@@ -17,7 +17,6 @@
 use "hologic.ML";
 
 use "~~/src/Provers/simplifier.ML";
-use "~~/src/Provers/split_paired_all.ML";
 use "~~/src/Provers/splitter.ML";
 use "~~/src/Provers/hypsubst.ML";
 use "~~/src/Provers/induct_method.ML";
diff -r 805b0c13607e -r b2a9853ec6dd src/Provers/split_paired_all.ML
--- a/src/Provers/split_paired_all.ML	Fri Oct 19 21:59:33 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,64 +0,0 @@
-(*  Title:      Provers/split_paired_all.ML
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-
-Derived rule for turning meta-level surjective pairing into split rule:
-
-           p == (fst p, snd p)
- --------------------------------------
-  !!a b. PROP (a, b) == !! x. PROP P x
-
-*)
-
-signature SPLIT_PAIRED_ALL =
-sig
-  val rule_params: string -> string -> thm -> thm
-  val rule: thm -> thm
-end;
-
-structure SplitPairedAll: SPLIT_PAIRED_ALL =
-struct
-
-
-fun all x T t = Term.all T $ Abs (x, T, t);
-
-infixr ==>;
-val op ==> = Logic.mk_implies;
-
-
-fun rule_params a b raw_surj_pair =
-  let
-    val ct = Thm.cterm_of (Thm.sign_of_thm raw_surj_pair);
-
-    val surj_pair = Drule.unvarify (standard raw_surj_pair);
-    val used = Term.add_term_names (#prop (Thm.rep_thm surj_pair), []);
-
-    val (p, con $ _ $ _) = Logic.dest_equals (#prop (rep_thm surj_pair));
-    val pT as Type (_, [aT, bT]) = fastype_of p;
-    val P = Free (variant used "P", pT --> propT);
-
-   (*"!!a b. PROP (a, b)"*)
-   val all_a_b = all a aT (all b bT (P $ (con $ Bound 1 $ Bound 0)));
-   (*"!!x. PROP P x"*)
-   val all_x = all "x" pT (P $ Bound 0);
-
-   (*lemma "P p == P (fst p, snd p)"*)
-   val lem1 = Thm.combination (Thm.reflexive (ct P)) surj_pair;
-
-   (*lemma "(!!a b. PROP P (a,b)) ==> PROP P p"*)
-   val lem2 = prove_goalw_cterm [lem1] (ct (all_a_b ==> P $ p))
-     (fn prems => [resolve_tac prems 1]);
-
-   (*lemma "(!!a b. PROP P (a,b)) ==> !!x. PROP P x"*)
-   val lem3 = prove_goalw_cterm [] (ct (all_a_b ==> all_x))
-     (fn prems => [rtac lem2 1, resolve_tac prems 1]);
-
-   (*lemma "(!!x. PROP P x) ==> !!a b. PROP P (a,b)"*)
-   val lem4 = prove_goalw_cterm [] (ct (all_x ==> all_a_b))
-     (fn prems => [resolve_tac prems 1]);
-  in standard (Thm.equal_intr lem4 lem3) end;
-
-val rule = rule_params "a" "b";
-
-
-end;