split_paired_all.ML;

--- a/src/HOL/IsaMakefile	Tue Oct 20 16:38:37 1998 +0200
+++ b/src/HOL/IsaMakefile	Tue Oct 20 16:39:14 1998 +0200
@@ -30,33 +30,32 @@
 	@cd $(SRC)/Pure; $(ISATOOL) make Pure
 
 $(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/cancel_sums.ML \
-  $(SRC)/Provers/Arith/nat_transitive.ML \
+  $(SRC)/Provers/Arith/nat_transitive.ML	\
   $(SRC)/Provers/Arith/abel_cancel.ML $(SRC)/Provers/blast.ML \
   $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
   $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/simplifier.ML \
-  $(SRC)/Provers/splitter.ML $(SRC)/Pure/section_utils.ML \
-  $(SRC)/TFL/dcterm.sml $(SRC)/TFL/post.sml $(SRC)/TFL/rules.new.sml \
-  $(SRC)/TFL/rules.sig $(SRC)/TFL/sys.sml $(SRC)/TFL/tfl.sig \
-  $(SRC)/TFL/tfl.sml $(SRC)/TFL/thms.sig $(SRC)/TFL/thms.sml \
-  $(SRC)/TFL/thry.sig $(SRC)/TFL/thry.sml $(SRC)/TFL/usyntax.sig \
-  $(SRC)/TFL/usyntax.sml $(SRC)/TFL/utils.sig $(SRC)/TFL/utils.sml \
-  Arith.ML Arith.thy Datatype.thy \
-  Divides.ML Divides.thy Finite.ML Finite.thy Fun.ML Fun.thy \
-  Gfp.ML Gfp.thy HOL.ML HOL.thy Inductive.thy \
-  Integ/Bin.ML Integ/Bin.thy Integ/Equiv.ML Integ/Equiv.thy \
-  Integ/IntDef.ML Integ/IntDef.thy Integ/Int.ML Integ/Int.thy \
-  Integ/simproc.ML \
-  Lfp.ML Lfp.thy List.ML List.thy Main.thy Map.ML Map.thy Nat.ML \
-  Nat.thy NatDef.ML NatDef.thy Option.ML Option.thy Ord.ML Ord.thy \
-  Power.ML Power.thy Prod.ML Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML \
+  $(SRC)/Provers/split_paired_all.ML $(SRC)/Provers/splitter.ML \
+  $(SRC)/Pure/section_utils.ML $(SRC)/TFL/dcterm.sml \
+  $(SRC)/TFL/post.sml $(SRC)/TFL/rules.new.sml $(SRC)/TFL/rules.sig \
+  $(SRC)/TFL/sys.sml $(SRC)/TFL/tfl.sig $(SRC)/TFL/tfl.sml \
+  $(SRC)/TFL/thms.sig $(SRC)/TFL/thms.sml $(SRC)/TFL/thry.sig \
+  $(SRC)/TFL/thry.sml $(SRC)/TFL/usyntax.sig $(SRC)/TFL/usyntax.sml \
+  $(SRC)/TFL/utils.sig $(SRC)/TFL/utils.sml Arith.ML Arith.thy \
+  Datatype.thy Divides.ML Divides.thy Finite.ML Finite.thy Fun.ML \
+  Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy Inductive.thy Integ/Bin.ML \
+  Integ/Bin.thy Integ/Equiv.ML Integ/Equiv.thy Integ/IntDef.ML \
+  Integ/IntDef.thy Integ/Int.ML Integ/Int.thy Integ/simproc.ML Lfp.ML \
+  Lfp.thy List.ML List.thy Main.thy Map.ML Map.thy Nat.ML Nat.thy \
+  NatDef.ML NatDef.thy Option.ML Option.thy Ord.ML Ord.thy Power.ML \
+  Power.thy Prod.ML Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML \
   RelPow.thy Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy \
-  String.thy Sum.ML Sum.thy \
-  Tools/datatype_aux.ML Tools/datatype_abs_proofs.ML Tools/datatype_package.ML \
+  String.thy Sum.ML Sum.thy Tools/datatype_aux.ML \
+  Tools/datatype_abs_proofs.ML Tools/datatype_package.ML \
   Tools/datatype_prop.ML Tools/datatype_rep_proofs.ML \
-  Tools/inductive_package.ML Tools/primrec_package.ML Tools/record_package.ML \
-  Tools/typedef_package.ML Trancl.ML Trancl.thy Univ.ML Univ.thy \
-  Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML \
-  WF_Rel.thy arith_data.ML cladata.ML equalities.ML \
+  Tools/inductive_package.ML Tools/primrec_package.ML \
+  Tools/record_package.ML Tools/typedef_package.ML Trancl.ML \
+  Trancl.thy Univ.ML Univ.thy Vimage.ML Vimage.thy WF.ML WF.thy \
+  WF_Rel.ML WF_Rel.thy arith_data.ML cladata.ML equalities.ML \
   equalities.thy hologic.ML mono.ML mono.thy simpdata.ML subset.ML \
   subset.thy thy_syntax.ML
 	@$(ISATOOL) usedir -b $(OUT)/Pure HOL

--- a/src/HOL/Prod.ML	Tue Oct 20 16:38:37 1998 +0200
+++ b/src/HOL/Prod.ML	Tue Oct 20 16:39:14 1998 +0200
@@ -67,25 +67,9 @@
 	rtac exI 1, rtac exI 1, rtac surjective_pairing 1]);
 Addsimps [surj_pair];
 
