# HG changeset patch # User paulson # Date 864120782 -7200 # Node ID 6d1768e1d9bc67d4a2f02d241bd2d854c09563ce # Parent 3772723c5e413551a098fee3b9967949e742152d Removal of ex/LexProd diff -r 3772723c5e41 -r 6d1768e1d9bc src/HOL/ex/LexProd.ML --- a/src/HOL/ex/LexProd.ML Tue May 20 11:05:59 1997 +0200 +++ /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 (stac surjective_pairing 1); -by (Fast_tac 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 (!claset addSEs [Pair_inject]) 1); -qed "wf_lex_prod"; diff -r 3772723c5e41 -r 6d1768e1d9bc src/HOL/ex/LexProd.thy --- a/src/HOL/ex/LexProd.thy Tue May 20 11:05:59 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,15 +0,0 @@ -(* Title: HOL/ex/lex-prod.thy - ID: $Id$ - Author: Tobias Nipkow, TU Munich - Copyright 1993 TU Munich - -The lexicographic product of two relations. -*) - -LexProd = WF + Prod + -consts "**" :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" (infixl 70) -rules -lex_prod_def "ra**rb == {p. ? a a' b b'. - p = ((a,b),(a',b')) & ((a,a') : ra | a=a' & (b,b') : rb)}" -end -