# HG changeset patch # User skalberg # Date 1062028600 -7200 # Node ID 0cab06e3bbd072a6b8537b6a9635256abeeff751 # Parent edd5a2ea38078920efdc03e6aedf47278eca1f0c Extended the notion of letter and digit, such that now one may use greek, gothic, euler, or calligraphic letters as normal letters. diff -r edd5a2ea3807 -r 0cab06e3bbd0 NEWS --- a/NEWS Wed Aug 27 18:22:34 2003 +0200 +++ b/NEWS Thu Aug 28 01:56:40 2003 +0200 @@ -4,6 +4,20 @@ New in this Isabelle release ---------------------------- +*** General *** + +* Pure: Greek letters (except small lambda, \), as well as gothic + (\,...\,\,...,\), caligraphic (\...\), and + euler (\...\), are now considered normal letters, and can + therefore be used anywhere where an ASCII letter (a...zA...Z) has + until now. Similarily, the symbol digits \<0>...\<9> are now + considered normal digits. COMPATIBILITY: This obviously changes the + parsing of some terms, especially where a symbol has been used as a + binder, say '\x. ...', which is now a type error since \x + will be parsed as an identifier. Fix it by inserting a space around + former symbols. Call 'isatool fixgreek' to try to fix parsing + errors in existing theory and ML files. + *** HOL *** * 'specification' command added, allowing for definition by diff -r edd5a2ea3807 -r 0cab06e3bbd0 lib/Tools/fixgreek --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/lib/Tools/fixgreek Thu Aug 28 01:56:40 2003 +0200 @@ -0,0 +1,42 @@ +#!/usr/bin/env bash +# +# $Id$ +# Author: Sebastian Skalberg, TU Muenchen +# License: GPL (GNU GENERAL PUBLIC LICENSE) +# +# DESCRIPTION: fix problems with greek and other foreign letters + + +## diagnostics + +PRG="$(basename "$0")" + +function usage() +{ + echo + echo "Usage: $PRG [FILES|DIRS...]" + echo + echo " Recursively find .thy files, fixing parse problems stemming" + echo " from the classification change of greek and other foreign" + echo " letters from symbols to letters." + echo + echo " Renames old versions of FILES by appending \"~~\"." + echo + exit 1 +} + + +## process command line + +[ "$#" -eq 0 -o "$1" = "-?" ] && usage + +SPECS="$@"; shift "$#" + + +## main + +#set by configure +AUTO_PERL=perl + +find $SPECS -name \*.thy -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixgreek.pl" +find $SPECS -name \*.ML -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixgreek.pl" diff -r edd5a2ea3807 -r 0cab06e3bbd0 lib/scripts/fixgreek.pl --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/lib/scripts/fixgreek.pl Thu Aug 28 01:56:40 2003 +0200 @@ -0,0 +1,50 @@ +# +# $Id$ +# Author: Sebastian Skalberg, TU Muenchen +# License: GPL (GNU GENERAL PUBLIC LICENSE) +# +# fixgreek.pl - fix problems with greek and other foreign letters now +# being classified as letters instead of symbols. +# + +sub fixgreek { + my ($file) = @_; + + open (FILE, $file) || die $!; + undef $/; $text = ; $/ = "\n"; # slurp whole file + close FILE || die $!; + + $_ = $text; + + s/(\\<(a|b|c|d|e|f|g|h|i|j|k|l|m|n|o|p|q|r|s|t|u|v|w|x|y|z|A|B|C|D|E|F|G|H|I|J|K|L|M|N|O|P|Q|R|S|T|U|V|W|X|Y|Z)>)([a-zA-Z0-9])/$1 $3/sg; + + s/([a-zA-Z][a-zA-Z0-9]*)(\\<(a|b|c|d|e|f|g|h|i|j|k|l|m|n|o|p|q|r|s|t|u|v|w|x|y|z|A|B|C|D|E|F|G|H|I|J|K|L|M|N|O|P|Q|R|S|T|U|V|W|X|Y|Z)>)/$1 $2/sg; + + s/(\\<(aa|bb|cc|dd|ee|ff|gg|hh|ii|jj|kk|ll|mm|nn|oo|pp|qq|rr|ss|tt|uu|vv|ww|xx|yy|zz|AA|BB|CC|DD|EE|FF|GG|HH|II|JJ|KK|LL|MM|NN|OO|PP|QQ|RR|SS|TT|UU|VV|WW|XX|YY|ZZ)>)([a-zA-Z0-9])/$1 $3/sg; + + s/([a-zA-Z][a-zA-Z0-9]*)(\\<(aa|bb|cc|dd|ee|ff|gg|hh|ii|jj|kk|ll|mm|nn|oo|pp|qq|rr|ss|tt|uu|vv|ww|xx|yy|zz|AA|BB|CC|DD|EE|FF|GG|HH|II|JJ|KK|LL|MM|NN|OO|PP|QQ|RR|SS|TT|UU|VV|WW|XX|YY|ZZ)>)/$1 $2/sg; + + s/(\\<(alpha|beta|gamma|delta|epsilon|zeta|eta|theta|iota|kappa|mu|nu|xi|pi|rho|sigma|tau|upsilon|phi|psi|omega|Gamma|Delta|Theta|Lambda|Xi|Pi|Sigma|Upsilon|Phi|Psi|Omega)>)([a-zA-Z0-9])/$1 $3/sg; + + s/([a-zA-Z][a-zA-Z0-9]*)(\\<(alpha|beta|gamma|delta|epsilon|zeta|eta|theta|iota|kappa|mu|nu|xi|pi|rho|sigma|tau|upsilon|phi|psi|omega|Gamma|Delta|Theta|Lambda|Xi|Pi|Sigma|Upsilon|Phi|Psi|Omega)>)/$1 $2/sg; + + $result = $_; + + if ($text ne $result) { + print STDERR "fixing $file\n"; + if (! -f "$file~~") { + rename $file, "$file~~" || die $!; + } + open (FILE, "> $file") || die $!; + print FILE $result; + close FILE || die $!; + } +} + + +## main + +foreach $file (@ARGV) { + eval { &fixgreek($file); }; + if ($@) { print STDERR "*** fixgreek $file: ", $@, "\n"; } +} diff -r edd5a2ea3807 -r 0cab06e3bbd0 src/HOL/Bali/Decl.thy --- a/src/HOL/Bali/Decl.thy Wed Aug 27 18:22:34 2003 +0200 +++ b/src/HOL/Bali/Decl.thy Thu Aug 28 01:56:40 2003 +0200 @@ -491,7 +491,7 @@ done lemma subcls1_def2: - "subcls1 G = (\C\{C. is_class G C}. {D. C\Object \ super (the(class G C))=D})" + "subcls1 G = (\ C\{C. is_class G C}. {D. C\Object \ super (the(class G C))=D})" apply (unfold subcls1_def) apply auto done diff -r edd5a2ea3807 -r 0cab06e3bbd0 src/HOL/Bali/State.thy --- a/src/HOL/Bali/State.thy Wed Aug 27 18:22:34 2003 +0200 +++ b/src/HOL/Bali/State.thy Thu Aug 28 01:56:40 2003 +0200 @@ -266,7 +266,7 @@ constdefs new_Addr :: "heap \ loc option" - "new_Addr h \ if (\a. h a \ None) then None else Some (\a. h a = None)" + "new_Addr h \ if (\a. h a \ None) then None else Some (\ a. h a = None)" lemma new_AddrD: "new_Addr h = Some a \ h a = None" apply (unfold new_Addr_def) diff -r edd5a2ea3807 -r 0cab06e3bbd0 src/HOL/Bali/Type.thy --- a/src/HOL/Bali/Type.thy Wed Aug 27 18:22:34 2003 +0200 +++ b/src/HOL/Bali/Type.thy Thu Aug 28 01:56:40 2003 +0200 @@ -51,7 +51,7 @@ constdefs the_Class :: "ty \ qtname" - "the_Class T \ \C. T = Class C" (** primrec not possible here **) + "the_Class T \ \ C. T = Class C" (** primrec not possible here **) lemma the_Class_eq [simp]: "the_Class (Class C)= C" by (auto simp add: the_Class_def) diff -r edd5a2ea3807 -r 0cab06e3bbd0 src/HOL/MicroJava/J/TypeRel.thy --- a/src/HOL/MicroJava/J/TypeRel.thy Wed Aug 27 18:22:34 2003 +0200 +++ b/src/HOL/MicroJava/J/TypeRel.thy Thu Aug 28 01:56:40 2003 +0200 @@ -42,7 +42,7 @@ done lemma subcls1_def2: -"subcls1 G = (\C\{C. is_class G C} . {D. C\Object \ fst (the (class G C))=D})" +"subcls1 G = (\ C\{C. is_class G C} . {D. C\Object \ fst (the (class G C))=D})" by (auto simp add: is_class_def dest: subcls1D intro: subcls1I) lemma finite_subcls1: "finite (subcls1 G)" diff -r edd5a2ea3807 -r 0cab06e3bbd0 src/HOL/NanoJava/TypeRel.thy --- a/src/HOL/NanoJava/TypeRel.thy Wed Aug 27 18:22:34 2003 +0200 +++ b/src/HOL/NanoJava/TypeRel.thy Thu Aug 28 01:56:40 2003 +0200 @@ -55,7 +55,7 @@ done lemma subcls1_def2: -"subcls1 = (\C\{C. is_class C} . {D. C\Object \ super (the (class C)) = D})" +"subcls1 = (\ C\{C. is_class C} . {D. C\Object \ super (the (class C)) = D})" apply (unfold subcls1_def is_class_def) apply auto done diff -r edd5a2ea3807 -r 0cab06e3bbd0 src/HOLCF/FOCUS/Buffer.ML --- a/src/HOLCF/FOCUS/Buffer.ML Wed Aug 27 18:22:34 2003 +0200 +++ b/src/HOLCF/FOCUS/Buffer.ML Thu Aug 28 01:56:40 2003 +0200 @@ -247,7 +247,7 @@ Goalw [BufSt_def, BufSt_P_def] "BufEq <= BufSt"; by Safe_tac; by (EVERY'[rename_tac "f", res_inst_tac - [("x","\\s. case s of Sd d => \\x. f\\(Md d\\x)| \\ => f")] bexI] 1); + [("x","\\s. case s of Sd d => \\ x. f\\(Md d\\x)| \\ => f")] bexI] 1); by ( Simp_tac 1); by (etac weak_coinduct_image 1); by (rewtac BufSt_F_def); diff -r edd5a2ea3807 -r 0cab06e3bbd0 src/HOLCF/FOCUS/Fstream.thy --- a/src/HOLCF/FOCUS/Fstream.thy Wed Aug 27 18:22:34 2003 +0200 +++ b/src/HOLCF/FOCUS/Fstream.thy Thu Aug 28 01:56:40 2003 +0200 @@ -39,7 +39,7 @@ defs - fscons_def "fscons a \\ \\s. Def a && s" + fscons_def "fscons a \\ \\ s. Def a && s" fsfilter_def "fsfilter A \\ sfilter\\(flift2 (\\x. x\\A))" end diff -r edd5a2ea3807 -r 0cab06e3bbd0 src/HOLCF/ex/Stream.ML --- a/src/HOLCF/ex/Stream.ML Wed Aug 27 18:22:34 2003 +0200 +++ b/src/HOLCF/ex/Stream.ML Thu Aug 28 01:56:40 2003 +0200 @@ -358,7 +358,7 @@ section "smap"; bind_thm ("smap_unfold", fix_prover2 thy smap_def - "smap = (\\f s. case s of x && l => f\\x && smap\\f\\l)"); + "smap = (\\ f s. case s of x && l => f\\x && smap\\f\\l)"); Goal "smap\\f\\\\ = \\"; by (stac smap_unfold 1); @@ -570,7 +570,7 @@ section "sfilter"; bind_thm ("sfilter_unfold", fix_prover2 thy sfilter_def - "sfilter = (\\p s. case s of x && xs => \ + "sfilter = (\\ p s. case s of x && xs => \ \ If p\\x then x && sfilter\\p\\xs else sfilter\\p\\xs fi)"); Goal "sfilter\\\\ = \\"; diff -r edd5a2ea3807 -r 0cab06e3bbd0 src/HOLCF/ex/Stream.thy --- a/src/HOLCF/ex/Stream.thy Wed Aug 27 18:22:34 2003 +0200 +++ b/src/HOLCF/ex/Stream.thy Thu Aug 28 01:56:40 2003 +0200 @@ -18,8 +18,8 @@ defs - smap_def "smap == fix\\(\\h f s. case s of x && xs => f\\x && h\\f\\xs)" - sfilter_def "sfilter == fix\\(\\h p s. case s of x && xs => + smap_def "smap == fix\\(\\ h f s. case s of x && xs => f\\x && h\\f\\xs)" + sfilter_def "sfilter == fix\\(\\ h p s. case s of x && xs => If p\\x then x && h\\p\\xs else h\\p\\xs fi)" slen_def "#s == if stream_finite s then Fin (LEAST n. stream_take n\\s = s) else \\" diff -r edd5a2ea3807 -r 0cab06e3bbd0 src/Pure/General/symbol.ML --- a/src/Pure/General/symbol.ML Wed Aug 27 18:22:34 2003 +0200 +++ b/src/Pure/General/symbol.ML Thu Aug 28 01:56:40 2003 +0200 @@ -85,13 +85,57 @@ fun is_ascii s = size s = 1 andalso ord s < 128; +local + fun wrap s = "\\<" ^ s ^ ">" + val pre_digits = + ["zero","one","two","three","four", + "five","six","seven","eight","nine"] + + val cal_letters = + ["A","B","C","D","E","F","G","H","I","J","K","L","M", + "N","O","P","Q","R","S","T","U","V","W","X","Y","Z"] + + val small_letters = + ["a","b","c","d","e","f","g","h","i","j","k","l","m", + "n","o","p","q","r","s","t","u","v","w","x","y","z"] + + val goth_letters = + ["AA","BB","CC","DD","EE","FF","GG","HH","II","JJ","KK","LL","MM", + "NN","OO","PP","QQ","RR","SS","TT","UU","VV","WW","XX","YY","ZZ", + "aa","bb","cc","dd","ee","ff","gg","hh","ii","jj","kk","ll","mm", + "nn","oo","pp","qq","rr","ss","tt","uu","vv","ww","xx","yy","zz"] + + val greek_letters = + ["alpha","beta","gamma","delta","epsilon","zeta","eta","theta", + "iota","kappa",(*"lambda",*)"mu","nu","xi","pi","rho","sigma","tau", + "upsilon","phi","psi","omega","Gamma","Delta","Theta","Lambda", + "Xi","Pi","Sigma","Upsilon","Phi","Psi","Omega"] + + val bbb_letters = ["bool","complex","nat","rat","real","int"] + + val pre_letters = + cal_letters @ + small_letters @ + goth_letters @ + greek_letters +in +val ext_digits = map wrap pre_digits +val ext_letters = map wrap pre_letters +val ext_letdigs = ext_digits @ ext_letters +fun is_ext_digit s = String.isPrefix "\\<" s andalso s mem ext_digits +fun is_ext_letter s = String.isPrefix "\\<" s andalso s mem ext_letters +fun is_ext_letdig s = String.isPrefix "\\<" s andalso s mem ext_letdigs +end + fun is_letter s = - size s = 1 andalso - (ord "A" <= ord s andalso ord s <= ord "Z" orelse - ord "a" <= ord s andalso ord s <= ord "z"); + (size s = 1 andalso + (ord "A" <= ord s andalso ord s <= ord "Z" orelse + ord "a" <= ord s andalso ord s <= ord "z")) + orelse is_ext_letter s fun is_digit s = - size s = 1 andalso ord "0" <= ord s andalso ord s <= ord "9"; + (size s = 1 andalso ord "0" <= ord s andalso ord s <= ord "9") + orelse is_ext_digit s fun is_quasi "_" = true | is_quasi "'" = true @@ -107,10 +151,12 @@ fun is_letdig s = is_quasi_letter s orelse is_digit s; fun is_symbolic s = - size s > 2 andalso nth_elem_string (2, s) <> "^"; + size s > 2 andalso nth_elem_string (2, s) <> "^" + andalso not (is_ext_letdig s); fun is_printable s = size s = 1 andalso ord space <= ord s andalso ord s <= ord "~" orelse + is_ext_letdig s orelse is_symbolic s; fun is_identifier s = diff -r edd5a2ea3807 -r 0cab06e3bbd0 src/ZF/AC.thy --- a/src/ZF/AC.thy Wed Aug 27 18:22:34 2003 +0200 +++ b/src/ZF/AC.thy Thu Aug 28 01:56:40 2003 +0200 @@ -26,7 +26,7 @@ apply (erule bspec, assumption) done -lemma AC_Pi_Pow: "\f. f \ (\X \ Pow(C)-{0}. X)" +lemma AC_Pi_Pow: "\f. f \ (\ X \ Pow(C)-{0}. X)" apply (rule_tac B1 = "%x. x" in AC_Pi [THEN exE]) apply (erule_tac [2] exI, blast) done @@ -52,7 +52,7 @@ apply (erule_tac [2] fun_weaken_type, blast+) done -lemma AC_Pi0: "0 \ A ==> \f. f \ (\x \ A. x)" +lemma AC_Pi0: "0 \ A ==> \f. f \ (\ x \ A. x)" apply (rule AC_Pi) apply (simp_all add: non_empty_family) done diff -r edd5a2ea3807 -r 0cab06e3bbd0 src/ZF/AC/AC15_WO6.thy --- a/src/ZF/AC/AC15_WO6.thy Wed Aug 27 18:22:34 2003 +0200 +++ b/src/ZF/AC/AC15_WO6.thy Thu Aug 28 01:56:40 2003 +0200 @@ -262,7 +262,7 @@ lemma AC13_AC1_lemma: "\B \ A. f(B)\0 & f(B)<=B & f(B) \ 1 - ==> (\x \ A. THE y. f(x)={y}) \ (\X \ A. X)" + ==> (\x \ A. THE y. f(x)={y}) \ (\ X \ A. X)" apply (rule lam_type) apply (drule bspec, assumption) apply (elim conjE) diff -r edd5a2ea3807 -r 0cab06e3bbd0 src/ZF/AC/AC17_AC1.thy --- a/src/ZF/AC/AC17_AC1.thy Wed Aug 27 18:22:34 2003 +0200 +++ b/src/ZF/AC/AC17_AC1.thy Thu Aug 28 01:56:40 2003 +0200 @@ -14,7 +14,7 @@ (** AC0 is equivalent to AC1. AC0 comes from Suppes, AC1 from Rubin & Rubin **) -lemma AC0_AC1_lemma: "[| f:(\X \ A. X); D \ A |] ==> \g. g:(\X \ D. X)" +lemma AC0_AC1_lemma: "[| f:(\ X \ A. X); D \ A |] ==> \g. g:(\ X \ D. X)" by (fast intro!: lam_type apply_type) lemma AC0_AC1: "AC0 ==> AC1" @@ -28,7 +28,7 @@ (**** The proof of AC1 ==> AC17 ****) -lemma AC1_AC17_lemma: "f \ (\X \ Pow(A) - {0}. X) ==> f \ (Pow(A) - {0} -> A)" +lemma AC1_AC17_lemma: "f \ (\ X \ Pow(A) - {0}. X) ==> f \ (Pow(A) - {0} -> A)" apply (rule Pi_type, assumption) apply (drule apply_type, assumption, fast) done @@ -143,7 +143,7 @@ (* ********************************************************************** *) lemma AC1_AC2_aux1: - "[| f:(\X \ A. X); B \ A; 0\A |] ==> {f`B} \ B Int {f`C. C \ A}" + "[| f:(\ X \ A. X); B \ A; 0\A |] ==> {f`B} \ B Int {f`C. C \ A}" by (fast elim!: apply_type) lemma AC1_AC2_aux2: @@ -177,7 +177,7 @@ lemma AC2_AC1_aux3: "\D \ {E*{E}. E \ A}. \y. D Int C = {y} - ==> (\x \ A. fst(THE z. (x*{x} Int C = {z}))) \ (\X \ A. X)" + ==> (\x \ A. fst(THE z. (x*{x} Int C = {z}))) \ (\ X \ A. X)" apply (rule lam_type) apply (drule bspec, blast) apply (blast intro: AC2_AC1_aux2 fst_type) @@ -233,7 +233,7 @@ (* ********************************************************************** *) lemma AC3_AC1_lemma: - "b\A ==> (\x \ {a \ A. id(A)`a\b}. id(A)`x) = (\x \ A. x)" + "b\A ==> (\ x \ {a \ A. id(A)`a\b}. id(A)`x) = (\ x \ A. x)" apply (simp add: id_def cong add: Pi_cong) apply (rule_tac b = A in subst_context, fast) done @@ -276,7 +276,7 @@ done lemma AC5_AC4_aux4: "[| R \ A*B; g \ C->R; \x \ C. (\z \ R. fst(z))` (g`x) = x |] - ==> (\x \ C. snd(g`x)): (\x \ C. R``{x})" + ==> (\x \ C. snd(g`x)): (\ x \ C. R``{x})" apply (rule lam_type) apply (force dest: apply_type) done diff -r edd5a2ea3807 -r 0cab06e3bbd0 src/ZF/AC/AC18_AC19.thy --- a/src/ZF/AC/AC18_AC19.thy Wed Aug 27 18:22:34 2003 +0200 +++ b/src/ZF/AC/AC18_AC19.thy Thu Aug 28 01:56:40 2003 +0200 @@ -17,14 +17,14 @@ (* ********************************************************************** *) lemma PROD_subsets: - "[| f \ (\b \ {P(a). a \ A}. b); \a \ A. P(a)<=Q(a) |] - ==> (\a \ A. f`P(a)) \ (\a \ A. Q(a))" + "[| f \ (\ b \ {P(a). a \ A}. b); \a \ A. P(a)<=Q(a) |] + ==> (\a \ A. f`P(a)) \ (\ a \ A. Q(a))" by (rule lam_type, drule apply_type, auto) lemma lemma_AC18: - "[| \A. 0 \ A --> (\f. f \ (\X \ A. X)); A \ 0 |] + "[| \A. 0 \ A --> (\f. f \ (\ X \ A. X)); A \ 0 |] ==> (\a \ A. \b \ B(a). X(a, b)) \ - (\f \ \a \ A. B(a). \a \ A. X(a, f`a))" + (\f \ \ a \ A. B(a). \a \ A. X(a, f`a))" apply (rule subsetI) apply (erule_tac x = "{{b \ B (a) . x \ X (a,b) }. a \ A}" in allE) apply (erule impE, fast) @@ -67,12 +67,12 @@ done lemma lemma1_2: - "[| f`(uu(a)) \ a; f \ (\B \ {uu(a). a \ A}. B); a \ A |] + "[| f`(uu(a)) \ a; f \ (\ B \ {uu(a). a \ A}. B); a \ A |] ==> f`(uu(a))-{0} \ a" apply (unfold uu_def, fast elim!: lemma1_1 dest!: apply_type) done -lemma lemma1: "\f. f \ (\B \ {uu(a). a \ A}. B) ==> \f. f \ (\B \ A. B)" +lemma lemma1: "\f. f \ (\ B \ {uu(a). a \ A}. B) ==> \f. f \ (\ B \ A. B)" apply (erule exE) apply (rule_tac x = "\a\A. if (f` (uu(a)) \ a, f` (uu(a)), f` (uu(a))-{0})" in exI) diff -r edd5a2ea3807 -r 0cab06e3bbd0 src/ZF/AC/AC7_AC9.thy --- a/src/ZF/AC/AC7_AC9.thy Wed Aug 27 18:22:34 2003 +0200 +++ b/src/ZF/AC/AC7_AC9.thy Thu Aug 28 01:56:40 2003 +0200 @@ -52,16 +52,16 @@ (* the proof. *) (* ********************************************************************** *) -lemma lemma1_1: "y \ (\B \ A. Y*B) ==> (\B \ A. snd(y`B)) \ (\B \ A. B)" +lemma lemma1_1: "y \ (\ B \ A. Y*B) ==> (\B \ A. snd(y`B)) \ (\ B \ A. B)" by (fast intro!: lam_type snd_type apply_type) lemma lemma1_2: - "y \ (\B \ {Y*C. C \ A}. B) ==> (\B \ A. y`(Y*B)) \ (\B \ A. Y*B)" + "y \ (\ B \ {Y*C. C \ A}. B) ==> (\B \ A. y`(Y*B)) \ (\ B \ A. Y*B)" apply (fast intro!: lam_type apply_type) done lemma AC7_AC6_lemma1: - "(\B \ {(nat->Union(A))*C. C \ A}. B) \ 0 ==> (\B \ A. B) \ 0" + "(\ B \ {(nat->Union(A))*C. C \ A}. B) \ 0 ==> (\ B \ A. B) \ 0" by (fast intro!: equals0I lemma1_1 lemma1_2) lemma AC7_AC6_lemma2: "0 \ A ==> 0 \ {(nat -> Union(A)) * C. C \ A}" @@ -91,7 +91,7 @@ done lemma AC1_AC8_lemma2: - "[| f \ (\X \ RepFun(A,p). X); D \ A |] ==> (\x \ A. f`p(x))`D \ p(D)" + "[| f \ (\ X \ RepFun(A,p). X); D \ A |] ==> (\x \ A. f`p(x))`D \ p(D)" apply (simp, fast elim!: apply_type) done @@ -151,7 +151,7 @@ "\B1 \ {(F*B)*N. B \ A} Un {cons(0,(F*B)*N). B \ A}. \B2 \ {(F*B)*N. B \ A} Un {cons(0,(F*B)*N). B \ A}. f` \ bij(B1, B2) - ==> (\B \ A. snd(fst((f`)`0))) \ (\X \ A. X)" + ==> (\B \ A. snd(fst((f`)`0))) \ (\ X \ A. X)" apply (intro lam_type snd_type fst_type) apply (rule apply_type [OF _ consI1]) apply (fast intro!: fun_weaken_type bij_is_fun) diff -r edd5a2ea3807 -r 0cab06e3bbd0 src/ZF/AC/AC_Equiv.thy --- a/src/ZF/AC/AC_Equiv.thy Wed Aug 27 18:22:34 2003 +0200 +++ b/src/ZF/AC/AC_Equiv.thy Thu Aug 28 01:56:40 2003 +0200 @@ -41,7 +41,7 @@ "WO7 == \A. Finite(A) <-> (\R. well_ord(A,R) --> well_ord(A,converse(R)))" WO8 :: o - "WO8 == \A. (\f. f \ (\X \ A. X)) --> (\