-(* lemmas for splitting paired `!!' *)
-local 
-    val lemma1 = prove_goal Prod.thy "(!!x. PROP P x) ==> (!!a b. PROP P(a,b))" 
-		 (fn prems => [resolve_tac prems 1]);
 
-    val psig = sign_of Prod.thy;
-    val pT = Sign.read_typ (psig, K None) "?'a*?'b=>prop";
-    val PeqP = reflexive(read_cterm psig ("P", pT));
-    val psplit = zero_var_indexes(read_instantiate [("p","x")]
-                                  surjective_pairing RS eq_reflection);
-    val adhoc = combination PeqP psplit;
-    val lemma = prove_goal Prod.thy "(!!a b. PROP P(a,b)) ==> PROP P x" 
-		(fn prems => [rewtac adhoc, resolve_tac prems 1]);
-    val lemma2 = prove_goal Prod.thy "(!!a b. PROP P(a,b)) ==> (!!x. PROP P x)"
-		(fn prems => [rtac lemma 1, resolve_tac prems 1]);
-in
-  val split_paired_all = equal_intr lemma1 lemma2
-end;
-bind_thm("split_paired_all", split_paired_all);
+bind_thm ("split_paired_all",
+  SplitPairedAll.rule (standard (surjective_pairing RS eq_reflection)));
 (*
 Addsimps [split_paired_all] does not work with simplifier 
 because it also affects premises in congrence rules, 

--- a/src/HOL/ROOT.ML	Tue Oct 20 16:38:37 1998 +0200
+++ b/src/HOL/ROOT.ML	Tue Oct 20 16:39:14 1998 +0200
@@ -17,6 +17,7 @@
 use "thy_syntax.ML";
 
 use "$ISABELLE_HOME/src/Provers/simplifier.ML";
+use "$ISABELLE_HOME/src/Provers/split_paired_all.ML";
 use "$ISABELLE_HOME/src/Provers/splitter.ML";
 use "$ISABELLE_HOME/src/Provers/hypsubst.ML";
 use "$ISABELLE_HOME/src/Provers/classical.ML";
@@ -39,9 +40,6 @@
 use_thy "Sum";
 use_thy "Gfp";
 
-use "Tools/record_package.ML";
-use_thy "Record";
-
 use_thy "NatDef";
 
 use "Tools/inductive_package.ML";
@@ -55,6 +53,9 @@
 use "Tools/primrec_package.ML";
 use_thy "Datatype";
 
+use "Tools/record_package.ML";
+use_thy "Record";
+
 use_thy "Arith";
 use "arith_data.ML";