diff -r f04b33ce250f -r a4dc62a46ee4 ex/LexProd.ML
--- a/ex/LexProd.ML	Tue Oct 24 14:59:17 1995 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-(*  Title: 	HOL/ex/lex-prod.ML
-    ID:         $Id$
-    Author: 	Tobias Nipkow, TU Munich
-    Copyright   1993  TU Munich
-
-For lex-prod.thy.
-The lexicographic product of two wellfounded relations is again wellfounded.
-*)
-
-val prems = goal Prod.thy "!a b. P(<a,b>) ==> !p.P(p)";
-by (cut_facts_tac prems 1);
-by (rtac allI 1);
-by (rtac (surjective_pairing RS ssubst) 1);
-by (fast_tac HOL_cs 1);
-qed "split_all_pair";
-
-val [wfa,wfb] = goalw LexProd.thy [wf_def,LexProd.lex_prod_def]
- "[| wf(ra); wf(rb) |] ==> wf(ra**rb)";
-by (EVERY1 [rtac allI,rtac impI, rtac split_all_pair]);
-by (rtac (wfa RS spec RS mp) 1);
-by (EVERY1 [rtac allI,rtac impI]);
-by (rtac (wfb RS spec RS mp) 1);
-by (fast_tac (set_cs addSEs [Pair_inject]) 1);
-qed "wf_lex_prod";