Extended the notion of letter and digit, such that now one may use greek,
authorskalberg
Thu Aug 28 01:56:40 2003 +0200 (2003-08-28)
changeset 141710cab06e3bbd0
parent 14170 edd5a2ea3807
child 14172 a872d646bf01
Extended the notion of letter and digit, such that now one may use greek,
gothic, euler, or calligraphic letters as normal letters.
NEWS
lib/Tools/fixgreek
lib/scripts/fixgreek.pl
src/HOL/Bali/Decl.thy
src/HOL/Bali/State.thy
src/HOL/Bali/Type.thy
src/HOL/MicroJava/J/TypeRel.thy
src/HOL/NanoJava/TypeRel.thy
src/HOLCF/FOCUS/Buffer.ML
src/HOLCF/FOCUS/Fstream.thy
src/HOLCF/ex/Stream.ML
src/HOLCF/ex/Stream.thy
src/Pure/General/symbol.ML
src/ZF/AC.thy
src/ZF/AC/AC15_WO6.thy
src/ZF/AC/AC17_AC1.thy
src/ZF/AC/AC18_AC19.thy
src/ZF/AC/AC7_AC9.thy
src/ZF/AC/AC_Equiv.thy
src/ZF/AC/HH.thy
src/ZF/Coind/Map.thy
src/ZF/Constructible/AC_in_L.thy
src/ZF/Constructible/Formula.thy
src/ZF/Constructible/L_axioms.thy
src/ZF/Constructible/Normal.thy
src/ZF/Constructible/Reflection.thy
src/ZF/Induct/Brouwer.thy
src/ZF/OrderArith.thy
src/ZF/UNITY/State.thy
src/ZF/Zorn.thy
src/ZF/equalities.thy
src/ZF/ex/Limit.thy
     1.1 --- a/NEWS	Wed Aug 27 18:22:34 2003 +0200
     1.2 +++ b/NEWS	Thu Aug 28 01:56:40 2003 +0200
     1.3 @@ -4,6 +4,20 @@
     1.4  New in this Isabelle release
     1.5  ----------------------------
     1.6  
     1.7 +*** General ***
     1.8 +
     1.9 +* Pure: Greek letters (except small lambda, \<lambda>), as well as gothic
    1.10 +  (\<aa>,...\<zz>,\<AA>,...,\<ZZ>), caligraphic (\<A>...\<Z>), and
    1.11 +  euler (\<a>...\<z>), are now considered normal letters, and can
    1.12 +  therefore be used anywhere where an ASCII letter (a...zA...Z) has
    1.13 +  until now.  Similarily, the symbol digits \<0>...\<9> are now
    1.14 +  considered normal digits.  COMPATIBILITY: This obviously changes the
    1.15 +  parsing of some terms, especially where a symbol has been used as a
    1.16 +  binder, say '\<Pi>x. ...', which is now a type error since \<Pi>x
    1.17 +  will be parsed as an identifier.  Fix it by inserting a space around
    1.18 +  former symbols.  Call 'isatool fixgreek' to try to fix parsing
    1.19 +  errors in existing theory and ML files.
    1.20 +
    1.21  *** HOL ***
    1.22  
    1.23  * 'specification' command added, allowing for definition by
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/lib/Tools/fixgreek	Thu Aug 28 01:56:40 2003 +0200
     2.3 @@ -0,0 +1,42 @@
     2.4 +#!/usr/bin/env bash
     2.5 +#
     2.6 +# $Id$
     2.7 +# Author: Sebastian Skalberg, TU Muenchen
     2.8 +# License: GPL (GNU GENERAL PUBLIC LICENSE)
     2.9 +#
    2.10 +# DESCRIPTION: fix problems with greek and other foreign letters
    2.11 +
    2.12 +
    2.13 +## diagnostics
    2.14 +
    2.15 +PRG="$(basename "$0")"
    2.16 +
    2.17 +function usage()
    2.18 +{
    2.19 +  echo
    2.20 +  echo "Usage: $PRG [FILES|DIRS...]"
    2.21 +  echo
    2.22 +  echo "  Recursively find .thy files, fixing parse problems stemming"
    2.23 +  echo "  from the classification change of greek and other foreign"
    2.24 +  echo "  letters from symbols to letters."
    2.25 +  echo
    2.26 +  echo "  Renames old versions of FILES by appending \"~~\"."
    2.27 +  echo
    2.28 +  exit 1
    2.29 +}
    2.30 +
    2.31 +
    2.32 +## process command line
    2.33 +
    2.34 +[ "$#" -eq 0 -o "$1" = "-?" ] && usage
    2.35 +
    2.36 +SPECS="$@"; shift "$#"
    2.37 +
    2.38 +
    2.39 +## main
    2.40 +
    2.41 +#set by configure
    2.42 +AUTO_PERL=perl
    2.43 +
    2.44 +find $SPECS -name \*.thy -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixgreek.pl"
    2.45 +find $SPECS -name \*.ML -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixgreek.pl"
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/lib/scripts/fixgreek.pl	Thu Aug 28 01:56:40 2003 +0200
     3.3 @@ -0,0 +1,50 @@
     3.4 +#
     3.5 +# $Id$
     3.6 +# Author: Sebastian Skalberg, TU Muenchen
     3.7 +# License: GPL (GNU GENERAL PUBLIC LICENSE)
     3.8 +#
     3.9 +# fixgreek.pl - fix problems with greek and other foreign letters now
    3.10 +#               being classified as letters instead of symbols.
    3.11 +#
    3.12 +
    3.13 +sub fixgreek {
    3.14 +    my ($file) = @_;
    3.15 +
    3.16 +    open (FILE, $file) || die $!;
    3.17 +    undef $/; $text = <FILE>; $/ = "\n";         # slurp whole file
    3.18 +    close FILE || die $!;
    3.19 +
    3.20 +    $_ = $text;
    3.21 +
    3.22 +    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;
    3.23 +
    3.24 +    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;
    3.25 +
    3.26 +    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;
    3.27 +
    3.28 +    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;
    3.29 +
    3.30 +    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;
    3.31 +
    3.32 +    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;
    3.33 +
    3.34 +    $result = $_;
    3.35 +
    3.36 +    if ($text ne $result) {
    3.37 +	print STDERR "fixing $file\n";
    3.38 +        if (! -f "$file~~") {
    3.39 +	    rename $file, "$file~~" || die $!;
    3.40 +        }
    3.41 +	open (FILE, "> $file") || die $!;
    3.42 +	print FILE $result;
    3.43 +	close FILE || die $!;
    3.44 +    }
    3.45 +}
    3.46 +
    3.47 +
    3.48 +## main
    3.49 +
    3.50 +foreach $file (@ARGV) {
    3.51 +  eval { &fixgreek($file); };
    3.52 +  if ($@) { print STDERR "*** fixgreek $file: ", $@, "\n"; }
    3.53 +}
     4.1 --- a/src/HOL/Bali/Decl.thy	Wed Aug 27 18:22:34 2003 +0200
     4.2 +++ b/src/HOL/Bali/Decl.thy	Thu Aug 28 01:56:40 2003 +0200
     4.3 @@ -491,7 +491,7 @@
     4.4  done
     4.5  
     4.6  lemma subcls1_def2: 
     4.7 - "subcls1 G = (\<Sigma>C\<in>{C. is_class G C}. {D. C\<noteq>Object \<and> super (the(class G C))=D})"
     4.8 + "subcls1 G = (\<Sigma> C\<in>{C. is_class G C}. {D. C\<noteq>Object \<and> super (the(class G C))=D})"
     4.9  apply (unfold subcls1_def)
    4.10  apply auto
    4.11  done
     5.1 --- a/src/HOL/Bali/State.thy	Wed Aug 27 18:22:34 2003 +0200
     5.2 +++ b/src/HOL/Bali/State.thy	Thu Aug 28 01:56:40 2003 +0200
     5.3 @@ -266,7 +266,7 @@
     5.4  
     5.5  constdefs
     5.6    new_Addr     :: "heap \<Rightarrow> loc option"
     5.7 - "new_Addr h   \<equiv> if (\<forall>a. h a \<noteq> None) then None else Some (\<epsilon>a. h a = None)"
     5.8 + "new_Addr h   \<equiv> if (\<forall>a. h a \<noteq> None) then None else Some (\<epsilon> a. h a = None)"
     5.9  
    5.10  lemma new_AddrD: "new_Addr h = Some a \<Longrightarrow> h a = None"
    5.11  apply (unfold new_Addr_def)
     6.1 --- a/src/HOL/Bali/Type.thy	Wed Aug 27 18:22:34 2003 +0200
     6.2 +++ b/src/HOL/Bali/Type.thy	Thu Aug 28 01:56:40 2003 +0200
     6.3 @@ -51,7 +51,7 @@
     6.4  
     6.5  constdefs
     6.6    the_Class :: "ty \<Rightarrow> qtname"
     6.7 - "the_Class T \<equiv> \<epsilon>C. T = Class C" (** primrec not possible here **)
     6.8 + "the_Class T \<equiv> \<epsilon> C. T = Class C" (** primrec not possible here **)
     6.9   
    6.10  lemma the_Class_eq [simp]: "the_Class (Class C)= C"
    6.11  by (auto simp add: the_Class_def)
     7.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Wed Aug 27 18:22:34 2003 +0200
     7.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Thu Aug 28 01:56:40 2003 +0200
     7.3 @@ -42,7 +42,7 @@
     7.4  done
     7.5  
     7.6  lemma subcls1_def2: 
     7.7 -"subcls1 G = (\<Sigma>C\<in>{C. is_class G C} . {D. C\<noteq>Object \<and> fst (the (class G C))=D})"
     7.8 +"subcls1 G = (\<Sigma> C\<in>{C. is_class G C} . {D. C\<noteq>Object \<and> fst (the (class G C))=D})"
     7.9    by (auto simp add: is_class_def dest: subcls1D intro: subcls1I)
    7.10  
    7.11  lemma finite_subcls1: "finite (subcls1 G)"
     8.1 --- a/src/HOL/NanoJava/TypeRel.thy	Wed Aug 27 18:22:34 2003 +0200
     8.2 +++ b/src/HOL/NanoJava/TypeRel.thy	Thu Aug 28 01:56:40 2003 +0200
     8.3 @@ -55,7 +55,7 @@
     8.4  done
     8.5  
     8.6  lemma subcls1_def2: 
     8.7 -"subcls1 = (\<Sigma>C\<in>{C. is_class C} . {D. C\<noteq>Object \<and> super (the (class C)) = D})"
     8.8 +"subcls1 = (\<Sigma> C\<in>{C. is_class C} . {D. C\<noteq>Object \<and> super (the (class C)) = D})"
     8.9  apply (unfold subcls1_def is_class_def)
    8.10  apply auto
    8.11  done
     9.1 --- a/src/HOLCF/FOCUS/Buffer.ML	Wed Aug 27 18:22:34 2003 +0200
     9.2 +++ b/src/HOLCF/FOCUS/Buffer.ML	Thu Aug 28 01:56:40 2003 +0200
     9.3 @@ -247,7 +247,7 @@
     9.4  Goalw [BufSt_def, BufSt_P_def] "BufEq <= BufSt";
     9.5  by Safe_tac;
     9.6  by (EVERY'[rename_tac "f", res_inst_tac 
     9.7 -        [("x","\\<lambda>s. case s of Sd d => \\<Lambda>x. f\\<cdot>(Md d\\<leadsto>x)| \\<currency> => f")] bexI] 1);
     9.8 +        [("x","\\<lambda>s. case s of Sd d => \\<Lambda> x. f\\<cdot>(Md d\\<leadsto>x)| \\<currency> => f")] bexI] 1);
     9.9  by ( Simp_tac 1);
    9.10  by (etac weak_coinduct_image 1);
    9.11  by (rewtac BufSt_F_def); 
    10.1 --- a/src/HOLCF/FOCUS/Fstream.thy	Wed Aug 27 18:22:34 2003 +0200
    10.2 +++ b/src/HOLCF/FOCUS/Fstream.thy	Thu Aug 28 01:56:40 2003 +0200
    10.3 @@ -39,7 +39,7 @@
    10.4  
    10.5  defs
    10.6  
    10.7 -  fscons_def	"fscons a   \\<equiv> \\<Lambda>s. Def a && s"
    10.8 +  fscons_def	"fscons a   \\<equiv> \\<Lambda> s. Def a && s"
    10.9    fsfilter_def  "fsfilter A \\<equiv> sfilter\\<cdot>(flift2 (\\<lambda>x. x\\<in>A))"
   10.10  
   10.11  end
    11.1 --- a/src/HOLCF/ex/Stream.ML	Wed Aug 27 18:22:34 2003 +0200
    11.2 +++ b/src/HOLCF/ex/Stream.ML	Thu Aug 28 01:56:40 2003 +0200
    11.3 @@ -358,7 +358,7 @@
    11.4  section "smap";
    11.5  
    11.6  bind_thm ("smap_unfold", fix_prover2 thy smap_def 
    11.7 -	"smap = (\\<Lambda>f s. case s of x && l => f\\<cdot>x && smap\\<cdot>f\\<cdot>l)");
    11.8 +	"smap = (\\<Lambda> f s. case s of x && l => f\\<cdot>x && smap\\<cdot>f\\<cdot>l)");
    11.9  
   11.10  Goal "smap\\<cdot>f\\<cdot>\\<bottom> = \\<bottom>";
   11.11  by (stac smap_unfold 1);
   11.12 @@ -570,7 +570,7 @@
   11.13  section "sfilter";
   11.14  
   11.15  bind_thm ("sfilter_unfold", fix_prover2 thy sfilter_def 
   11.16 -	"sfilter = (\\<Lambda>p s. case s of x && xs => \
   11.17 +	"sfilter = (\\<Lambda> p s. case s of x && xs => \
   11.18  \  If p\\<cdot>x then x && sfilter\\<cdot>p\\<cdot>xs else sfilter\\<cdot>p\\<cdot>xs fi)");
   11.19  
   11.20  Goal "sfilter\\<cdot>\\<bottom> = \\<bottom>";
    12.1 --- a/src/HOLCF/ex/Stream.thy	Wed Aug 27 18:22:34 2003 +0200
    12.2 +++ b/src/HOLCF/ex/Stream.thy	Thu Aug 28 01:56:40 2003 +0200
    12.3 @@ -18,8 +18,8 @@
    12.4  
    12.5  defs
    12.6  
    12.7 -  smap_def	"smap	 == fix\\<cdot>(\\<Lambda>h f s. case s of x && xs => f\\<cdot>x && h\\<cdot>f\\<cdot>xs)"
    12.8 -  sfilter_def	"sfilter == fix\\<cdot>(\\<Lambda>h p s. case s of x && xs => 
    12.9 +  smap_def	"smap	 == fix\\<cdot>(\\<Lambda> h f s. case s of x && xs => f\\<cdot>x && h\\<cdot>f\\<cdot>xs)"
   12.10 +  sfilter_def	"sfilter == fix\\<cdot>(\\<Lambda> h p s. case s of x && xs => 
   12.11  				     If p\\<cdot>x then x && h\\<cdot>p\\<cdot>xs else h\\<cdot>p\\<cdot>xs fi)"
   12.12    slen_def	"#s == if stream_finite s 
   12.13  		      then Fin (LEAST n. stream_take n\\<cdot>s = s) else \\<infinity>"
    13.1 --- a/src/Pure/General/symbol.ML	Wed Aug 27 18:22:34 2003 +0200
    13.2 +++ b/src/Pure/General/symbol.ML	Thu Aug 28 01:56:40 2003 +0200
    13.3 @@ -85,13 +85,57 @@
    13.4  
    13.5  fun is_ascii s = size s = 1 andalso ord s < 128;
    13.6  
    13.7 +local
    13.8 +    fun wrap s = "\\<" ^ s ^ ">"
    13.9 +    val pre_digits =
   13.10 +	["zero","one","two","three","four",
   13.11 +	 "five","six","seven","eight","nine"]
   13.12 +
   13.13 +    val cal_letters =
   13.14 +	["A","B","C","D","E","F","G","H","I","J","K","L","M",
   13.15 +	 "N","O","P","Q","R","S","T","U","V","W","X","Y","Z"]
   13.16 +
   13.17 +    val small_letters =
   13.18 +	["a","b","c","d","e","f","g","h","i","j","k","l","m",
   13.19 +	 "n","o","p","q","r","s","t","u","v","w","x","y","z"]
   13.20 +
   13.21 +    val goth_letters =
   13.22 +	["AA","BB","CC","DD","EE","FF","GG","HH","II","JJ","KK","LL","MM",
   13.23 +	 "NN","OO","PP","QQ","RR","SS","TT","UU","VV","WW","XX","YY","ZZ",
   13.24 +	 "aa","bb","cc","dd","ee","ff","gg","hh","ii","jj","kk","ll","mm",
   13.25 +	 "nn","oo","pp","qq","rr","ss","tt","uu","vv","ww","xx","yy","zz"]
   13.26 +
   13.27 +    val greek_letters =
   13.28 +	["alpha","beta","gamma","delta","epsilon","zeta","eta","theta",
   13.29 +	 "iota","kappa",(*"lambda",*)"mu","nu","xi","pi","rho","sigma","tau",
   13.30 +	 "upsilon","phi","psi","omega","Gamma","Delta","Theta","Lambda",
   13.31 +	 "Xi","Pi","Sigma","Upsilon","Phi","Psi","Omega"]
   13.32 +
   13.33 +    val bbb_letters = ["bool","complex","nat","rat","real","int"]
   13.34 +
   13.35 +    val pre_letters =
   13.36 +	cal_letters   @
   13.37 +	small_letters @
   13.38 +	goth_letters  @
   13.39 +	greek_letters
   13.40 +in
   13.41 +val ext_digits  = map wrap pre_digits
   13.42 +val ext_letters = map wrap pre_letters
   13.43 +val ext_letdigs = ext_digits @ ext_letters
   13.44 +fun is_ext_digit  s = String.isPrefix "\\<" s andalso s mem ext_digits
   13.45 +fun is_ext_letter s = String.isPrefix "\\<" s andalso s mem ext_letters
   13.46 +fun is_ext_letdig s = String.isPrefix "\\<" s andalso s mem ext_letdigs
   13.47 +end
   13.48 +     
   13.49  fun is_letter s =
   13.50 -  size s = 1 andalso
   13.51 -   (ord "A" <= ord s andalso ord s <= ord "Z" orelse
   13.52 -    ord "a" <= ord s andalso ord s <= ord "z");
   13.53 +    (size s = 1 andalso
   13.54 +     (ord "A" <= ord s andalso ord s <= ord "Z" orelse
   13.55 +      ord "a" <= ord s andalso ord s <= ord "z"))
   13.56 +    orelse is_ext_letter s
   13.57  
   13.58  fun is_digit s =
   13.59 -  size s = 1 andalso ord "0" <= ord s andalso ord s <= ord "9";
   13.60 +    (size s = 1 andalso ord "0" <= ord s andalso ord s <= ord "9")
   13.61 +    orelse is_ext_digit s
   13.62  
   13.63  fun is_quasi "_" = true
   13.64    | is_quasi "'" = true
   13.65 @@ -107,10 +151,12 @@
   13.66  fun is_letdig s = is_quasi_letter s orelse is_digit s;
   13.67  
   13.68  fun is_symbolic s =
   13.69 -  size s > 2 andalso nth_elem_string (2, s) <> "^";
   13.70 +  size s > 2 andalso nth_elem_string (2, s) <> "^"
   13.71 +  andalso not (is_ext_letdig s);
   13.72  
   13.73  fun is_printable s =
   13.74    size s = 1 andalso ord space <= ord s andalso ord s <= ord "~" orelse
   13.75 +  is_ext_letdig s orelse
   13.76    is_symbolic s;
   13.77  
   13.78  fun is_identifier s =
    14.1 --- a/src/ZF/AC.thy	Wed Aug 27 18:22:34 2003 +0200
    14.2 +++ b/src/ZF/AC.thy	Thu Aug 28 01:56:40 2003 +0200
    14.3 @@ -26,7 +26,7 @@
    14.4  apply (erule bspec, assumption)
    14.5  done
    14.6  
    14.7 -lemma AC_Pi_Pow: "\<exists>f. f \<in> (\<Pi>X \<in> Pow(C)-{0}. X)"
    14.8 +lemma AC_Pi_Pow: "\<exists>f. f \<in> (\<Pi> X \<in> Pow(C)-{0}. X)"
    14.9  apply (rule_tac B1 = "%x. x" in AC_Pi [THEN exE])
   14.10  apply (erule_tac [2] exI, blast)
   14.11  done
   14.12 @@ -52,7 +52,7 @@
   14.13  apply (erule_tac [2] fun_weaken_type, blast+)
   14.14  done
   14.15  
   14.16 -lemma AC_Pi0: "0 \<notin> A ==> \<exists>f. f \<in> (\<Pi>x \<in> A. x)"
   14.17 +lemma AC_Pi0: "0 \<notin> A ==> \<exists>f. f \<in> (\<Pi> x \<in> A. x)"
   14.18  apply (rule AC_Pi)
   14.19  apply (simp_all add: non_empty_family) 
   14.20  done
    15.1 --- a/src/ZF/AC/AC15_WO6.thy	Wed Aug 27 18:22:34 2003 +0200
    15.2 +++ b/src/ZF/AC/AC15_WO6.thy	Thu Aug 28 01:56:40 2003 +0200
    15.3 @@ -262,7 +262,7 @@
    15.4  
    15.5  lemma AC13_AC1_lemma:
    15.6       "\<forall>B \<in> A. f(B)\<noteq>0 & f(B)<=B & f(B) \<lesssim> 1   
    15.7 -      ==> (\<lambda>x \<in> A. THE y. f(x)={y}) \<in> (\<Pi>X \<in> A. X)"
    15.8 +      ==> (\<lambda>x \<in> A. THE y. f(x)={y}) \<in> (\<Pi> X \<in> A. X)"
    15.9  apply (rule lam_type)
   15.10  apply (drule bspec, assumption)
   15.11  apply (elim conjE)
    16.1 --- a/src/ZF/AC/AC17_AC1.thy	Wed Aug 27 18:22:34 2003 +0200
    16.2 +++ b/src/ZF/AC/AC17_AC1.thy	Thu Aug 28 01:56:40 2003 +0200
    16.3 @@ -14,7 +14,7 @@
    16.4  (** AC0 is equivalent to AC1.  
    16.5      AC0 comes from Suppes, AC1 from Rubin & Rubin **)
    16.6  
    16.7 -lemma AC0_AC1_lemma: "[| f:(\<Pi>X \<in> A. X); D \<subseteq> A |] ==> \<exists>g. g:(\<Pi>X \<in> D. X)"
    16.8 +lemma AC0_AC1_lemma: "[| f:(\<Pi> X \<in> A. X); D \<subseteq> A |] ==> \<exists>g. g:(\<Pi> X \<in> D. X)"
    16.9  by (fast intro!: lam_type apply_type)
   16.10  
   16.11  lemma AC0_AC1: "AC0 ==> AC1"
   16.12 @@ -28,7 +28,7 @@
   16.13  
   16.14  (**** The proof of AC1 ==> AC17 ****)
   16.15  
   16.16 -lemma AC1_AC17_lemma: "f \<in> (\<Pi>X \<in> Pow(A) - {0}. X) ==> f \<in> (Pow(A) - {0} -> A)"
   16.17 +lemma AC1_AC17_lemma: "f \<in> (\<Pi> X \<in> Pow(A) - {0}. X) ==> f \<in> (Pow(A) - {0} -> A)"
   16.18  apply (rule Pi_type, assumption)
   16.19  apply (drule apply_type, assumption, fast)
   16.20  done
   16.21 @@ -143,7 +143,7 @@
   16.22  (* ********************************************************************** *)
   16.23  
   16.24  lemma AC1_AC2_aux1:
   16.25 -     "[| f:(\<Pi>X \<in> A. X);  B \<in> A;  0\<notin>A |] ==> {f`B} \<subseteq> B Int {f`C. C \<in> A}"
   16.26 +     "[| f:(\<Pi> X \<in> A. X);  B \<in> A;  0\<notin>A |] ==> {f`B} \<subseteq> B Int {f`C. C \<in> A}"
   16.27  by (fast elim!: apply_type)
   16.28  
   16.29  lemma AC1_AC2_aux2: 
   16.30 @@ -177,7 +177,7 @@
   16.31  
   16.32  lemma AC2_AC1_aux3:
   16.33       "\<forall>D \<in> {E*{E}. E \<in> A}. \<exists>y. D Int C = {y}   
   16.34 -      ==> (\<lambda>x \<in> A. fst(THE z. (x*{x} Int C = {z}))) \<in> (\<Pi>X \<in> A. X)"
   16.35 +      ==> (\<lambda>x \<in> A. fst(THE z. (x*{x} Int C = {z}))) \<in> (\<Pi> X \<in> A. X)"
   16.36  apply (rule lam_type)
   16.37  apply (drule bspec, blast)
   16.38  apply (blast intro: AC2_AC1_aux2 fst_type)
   16.39 @@ -233,7 +233,7 @@
   16.40  (* ********************************************************************** *)
   16.41  
   16.42  lemma AC3_AC1_lemma:
   16.43 -     "b\<notin>A ==> (\<Pi>x \<in> {a \<in> A. id(A)`a\<noteq>b}. id(A)`x) = (\<Pi>x \<in> A. x)"
   16.44 +     "b\<notin>A ==> (\<Pi> x \<in> {a \<in> A. id(A)`a\<noteq>b}. id(A)`x) = (\<Pi> x \<in> A. x)"
   16.45  apply (simp add: id_def cong add: Pi_cong)
   16.46  apply (rule_tac b = A in subst_context, fast)
   16.47  done
   16.48 @@ -276,7 +276,7 @@
   16.49  done
   16.50  
   16.51  lemma AC5_AC4_aux4: "[| R \<subseteq> A*B; g \<in> C->R; \<forall>x \<in> C. (\<lambda>z \<in> R. fst(z))` (g`x) = x |]  
   16.52 -                ==> (\<lambda>x \<in> C. snd(g`x)): (\<Pi>x \<in> C. R``{x})"
   16.53 +                ==> (\<lambda>x \<in> C. snd(g`x)): (\<Pi> x \<in> C. R``{x})"
   16.54  apply (rule lam_type)
   16.55  apply (force dest: apply_type)
   16.56  done
    17.1 --- a/src/ZF/AC/AC18_AC19.thy	Wed Aug 27 18:22:34 2003 +0200
    17.2 +++ b/src/ZF/AC/AC18_AC19.thy	Thu Aug 28 01:56:40 2003 +0200
    17.3 @@ -17,14 +17,14 @@
    17.4  (* ********************************************************************** *)
    17.5  
    17.6  lemma PROD_subsets:
    17.7 -     "[| f \<in> (\<Pi>b \<in> {P(a). a \<in> A}. b);  \<forall>a \<in> A. P(a)<=Q(a) |]   
    17.8 -      ==> (\<lambda>a \<in> A. f`P(a)) \<in> (\<Pi>a \<in> A. Q(a))"
    17.9 +     "[| f \<in> (\<Pi> b \<in> {P(a). a \<in> A}. b);  \<forall>a \<in> A. P(a)<=Q(a) |]   
   17.10 +      ==> (\<lambda>a \<in> A. f`P(a)) \<in> (\<Pi> a \<in> A. Q(a))"
   17.11  by (rule lam_type, drule apply_type, auto)
   17.12  
   17.13  lemma lemma_AC18:
   17.14 -     "[| \<forall>A. 0 \<notin> A --> (\<exists>f. f \<in> (\<Pi>X \<in> A. X)); A \<noteq> 0 |] 
   17.15 +     "[| \<forall>A. 0 \<notin> A --> (\<exists>f. f \<in> (\<Pi> X \<in> A. X)); A \<noteq> 0 |] 
   17.16        ==> (\<Inter>a \<in> A. \<Union>b \<in> B(a). X(a, b)) \<subseteq> 
   17.17 -          (\<Union>f \<in> \<Pi>a \<in> A. B(a). \<Inter>a \<in> A. X(a, f`a))"
   17.18 +          (\<Union>f \<in> \<Pi> a \<in> A. B(a). \<Inter>a \<in> A. X(a, f`a))"
   17.19  apply (rule subsetI)
   17.20  apply (erule_tac x = "{{b \<in> B (a) . x \<in> X (a,b) }. a \<in> A}" in allE)
   17.21  apply (erule impE, fast)
   17.22 @@ -67,12 +67,12 @@
   17.23  done
   17.24  
   17.25  lemma lemma1_2: 
   17.26 -        "[| f`(uu(a)) \<notin> a; f \<in> (\<Pi>B \<in> {uu(a). a \<in> A}. B); a \<in> A |]   
   17.27 +        "[| f`(uu(a)) \<notin> a; f \<in> (\<Pi> B \<in> {uu(a). a \<in> A}. B); a \<in> A |]   
   17.28                  ==> f`(uu(a))-{0} \<in> a"
   17.29  apply (unfold uu_def, fast elim!: lemma1_1 dest!: apply_type)
   17.30  done
   17.31  
   17.32 -lemma lemma1: "\<exists>f. f \<in> (\<Pi>B \<in> {uu(a). a \<in> A}. B) ==> \<exists>f. f \<in> (\<Pi>B \<in> A. B)"
   17.33 +lemma lemma1: "\<exists>f. f \<in> (\<Pi> B \<in> {uu(a). a \<in> A}. B) ==> \<exists>f. f \<in> (\<Pi> B \<in> A. B)"
   17.34  apply (erule exE)
   17.35  apply (rule_tac x = "\<lambda>a\<in>A. if (f` (uu(a)) \<in> a, f` (uu(a)), f` (uu(a))-{0})" 
   17.36         in exI)
    18.1 --- a/src/ZF/AC/AC7_AC9.thy	Wed Aug 27 18:22:34 2003 +0200
    18.2 +++ b/src/ZF/AC/AC7_AC9.thy	Thu Aug 28 01:56:40 2003 +0200
    18.3 @@ -52,16 +52,16 @@
    18.4  (* the proof.                                                             *)
    18.5  (* ********************************************************************** *)
    18.6  
    18.7 -lemma lemma1_1: "y \<in> (\<Pi>B \<in> A. Y*B) ==> (\<lambda>B \<in> A. snd(y`B)) \<in> (\<Pi>B \<in> A. B)"
    18.8 +lemma lemma1_1: "y \<in> (\<Pi> B \<in> A. Y*B) ==> (\<lambda>B \<in> A. snd(y`B)) \<in> (\<Pi> B \<in> A. B)"
    18.9  by (fast intro!: lam_type snd_type apply_type)
   18.10  
   18.11  lemma lemma1_2:
   18.12 -     "y \<in> (\<Pi>B \<in> {Y*C. C \<in> A}. B) ==> (\<lambda>B \<in> A. y`(Y*B)) \<in> (\<Pi>B \<in> A. Y*B)"
   18.13 +     "y \<in> (\<Pi> B \<in> {Y*C. C \<in> A}. B) ==> (\<lambda>B \<in> A. y`(Y*B)) \<in> (\<Pi> B \<in> A. Y*B)"
   18.14  apply (fast intro!: lam_type apply_type)
   18.15  done
   18.16  
   18.17  lemma AC7_AC6_lemma1:
   18.18 -     "(\<Pi>B \<in> {(nat->Union(A))*C. C \<in> A}. B) \<noteq> 0 ==> (\<Pi>B \<in> A. B) \<noteq> 0"
   18.19 +     "(\<Pi> B \<in> {(nat->Union(A))*C. C \<in> A}. B) \<noteq> 0 ==> (\<Pi> B \<in> A. B) \<noteq> 0"
   18.20  by (fast intro!: equals0I lemma1_1 lemma1_2)
   18.21  
   18.22  lemma AC7_AC6_lemma2: "0 \<notin> A ==> 0 \<notin> {(nat -> Union(A)) * C. C \<in> A}"
   18.23 @@ -91,7 +91,7 @@
   18.24  done
   18.25  
   18.26  lemma AC1_AC8_lemma2:
   18.27 -     "[| f \<in> (\<Pi>X \<in> RepFun(A,p). X); D \<in> A |] ==> (\<lambda>x \<in> A. f`p(x))`D \<in> p(D)" 
   18.28 +     "[| f \<in> (\<Pi> X \<in> RepFun(A,p). X); D \<in> A |] ==> (\<lambda>x \<in> A. f`p(x))`D \<in> p(D)" 
   18.29  apply (simp, fast elim!: apply_type)
   18.30  done
   18.31  
   18.32 @@ -151,7 +151,7 @@
   18.33       "\<forall>B1 \<in> {(F*B)*N. B \<in> A} Un {cons(0,(F*B)*N). B \<in> A}.   
   18.34        \<forall>B2 \<in> {(F*B)*N. B \<in> A} Un {cons(0,(F*B)*N). B \<in> A}.   
   18.35          f`<B1,B2> \<in> bij(B1, B2)   
   18.36 -      ==> (\<lambda>B \<in> A. snd(fst((f`<cons(0,(F*B)*N),(F*B)*N>)`0))) \<in> (\<Pi>X \<in> A. X)"
   18.37 +      ==> (\<lambda>B \<in> A. snd(fst((f`<cons(0,(F*B)*N),(F*B)*N>)`0))) \<in> (\<Pi> X \<in> A. X)"
   18.38  apply (intro lam_type snd_type fst_type)
   18.39  apply (rule apply_type [OF _ consI1]) 
   18.40  apply (fast intro!: fun_weaken_type bij_is_fun)
    19.1 --- a/src/ZF/AC/AC_Equiv.thy	Wed Aug 27 18:22:34 2003 +0200
    19.2 +++ b/src/ZF/AC/AC_Equiv.thy	Thu Aug 28 01:56:40 2003 +0200
    19.3 @@ -41,7 +41,7 @@
    19.4      "WO7 == \<forall>A. Finite(A) <-> (\<forall>R. well_ord(A,R) --> well_ord(A,converse(R)))"
    19.5  
    19.6    WO8 :: o
    19.7 -    "WO8 == \<forall>A. (\<exists>f. f \<in> (\<Pi>X \<in> A. X)) --> (\<exists>R. well_ord(A,R))"
    19.8 +    "WO8 == \<forall>A. (\<exists>f. f \<in> (\<Pi> X \<in> A. X)) --> (\<exists>R. well_ord(A,R))"
    19.9  
   19.10  
   19.11  (* Auxiliary concepts needed below *)
   19.12 @@ -54,28 +54,28 @@
   19.13  
   19.14  (* Axioms of Choice *)  
   19.15    AC0 :: o
   19.16 -    "AC0 == \<forall>A. \<exists>f. f \<in> (\<Pi>X \<in> Pow(A)-{0}. X)"
   19.17 +    "AC0 == \<forall>A. \<exists>f. f \<in> (\<Pi> X \<in> Pow(A)-{0}. X)"
   19.18  
   19.19    AC1 :: o
   19.20 -    "AC1 == \<forall>A. 0\<notin>A --> (\<exists>f. f \<in> (\<Pi>X \<in> A. X))"
   19.21 +    "AC1 == \<forall>A. 0\<notin>A --> (\<exists>f. f \<in> (\<Pi> X \<in> A. X))"
   19.22  
   19.23    AC2 :: o
   19.24      "AC2 == \<forall>A. 0\<notin>A & pairwise_disjoint(A)   
   19.25  		   --> (\<exists>C. \<forall>B \<in> A. \<exists>y. B Int C = {y})"
   19.26    AC3 :: o
   19.27 -    "AC3 == \<forall>A B. \<forall>f \<in> A->B. \<exists>g. g \<in> (\<Pi>x \<in> {a \<in> A. f`a\<noteq>0}. f`x)"
   19.28 +    "AC3 == \<forall>A B. \<forall>f \<in> A->B. \<exists>g. g \<in> (\<Pi> x \<in> {a \<in> A. f`a\<noteq>0}. f`x)"
   19.29  
   19.30    AC4 :: o
   19.31 -    "AC4 == \<forall>R A B. (R \<subseteq> A*B --> (\<exists>f. f \<in> (\<Pi>x \<in> domain(R). R``{x})))"
   19.32 +    "AC4 == \<forall>R A B. (R \<subseteq> A*B --> (\<exists>f. f \<in> (\<Pi> x \<in> domain(R). R``{x})))"
   19.33  
   19.34    AC5 :: o
   19.35      "AC5 == \<forall>A B. \<forall>f \<in> A->B. \<exists>g \<in> range(f)->A. \<forall>x \<in> domain(g). f`(g`x) = x"
   19.36  
   19.37    AC6 :: o
   19.38 -    "AC6 == \<forall>A. 0\<notin>A --> (\<Pi>B \<in> A. B)\<noteq>0"
   19.39 +    "AC6 == \<forall>A. 0\<notin>A --> (\<Pi> B \<in> A. B)\<noteq>0"
   19.40  
   19.41    AC7 :: o
   19.42 -    "AC7 == \<forall>A. 0\<notin>A & (\<forall>B1 \<in> A. \<forall>B2 \<in> A. B1\<approx>B2) --> (\<Pi>B \<in> A. B) \<noteq> 0"
   19.43 +    "AC7 == \<forall>A. 0\<notin>A & (\<forall>B1 \<in> A. \<forall>B2 \<in> A. B1\<approx>B2) --> (\<Pi> B \<in> A. B) \<noteq> 0"
   19.44  
   19.45    AC8 :: o
   19.46      "AC8 == \<forall>A. (\<forall>B \<in> A. \<exists>B1 B2. B=<B1,B2> & B1\<approx>B2)   
   19.47 @@ -121,13 +121,13 @@
   19.48  locale AC18 =
   19.49    assumes AC18: "A\<noteq>0 & (\<forall>a \<in> A. B(a) \<noteq> 0) -->
   19.50      ((\<Inter>a \<in> A. \<Union>b \<in> B(a). X(a,b)) =   
   19.51 -      (\<Union>f \<in> \<Pi>a \<in> A. B(a). \<Inter>a \<in> A. X(a, f`a)))"
   19.52 +      (\<Union>f \<in> \<Pi> a \<in> A. B(a). \<Inter>a \<in> A. X(a, f`a)))"
   19.53    --"AC18 cannot be expressed within the object-logic"
   19.54  
   19.55  constdefs
   19.56    AC19 :: o
   19.57      "AC19 == \<forall>A. A\<noteq>0 & 0\<notin>A --> ((\<Inter>a \<in> A. \<Union>b \<in> a. b) =   
   19.58 -		   (\<Union>f \<in> (\<Pi>B \<in> A. B). \<Inter>a \<in> A. f`a))"
   19.59 +		   (\<Union>f \<in> (\<Pi> B \<in> A. B). \<Inter>a \<in> A. f`a))"
   19.60  
   19.61  
   19.62  
   19.63 @@ -194,10 +194,10 @@
   19.64  by (blast dest!: well_ord_imp_ex1_first
   19.65                      [THEN theI, THEN first_def [THEN def_imp_iff, THEN iffD1]])
   19.66  
   19.67 -lemma ex_choice_fun: "[| well_ord(Union(A), R); 0\<notin>A |] ==> \<exists>f. f:(\<Pi>X \<in> A. X)"
   19.68 +lemma ex_choice_fun: "[| well_ord(Union(A), R); 0\<notin>A |] ==> \<exists>f. f:(\<Pi> X \<in> A. X)"
   19.69  by (fast elim!: first_in_B intro!: lam_type)
   19.70  
   19.71 -lemma ex_choice_fun_Pow: "well_ord(A, R) ==> \<exists>f. f:(\<Pi>X \<in> Pow(A)-{0}. X)"
   19.72 +lemma ex_choice_fun_Pow: "well_ord(A, R) ==> \<exists>f. f:(\<Pi> X \<in> Pow(A)-{0}. X)"
   19.73  by (fast elim!: well_ord_subset [THEN ex_choice_fun])
   19.74  
   19.75  
    20.1 --- a/src/ZF/AC/HH.thy	Wed Aug 27 18:22:34 2003 +0200
    20.2 +++ b/src/ZF/AC/HH.thy	Thu Aug 28 01:56:40 2003 +0200
    20.3 @@ -208,8 +208,8 @@
    20.4  done
    20.5  
    20.6  lemma lam_singI:
    20.7 -     "f \<in> (\<Pi>X \<in> Pow(x)-{0}. F(X))   
    20.8 -      ==> (\<lambda>X \<in> Pow(x)-{0}. {f`X}) \<in> (\<Pi>X \<in> Pow(x)-{0}. {{z}. z \<in> F(X)})"
    20.9 +     "f \<in> (\<Pi> X \<in> Pow(x)-{0}. F(X))   
   20.10 +      ==> (\<lambda>X \<in> Pow(x)-{0}. {f`X}) \<in> (\<Pi> X \<in> Pow(x)-{0}. {{z}. z \<in> F(X)})"
   20.11  by (fast del: DiffI DiffE
   20.12  	    intro!: lam_type singleton_eq_iff [THEN iffD2] dest: apply_type)
   20.13  
   20.14 @@ -233,7 +233,7 @@
   20.15  Perhaps it could be simplified. *)
   20.16  
   20.17  lemma bijection:
   20.18 -     "f \<in> (\<Pi>X \<in> Pow(x) - {0}. X) 
   20.19 +     "f \<in> (\<Pi> X \<in> Pow(x) - {0}. X) 
   20.20        ==> \<exists>g. g \<in> bij(x, LEAST i. HH(\<lambda>X \<in> Pow(x)-{0}. {f`X}, x, i) = {x})"
   20.21  apply (rule exI) 
   20.22  apply (rule bij_Least_HH_x [THEN bij_converse_bij])
    21.1 --- a/src/ZF/Coind/Map.thy	Wed Aug 27 18:22:34 2003 +0200
    21.2 +++ b/src/ZF/Coind/Map.thy	Thu Aug 28 01:56:40 2003 +0200
    21.3 @@ -23,7 +23,7 @@
    21.4     "map_emp == 0"
    21.5  
    21.6    map_owr :: "[i,i,i]=>i"
    21.7 -   "map_owr(m,a,b) == \<Sigma>x \<in> {a} Un domain(m). if x=a then b else m``{x}"
    21.8 +   "map_owr(m,a,b) == \<Sigma> x \<in> {a} Un domain(m). if x=a then b else m``{x}"
    21.9  
   21.10    map_app :: "[i,i]=>i"
   21.11     "map_app(m,a) == m``{a}"
    22.1 --- a/src/ZF/Constructible/AC_in_L.thy	Wed Aug 27 18:22:34 2003 +0200
    22.2 +++ b/src/ZF/Constructible/AC_in_L.thy	Thu Aug 28 01:56:40 2003 +0200
    22.3 @@ -244,7 +244,7 @@
    22.4  
    22.5    DPow_least :: "[i,i,i,i]=>i"
    22.6      --{*function yielding the smallest index for @{term X}*}
    22.7 -   "DPow_least(f,r,A,X) == \<mu>k. DPow_ord(f,r,A,X,k)"
    22.8 +   "DPow_least(f,r,A,X) == \<mu> k. DPow_ord(f,r,A,X,k)"
    22.9  
   22.10    DPow_r :: "[i,i,i]=>i"
   22.11      --{*a wellordering on @{term "DPow(A)"}*}
    23.1 --- a/src/ZF/Constructible/Formula.thy	Wed Aug 27 18:22:34 2003 +0200
    23.2 +++ b/src/ZF/Constructible/Formula.thy	Thu Aug 28 01:56:40 2003 +0200
    23.3 @@ -820,7 +820,7 @@
    23.4  text{*The rank function for the constructible universe*}
    23.5  constdefs
    23.6    lrank :: "i=>i" --{*Kunen's definition VI 1.7*}
    23.7 -    "lrank(x) == \<mu>i. x \<in> Lset(succ(i))"
    23.8 +    "lrank(x) == \<mu> i. x \<in> Lset(succ(i))"
    23.9  
   23.10  lemma L_I: "[|x \<in> Lset(i); Ord(i)|] ==> L(x)"
   23.11  by (simp add: L_def, blast)
    24.1 --- a/src/ZF/Constructible/L_axioms.thy	Wed Aug 27 18:22:34 2003 +0200
    24.2 +++ b/src/ZF/Constructible/L_axioms.thy	Thu Aug 28 01:56:40 2003 +0200
    24.3 @@ -189,7 +189,7 @@
    24.4  text{*instances of locale constants*}
    24.5  constdefs
    24.6    L_F0 :: "[i=>o,i] => i"
    24.7 -    "L_F0(P,y) == \<mu>b. (\<exists>z. L(z) \<and> P(<y,z>)) --> (\<exists>z\<in>Lset(b). P(<y,z>))"
    24.8 +    "L_F0(P,y) == \<mu> b. (\<exists>z. L(z) \<and> P(<y,z>)) --> (\<exists>z\<in>Lset(b). P(<y,z>))"
    24.9  
   24.10    L_FF :: "[i=>o,i] => i"
   24.11      "L_FF(P)   == \<lambda>a. \<Union>y\<in>Lset(a). L_F0(P,y)"
    25.1 --- a/src/ZF/Constructible/Normal.thy	Wed Aug 27 18:22:34 2003 +0200
    25.2 +++ b/src/ZF/Constructible/Normal.thy	Thu Aug 28 01:56:40 2003 +0200
    25.3 @@ -84,7 +84,7 @@
    25.4    assumes closed:    "a\<in>A ==> Closed(P(a))"
    25.5        and unbounded: "a\<in>A ==> Unbounded(P(a))"
    25.6        and A_non0: "A\<noteq>0"
    25.7 -  defines "next_greater(a,x) == \<mu>y. x<y \<and> P(a,y)"
    25.8 +  defines "next_greater(a,x) == \<mu> y. x<y \<and> P(a,y)"
    25.9        and "sup_greater(x) == \<Union>a\<in>A. next_greater(a,x)"
   25.10   
   25.11  
    26.1 --- a/src/ZF/Constructible/Reflection.thy	Wed Aug 27 18:22:34 2003 +0200
    26.2 +++ b/src/ZF/Constructible/Reflection.thy	Thu Aug 28 01:56:40 2003 +0200
    26.3 @@ -42,7 +42,7 @@
    26.4    fixes F0 --{*ordinal for a specific value @{term y}*}
    26.5    fixes FF --{*sup over the whole level, @{term "y\<in>Mset(a)"}*}
    26.6    fixes ClEx --{*Reflecting ordinals for the formula @{term "\<exists>z. P"}*}
    26.7 -  defines "F0(P,y) == \<mu>b. (\<exists>z. M(z) & P(<y,z>)) --> 
    26.8 +  defines "F0(P,y) == \<mu> b. (\<exists>z. M(z) & P(<y,z>)) --> 
    26.9                                 (\<exists>z\<in>Mset(b). P(<y,z>))"
   26.10        and "FF(P)   == \<lambda>a. \<Union>y\<in>Mset(a). F0(P,y)"
   26.11        and "ClEx(P,a) == Limit(a) & normalize(FF(P),a) = a"
   26.12 @@ -354,8 +354,8 @@
   26.13  to be relativized.*}
   26.14  lemma (in reflection) 
   26.15       "Reflects(?Cl,
   26.16 -               \<lambda>A. 0\<notin>A --> (\<exists>f. M(f) & f \<in> (\<Pi>X \<in> A. X)),
   26.17 -               \<lambda>a A. 0\<notin>A --> (\<exists>f\<in>Mset(a). f \<in> (\<Pi>X \<in> A. X)))"
   26.18 +               \<lambda>A. 0\<notin>A --> (\<exists>f. M(f) & f \<in> (\<Pi> X \<in> A. X)),
   26.19 +               \<lambda>a A. 0\<notin>A --> (\<exists>f\<in>Mset(a). f \<in> (\<Pi> X \<in> A. X)))"
   26.20  by fast
   26.21  
   26.22  end
    27.1 --- a/src/ZF/Induct/Brouwer.thy	Wed Aug 27 18:22:34 2003 +0200
    27.2 +++ b/src/ZF/Induct/Brouwer.thy	Thu Aug 28 01:56:40 2003 +0200
    27.3 @@ -53,7 +53,7 @@
    27.4    monos Pi_mono
    27.5    type_intros le_trans [OF UN_upper_cardinal le_nat_Un_cardinal] inf_datatype_intros
    27.6  
    27.7 -lemma Well_unfold: "Well(A, B) = (\<Sigma>x \<in> A. B(x) -> Well(A, B))"
    27.8 +lemma Well_unfold: "Well(A, B) = (\<Sigma> x \<in> A. B(x) -> Well(A, B))"
    27.9    by (fast intro!: Well.intros [unfolded Well.con_defs]
   27.10      elim: Well.cases [unfolded Well.con_defs])
   27.11  
    28.1 --- a/src/ZF/OrderArith.thy	Wed Aug 27 18:22:34 2003 +0200
    28.2 +++ b/src/ZF/OrderArith.thy	Thu Aug 28 01:56:40 2003 +0200
    28.3 @@ -556,7 +556,7 @@
    28.4  text{*As a special case, we have @{term "bij(Pow(A*B), A -> Pow(B))"} *}
    28.5  lemma Pow_Sigma_bij:
    28.6      "(\<lambda>r \<in> Pow(Sigma(A,B)). \<lambda>x \<in> A. r``{x})  
    28.7 -     \<in> bij(Pow(Sigma(A,B)), \<Pi>x \<in> A. Pow(B(x)))"
    28.8 +     \<in> bij(Pow(Sigma(A,B)), \<Pi> x \<in> A. Pow(B(x)))"
    28.9  apply (rule_tac d = "%f. \<Union>x \<in> A. \<Union>y \<in> f`x. {<x,y>}" in lam_bijective)
   28.10  apply (blast intro: lam_type)
   28.11  apply (blast dest: apply_type, simp_all)
    29.1 --- a/src/ZF/UNITY/State.thy	Wed Aug 27 18:22:34 2003 +0200
    29.2 +++ b/src/ZF/UNITY/State.thy	Thu Aug 28 01:56:40 2003 +0200
    29.3 @@ -23,7 +23,7 @@
    29.4  
    29.5  constdefs
    29.6    state   :: i
    29.7 -   "state == \<Pi>x \<in> var. cons(default_val(x), type_of(x))"
    29.8 +   "state == \<Pi> x \<in> var. cons(default_val(x), type_of(x))"
    29.9  
   29.10    st0     :: i
   29.11     "st0 == \<lambda>x \<in> var. default_val(x)"
    30.1 --- a/src/ZF/Zorn.thy	Wed Aug 27 18:22:34 2003 +0200
    30.2 +++ b/src/ZF/Zorn.thy	Thu Aug 28 01:56:40 2003 +0200
    30.3 @@ -197,14 +197,14 @@
    30.4  done
    30.5  
    30.6  lemma choice_super:
    30.7 -     "[| ch \<in> (\<Pi>X \<in> Pow(chain(S)) - {0}. X); X \<in> chain(S);  X \<notin> maxchain(S) |]
    30.8 +     "[| ch \<in> (\<Pi> X \<in> Pow(chain(S)) - {0}. X); X \<in> chain(S);  X \<notin> maxchain(S) |]
    30.9        ==> ch ` super(S,X) \<in> super(S,X)"
   30.10  apply (erule apply_type)
   30.11  apply (unfold super_def maxchain_def, blast)
   30.12  done
   30.13  
   30.14  lemma choice_not_equals:
   30.15 -     "[| ch \<in> (\<Pi>X \<in> Pow(chain(S)) - {0}. X); X \<in> chain(S);  X \<notin> maxchain(S) |]
   30.16 +     "[| ch \<in> (\<Pi> X \<in> Pow(chain(S)) - {0}. X); X \<in> chain(S);  X \<notin> maxchain(S) |]
   30.17        ==> ch ` super(S,X) \<noteq> X"
   30.18  apply (rule notI)
   30.19  apply (drule choice_super, assumption, assumption)
   30.20 @@ -213,7 +213,7 @@
   30.21  
   30.22  text{*This justifies Definition 4.4*}
   30.23  lemma Hausdorff_next_exists:
   30.24 -     "ch \<in> (\<Pi>X \<in> Pow(chain(S))-{0}. X) ==>
   30.25 +     "ch \<in> (\<Pi> X \<in> Pow(chain(S))-{0}. X) ==>
   30.26        \<exists>next \<in> increasing(S). \<forall>X \<in> Pow(S).
   30.27                     next`X = if(X \<in> chain(S)-maxchain(S), ch`super(S,X), X)"
   30.28  apply (rule_tac x="\<lambda>X\<in>Pow(S).
   30.29 @@ -237,7 +237,7 @@
   30.30  text{*Lemma 4*}
   30.31  lemma TFin_chain_lemma4:
   30.32       "[| c \<in> TFin(S,next);
   30.33 -         ch \<in> (\<Pi>X \<in> Pow(chain(S))-{0}. X);
   30.34 +         ch \<in> (\<Pi> X \<in> Pow(chain(S))-{0}. X);
   30.35           next \<in> increasing(S);
   30.36           \<forall>X \<in> Pow(S). next`X =
   30.37                            if(X \<in> chain(S)-maxchain(S), ch`super(S,X), X) |]
   30.38 @@ -344,14 +344,14 @@
   30.39  text{** Defining the "next" operation for Zermelo's Theorem **}
   30.40  
   30.41  lemma choice_Diff:
   30.42 -     "[| ch \<in> (\<Pi>X \<in> Pow(S) - {0}. X);  X \<subseteq> S;  X\<noteq>S |] ==> ch ` (S-X) \<in> S-X"
   30.43 +     "[| ch \<in> (\<Pi> X \<in> Pow(S) - {0}. X);  X \<subseteq> S;  X\<noteq>S |] ==> ch ` (S-X) \<in> S-X"
   30.44  apply (erule apply_type)
   30.45  apply (blast elim!: equalityE)
   30.46  done
   30.47  
   30.48  text{*This justifies Definition 6.1*}
   30.49  lemma Zermelo_next_exists:
   30.50 -     "ch \<in> (\<Pi>X \<in> Pow(S)-{0}. X) ==>
   30.51 +     "ch \<in> (\<Pi> X \<in> Pow(S)-{0}. X) ==>
   30.52             \<exists>next \<in> increasing(S). \<forall>X \<in> Pow(S).
   30.53                        next`X = (if X=S then S else cons(ch`(S-X), X))"
   30.54  apply (rule_tac x="\<lambda>X\<in>Pow(S). if X=S then S else cons(ch`(S-X), X)"
   30.55 @@ -371,7 +371,7 @@
   30.56  
   30.57  text{*The construction of the injection*}
   30.58  lemma choice_imp_injection:
   30.59 -     "[| ch \<in> (\<Pi>X \<in> Pow(S)-{0}. X);
   30.60 +     "[| ch \<in> (\<Pi> X \<in> Pow(S)-{0}. X);
   30.61           next \<in> increasing(S);
   30.62           \<forall>X \<in> Pow(S). next`X = if(X=S, S, cons(ch`(S-X), X)) |]
   30.63        ==> (\<lambda> x \<in> S. Union({y \<in> TFin(S,next). x \<notin> y}))
    31.1 --- a/src/ZF/equalities.thy	Wed Aug 27 18:22:34 2003 +0200
    31.2 +++ b/src/ZF/equalities.thy	Thu Aug 28 01:56:40 2003 +0200
    31.3 @@ -537,19 +537,19 @@
    31.4  by blast
    31.5  
    31.6  lemma SUM_UN_distrib1:
    31.7 -     "(\<Sigma>x \<in> (\<Union>y\<in>A. C(y)). B(x)) = (\<Union>y\<in>A. \<Sigma>x\<in>C(y). B(x))"
    31.8 +     "(\<Sigma> x \<in> (\<Union>y\<in>A. C(y)). B(x)) = (\<Union>y\<in>A. \<Sigma> x\<in>C(y). B(x))"
    31.9  by blast
   31.10  
   31.11  lemma SUM_UN_distrib2:
   31.12 -     "(\<Sigma>i\<in>I. \<Union>j\<in>J. C(i,j)) = (\<Union>j\<in>J. \<Sigma>i\<in>I. C(i,j))"
   31.13 +     "(\<Sigma> i\<in>I. \<Union>j\<in>J. C(i,j)) = (\<Union>j\<in>J. \<Sigma> i\<in>I. C(i,j))"
   31.14  by blast
   31.15  
   31.16  lemma SUM_Un_distrib1:
   31.17 -     "(\<Sigma>i\<in>I Un J. C(i)) = (\<Sigma>i\<in>I. C(i)) Un (\<Sigma>j\<in>J. C(j))"
   31.18 +     "(\<Sigma> i\<in>I Un J. C(i)) = (\<Sigma> i\<in>I. C(i)) Un (\<Sigma> j\<in>J. C(j))"
   31.19  by blast
   31.20  
   31.21  lemma SUM_Un_distrib2:
   31.22 -     "(\<Sigma>i\<in>I. A(i) Un B(i)) = (\<Sigma>i\<in>I. A(i)) Un (\<Sigma>i\<in>I. B(i))"
   31.23 +     "(\<Sigma> i\<in>I. A(i) Un B(i)) = (\<Sigma> i\<in>I. A(i)) Un (\<Sigma> i\<in>I. B(i))"
   31.24  by blast
   31.25  
   31.26  (*First-order version of the above, for rewriting*)
   31.27 @@ -557,11 +557,11 @@
   31.28  by (rule SUM_Un_distrib2)
   31.29  
   31.30  lemma SUM_Int_distrib1:
   31.31 -     "(\<Sigma>i\<in>I Int J. C(i)) = (\<Sigma>i\<in>I. C(i)) Int (\<Sigma>j\<in>J. C(j))"
   31.32 +     "(\<Sigma> i\<in>I Int J. C(i)) = (\<Sigma> i\<in>I. C(i)) Int (\<Sigma> j\<in>J. C(j))"
   31.33  by blast
   31.34  
   31.35  lemma SUM_Int_distrib2:
   31.36 -     "(\<Sigma>i\<in>I. A(i) Int B(i)) = (\<Sigma>i\<in>I. A(i)) Int (\<Sigma>i\<in>I. B(i))"
   31.37 +     "(\<Sigma> i\<in>I. A(i) Int B(i)) = (\<Sigma> i\<in>I. A(i)) Int (\<Sigma> i\<in>I. B(i))"
   31.38  by blast
   31.39  
   31.40  (*First-order version of the above, for rewriting*)
   31.41 @@ -569,7 +569,7 @@
   31.42  by (rule SUM_Int_distrib2)
   31.43  
   31.44  (*Cf Aczel, Non-Well-Founded Sets, page 115*)
   31.45 -lemma SUM_eq_UN: "(\<Sigma>i\<in>I. A(i)) = (\<Union>i\<in>I. {i} * A(i))"
   31.46 +lemma SUM_eq_UN: "(\<Sigma> i\<in>I. A(i)) = (\<Union>i\<in>I. {i} * A(i))"
   31.47  by blast
   31.48  
   31.49  lemma times_subset_iff:
   31.50 @@ -577,7 +577,7 @@
   31.51  by blast
   31.52  
   31.53  lemma Int_Sigma_eq:
   31.54 -     "(\<Sigma>x \<in> A'. B'(x)) Int (\<Sigma>x \<in> A. B(x)) = (\<Sigma>x \<in> A' Int A. B'(x) Int B(x))"
   31.55 +     "(\<Sigma> x \<in> A'. B'(x)) Int (\<Sigma> x \<in> A. B(x)) = (\<Sigma> x \<in> A' Int A. B'(x) Int B(x))"
   31.56  by blast
   31.57  
   31.58  (** Domain **)
    32.1 --- a/src/ZF/ex/Limit.thy	Wed Aug 27 18:22:34 2003 +0200
    32.2 +++ b/src/ZF/ex/Limit.thy	Thu Aug 28 01:56:40 2003 +0200
    32.3 @@ -103,8 +103,8 @@
    32.4    (* Twice, constructions on cpos are more difficult. *)
    32.5    iprod     :: "i=>i"
    32.6      "iprod(DD) ==
    32.7 -     <(\<Pi>n \<in> nat. set(DD`n)),
    32.8 -      {x:(\<Pi>n \<in> nat. set(DD`n))*(\<Pi>n \<in> nat. set(DD`n)).
    32.9 +     <(\<Pi> n \<in> nat. set(DD`n)),
   32.10 +      {x:(\<Pi> n \<in> nat. set(DD`n))*(\<Pi> n \<in> nat. set(DD`n)).
   32.11         \<forall>n \<in> nat. rel(DD`n,fst(x)`n,snd(x)`n)}>"
   32.12  
   32.13    mkcpo     :: "[i,i=>o]=>i"
   32.14 @@ -1024,18 +1024,18 @@
   32.15  (*----------------------------------------------------------------------*)
   32.16  
   32.17  lemma iprodI:
   32.18 -    "x:(\<Pi>n \<in> nat. set(DD`n)) ==> x \<in> set(iprod(DD))"
   32.19 +    "x:(\<Pi> n \<in> nat. set(DD`n)) ==> x \<in> set(iprod(DD))"
   32.20  by (simp add: set_def iprod_def)
   32.21  
   32.22  lemma iprodE:
   32.23 -    "x \<in> set(iprod(DD)) ==> x:(\<Pi>n \<in> nat. set(DD`n))"
   32.24 +    "x \<in> set(iprod(DD)) ==> x:(\<Pi> n \<in> nat. set(DD`n))"
   32.25  by (simp add: set_def iprod_def)
   32.26  
   32.27  (* Contains typing conditions in contrast to HOL-ST *)
   32.28  
   32.29  lemma rel_iprodI:
   32.30 -    "[|!!n. n \<in> nat ==> rel(DD`n,f`n,g`n); f:(\<Pi>n \<in> nat. set(DD`n));
   32.31 -       g:(\<Pi>n \<in> nat. set(DD`n))|] ==> rel(iprod(DD),f,g)"
   32.32 +    "[|!!n. n \<in> nat ==> rel(DD`n,f`n,g`n); f:(\<Pi> n \<in> nat. set(DD`n));
   32.33 +       g:(\<Pi> n \<in> nat. set(DD`n))|] ==> rel(iprod(DD),f,g)"
   32.34  by (simp add: iprod_def rel_I)
   32.35  
   32.36  lemma rel_iprodE:
   32.37 @@ -1205,14 +1205,14 @@
   32.38  (*----------------------------------------------------------------------*)
   32.39  
   32.40  lemma DinfI:
   32.41 -    "[|x:(\<Pi>n \<in> nat. set(DD`n));
   32.42 +    "[|x:(\<Pi> n \<in> nat. set(DD`n));
   32.43         !!n. n \<in> nat ==> Rp(DD`n,DD`succ(n),ee`n)`(x`succ(n)) = x`n|]
   32.44       ==> x \<in> set(Dinf(DD,ee))"
   32.45  apply (simp add: Dinf_def)
   32.46  apply (blast intro: mkcpoI iprodI)
   32.47  done
   32.48  
   32.49 -lemma Dinf_prod: "x \<in> set(Dinf(DD,ee)) ==> x:(\<Pi>n \<in> nat. set(DD`n))"
   32.50 +lemma Dinf_prod: "x \<in> set(Dinf(DD,ee)) ==> x:(\<Pi> n \<in> nat. set(DD`n))"
   32.51  apply (simp add: Dinf_def)
   32.52  apply (erule mkcpoD1 [THEN iprodE])
   32.53  done
   32.54 @@ -1226,7 +1226,7 @@
   32.55  
   32.56  lemma rel_DinfI:
   32.57      "[|!!n. n \<in> nat ==> rel(DD`n,x`n,y`n);
   32.58 -       x:(\<Pi>n \<in> nat. set(DD`n)); y:(\<Pi>n \<in> nat. set(DD`n))|] 
   32.59 +       x:(\<Pi> n \<in> nat. set(DD`n)); y:(\<Pi> n \<in> nat. set(DD`n))|] 
   32.60       ==> rel(Dinf(DD,ee),x,y)"
   32.61  apply (simp add: Dinf_def)
   32.62  apply (blast intro: rel_mkcpo [THEN iffD2] rel_iprodI iprodI)