bounded abstraction now uses syntax "%" / "\<lambda>" instead of "lam";
authorwenzelm
Mon Dec 10 20:59:43 2001 +0100 (2001-12-10)
changeset 124596978ab7cac64
parent 12458 a8c219e76ae0
child 12460 624a8cd51b4e
bounded abstraction now uses syntax "%" / "\<lambda>" instead of "lam";
src/HOL/Fun.ML
src/HOL/Fun.thy
src/HOL/GroupTheory/Bij.ML
src/HOL/GroupTheory/Bij.thy
src/HOL/GroupTheory/DirProd.ML
src/HOL/GroupTheory/DirProd.thy
src/HOL/GroupTheory/FactGroup.ML
src/HOL/GroupTheory/FactGroup.thy
src/HOL/GroupTheory/Group.ML
src/HOL/GroupTheory/Group.thy
src/HOL/GroupTheory/Homomorphism.ML
src/HOL/GroupTheory/PiSets.ML
src/HOL/GroupTheory/PiSets.thy
src/HOL/GroupTheory/Ring.thy
src/HOL/GroupTheory/RingConstr.thy
src/HOL/GroupTheory/Sylow.ML
src/HOL/Hilbert_Choice_lemmas.ML
src/HOL/ex/Tarski.ML
src/HOL/ex/Tarski.thy
     1.1 --- a/src/HOL/Fun.ML	Mon Dec 10 20:58:15 2001 +0100
     1.2 +++ b/src/HOL/Fun.ML	Mon Dec 10 20:59:43 2001 +0100
     1.3 @@ -445,25 +445,25 @@
     1.4  qed "inj_on_compose";
     1.5  
     1.6  
     1.7 -(*** restrict / lam ***)
     1.8 +(*** restrict / bounded abstraction ***)
     1.9  
    1.10 -Goal "f`A <= B ==> (lam x: A. f x) : A funcset B";
    1.11 +Goal "f`A <= B ==> (%x:A. f x) : A funcset B";
    1.12  by (auto_tac (claset(),
    1.13  	      simpset() addsimps [restrict_def, Pi_def]));
    1.14  qed "restrict_in_funcset";
    1.15  
    1.16  val prems = Goalw [restrict_def, Pi_def]
    1.17 -     "(!!x. x: A ==> f x: B x) ==> (lam x: A. f x) : Pi A B";
    1.18 +     "(!!x. x: A ==> f x: B x) ==> (%x:A. f x) : Pi A B";
    1.19  by (asm_simp_tac (simpset() addsimps prems) 1);
    1.20  qed "restrictI";
    1.21  
    1.22 -Goal "(lam y: A. f y) x = (if x : A then f x else arbitrary)";
    1.23 +Goal "(%y:A. f y) x = (if x : A then f x else arbitrary)";
    1.24  by (asm_simp_tac (simpset() addsimps [restrict_def]) 1);
    1.25  qed "restrict_apply";
    1.26  Addsimps [restrict_apply];
    1.27  
    1.28  val prems = Goal
    1.29 -    "(!!x. x: A ==> f x = g x) ==> (lam x: A. f x) = (lam x: A. g x)";
    1.30 +    "(!!x. x: A ==> f x = g x) ==> (%x:A. f x) = (%x:A. g x)";
    1.31  by (rtac ext 1);
    1.32  by (auto_tac (claset(),
    1.33  	      simpset() addsimps prems@[restrict_def, Pi_def]));
    1.34 @@ -474,12 +474,12 @@
    1.35  qed "inj_on_restrict_eq";
    1.36  
    1.37  
    1.38 -Goal "f : A funcset B ==> compose A (lam y:B. y) f = f";
    1.39 +Goal "f : A funcset B ==> compose A (%y:B. y) f = f";
    1.40  by (rtac ext 1); 
    1.41  by (auto_tac (claset(), simpset() addsimps [compose_def, Pi_def])); 
    1.42  qed "Id_compose";
    1.43  
    1.44 -Goal "g : A funcset B ==> compose A g (lam x:A. x) = g";
    1.45 +Goal "g : A funcset B ==> compose A g (%x:A. x) = g";
    1.46  by (rtac ext 1); 
    1.47  by (auto_tac (claset(), simpset() addsimps [compose_def, Pi_def])); 
    1.48  qed "compose_Id";
     2.1 --- a/src/HOL/Fun.thy	Mon Dec 10 20:58:15 2001 +0100
     2.2 +++ b/src/HOL/Fun.thy	Mon Dec 10 20:59:43 2001 +0100
     2.3 @@ -75,9 +75,11 @@
     2.4  syntax
     2.5    "@Pi"  :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3PI _:_./ _)" 10)
     2.6    funcset :: "['a set, 'b set] => ('a => 'b) set"      (infixr 60)
     2.7 -  "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a => 'b)"  ("(3lam _:_./ _)" 10)
     2.8 +  "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a => 'b)"  ("(3%_:_./ _)" [0, 0, 3] 3)
     2.9 +syntax (xsymbols)
    2.10 +  "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a => 'b)"  ("(3\\<lambda>_\<in>_./ _)" [0, 0, 3] 3)
    2.11  
    2.12 -  (*Giving funcset the arrow syntax (namely ->) clashes with other theories*)
    2.13 +  (*Giving funcset an arrow syntax (-> or =>) clashes with many existing theories*)
    2.14  
    2.15  syntax (xsymbols)
    2.16    "@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\\<Pi> _\\<in>_./ _)"   10)
    2.17 @@ -85,11 +87,11 @@
    2.18  translations
    2.19    "PI x:A. B" => "Pi A (%x. B)"
    2.20    "A funcset B"    => "Pi A (_K B)"
    2.21 -  "lam x:A. f"  == "restrict (%x. f) A"
    2.22 +  "%x:A. f"  == "restrict (%x. f) A"
    2.23  
    2.24  constdefs
    2.25    compose :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)"
    2.26 -    "compose A g f == lam x : A. g(f x)"
    2.27 +  "compose A g f == %x:A. g (f x)"
    2.28  
    2.29  end
    2.30  
     3.1 --- a/src/HOL/GroupTheory/Bij.ML	Mon Dec 10 20:58:15 2001 +0100
     3.2 +++ b/src/HOL/GroupTheory/Bij.ML	Mon Dec 10 20:59:43 2001 +0100
     3.3 @@ -46,11 +46,11 @@
     3.4  
     3.5  
     3.6  (* restrict (Inv S f) S  *)
     3.7 -Goal "f \\<in> B ==> (lam x: S. (inv' f) x) \\<in> B";
     3.8 +Goal "f \\<in> B ==> (%x:S. (inv' f) x) \\<in> B";
     3.9  by (rtac BijI 1);
    3.10 -(* 1. (lam x: S. (inv' f) x): S \\<rightarrow> S *)
    3.11 +(* 1. (%x:S. (inv' f) x): S \\<rightarrow> S *)
    3.12  by (afs [Inv_funcset] 1);
    3.13 -(* 2. (lam x: S. (inv' f) x) ` S = S *)
    3.14 +(* 2. (%x:S. (inv' f) x) ` S = S *)
    3.15  by (asm_full_simp_tac (simpset() addsimps [inv_def]) 1); 
    3.16  by (rtac equalityI 1);
    3.17  (* 2. <= *)
    3.18 @@ -73,7 +73,7 @@
    3.19  by (auto_tac (claset(), simpset() addsimps [funcsetI, inj_on_def])); 
    3.20  qed "restrict_id_Bij";
    3.21  
    3.22 -Goal "f \\<in> B ==> (lam g: B. lam x: S. (inv' g) x) f = (lam x: S. (inv' f) x)";
    3.23 +Goal "f \\<in> B ==> (%g:B. %x:S. (inv' g) x) f = (%x:S. (inv' f) x)";
    3.24  by (Asm_full_simp_tac 1); 
    3.25  qed "eval_restrict_Inv";
    3.26  
    3.27 @@ -95,7 +95,7 @@
    3.28  
    3.29  val BG_def = thm "BG_def";
    3.30  
    3.31 -Goal "[| x\\<in>B; y\\<in>B |] ==> (lam g: B. lam f: B. g o' f) x y = x o' y";
    3.32 +Goal "[| x\\<in>B; y\\<in>B |] ==> (%g:B. %f:B. g o' f) x y = x o' y";
    3.33  by (Asm_full_simp_tac 1); 
    3.34  qed "eval_restrict_comp2";
    3.35  
    3.36 @@ -106,11 +106,11 @@
    3.37  by (afs [BijGroup_def] 1);
    3.38  qed "BG_carrier";
    3.39  
    3.40 -Goal "bin_op BG == lam g: B. lam f: B. g o' f";
    3.41 +Goal "bin_op BG == %g:B. %f:B. g o' f";
    3.42  by (afs [BijGroup_def] 1);
    3.43  qed "BG_bin_op";
    3.44                 
    3.45 -Goal "inverse BG == lam f: B. lam x: S. (inv' f) x";
    3.46 +Goal "inverse BG == %f:B. %x:S. (inv' f) x";
    3.47  by (afs [BijGroup_def] 1);
    3.48  qed "BG_inverse"; 
    3.49  
    3.50 @@ -126,7 +126,7 @@
    3.51  Delsimps [B_def, BG_def, o'_def, inv'_def, e'_def];
    3.52  
    3.53  
    3.54 -Goal "(lam g: B. lam f: B. g o' f) \\<in> B \\<rightarrow> B \\<rightarrow> B";
    3.55 +Goal "(%g:B. %f:B. g o' f) \\<in> B \\<rightarrow> B \\<rightarrow> B";
    3.56  by (simp_tac (simpset() addsimps [funcsetI, compose_Bij]) 1); 
    3.57  qed "restrict_compose_Bij";
    3.58  
     4.1 --- a/src/HOL/GroupTheory/Bij.thy	Mon Dec 10 20:58:15 2001 +0100
     4.2 +++ b/src/HOL/GroupTheory/Bij.thy	Mon Dec 10 20:59:43 2001 +0100
     4.3 @@ -16,9 +16,9 @@
     4.4  constdefs 
     4.5  BijGroup ::  "'a set => (('a => 'a) grouptype)"
     4.6  "BijGroup S == (| carrier = Bij S, 
     4.7 -                  bin_op  = lam g: Bij S. lam f: Bij S. compose S g f,
     4.8 -                  inverse = lam f: Bij S. lam x: S. (Inv S f) x, 
     4.9 -                  unit    = lam x: S. x |)"
    4.10 +                  bin_op  = %g: Bij S. %f: Bij S. compose S g f,
    4.11 +                  inverse = %f: Bij S. %x: S. (Inv S f) x, 
    4.12 +                  unit    = %x: S. x |)"
    4.13  
    4.14  locale bij = 
    4.15    fixes 
    4.16 @@ -31,7 +31,7 @@
    4.17      B_def    "B == Bij S"
    4.18      o'_def   "g o' f == compose S g f"
    4.19      inv'_def   "inv' f == Inv S f"
    4.20 -    e'_def   "e'  == (lam x: S. x)"
    4.21 +    e'_def   "e'  == (%x: S. x)"
    4.22  
    4.23  locale bijgroup = bij +
    4.24    fixes 
     5.1 --- a/src/HOL/GroupTheory/DirProd.ML	Mon Dec 10 20:58:15 2001 +0100
     5.2 +++ b/src/HOL/GroupTheory/DirProd.ML	Mon Dec 10 20:59:43 2001 +0100
     5.3 @@ -22,11 +22,11 @@
     5.4  qed "P_carrier";
     5.5  
     5.6  Goal "(P.<f>) = \
     5.7 -\     (lam (x, x'): (P.<cr>). lam (y, y'): (P.<cr>). ( x ## y, x' ##' y'))";
     5.8 +\     (%(x, x'): (P.<cr>). %(y, y'): (P.<cr>). ( x ## y, x' ##' y'))";
     5.9  by (afs [ProdGroup_def, binop_def, binop'_def] 1);
    5.10  qed "P_bin_op";
    5.11  
    5.12 -Goal "(P.<inv>) = (lam (x, y): (P.<cr>). (i x, i' y))";
    5.13 +Goal "(P.<inv>) = (%(x, y): (P.<cr>). (i x, i' y))";
    5.14  by (afs [ProdGroup_def, inv_def, inv'_def] 1);
    5.15  qed "P_inverse";
    5.16  
    5.17 @@ -35,9 +35,9 @@
    5.18  qed "P_unit";
    5.19  
    5.20  Goal "P = (| carrier = P.<cr>, \
    5.21 -\       bin_op = (lam (x, x'): (P.<cr>). lam (y, y'): (P.<cr>).\
    5.22 +\       bin_op = (%(x, x'): (P.<cr>). %(y, y'): (P.<cr>).\
    5.23  \                  (x ## y, x' ##' y')), \
    5.24 -\       inverse = (lam (x, y): (P.<cr>). (i x, i' y)), \
    5.25 +\       inverse = (%(x, y): (P.<cr>). (i x, i' y)), \
    5.26  \       unit = P.<e> |)";
    5.27  by (afs [ProdGroup_def, P_carrier, P_bin_op, P_inverse, P_unit] 1);
    5.28  by (afs [binop_def, binop'_def, inv_def, inv'_def] 1);
     6.1 --- a/src/HOL/GroupTheory/DirProd.thy	Mon Dec 10 20:58:15 2001 +0100
     6.2 +++ b/src/HOL/GroupTheory/DirProd.thy	Mon Dec 10 20:59:43 2001 +0100
     6.3 @@ -12,12 +12,12 @@
     6.4    ProdGroup :: "(['a grouptype, 'b grouptype] => ('a * 'b) grouptype)"
     6.5  
     6.6  defs 
     6.7 -  ProdGroup_def "ProdGroup == lam G: Group. lam G': Group.
     6.8 +  ProdGroup_def "ProdGroup == %G: Group. %G': Group.
     6.9      (| carrier = ((G.<cr>) \\<times> (G'.<cr>)),
    6.10 -       bin_op = (lam (x, x'): ((G.<cr>) \\<times> (G'.<cr>)). 
    6.11 -                 lam (y, y'): ((G.<cr>) \\<times> (G'.<cr>)).
    6.12 +       bin_op = (%(x, x'): ((G.<cr>) \\<times> (G'.<cr>)). 
    6.13 +                 %(y, y'): ((G.<cr>) \\<times> (G'.<cr>)).
    6.14                    ((G.<f>) x y,(G'.<f>) x' y')),
    6.15 -       inverse = (lam (x, y): ((G.<cr>) \\<times> (G'.<cr>)). ((G.<inv>) x, (G'.<inv>) y)),
    6.16 +       inverse = (%(x, y): ((G.<cr>) \\<times> (G'.<cr>)). ((G.<inv>) x, (G'.<inv>) y)),
    6.17         unit = ((G.<e>),(G'.<e>)) |)"
    6.18  
    6.19  syntax
     7.1 --- a/src/HOL/GroupTheory/FactGroup.ML	Mon Dec 10 20:58:15 2001 +0100
     7.2 +++ b/src/HOL/GroupTheory/FactGroup.ML	Mon Dec 10 20:59:43 2001 +0100
     7.3 @@ -18,11 +18,11 @@
     7.4  by (afs [FactGroup_def] 1);
     7.5  qed "F_carrier";
     7.6  
     7.7 -Goal "bin_op F = (lam X: {* H *}. lam Y: {* H *}. X <#> Y) ";
     7.8 +Goal "bin_op F = (%X: {* H *}. %Y: {* H *}. X <#> Y) ";
     7.9  by (afs [FactGroup_def, setprod_def] 1);
    7.10  qed "F_bin_op";
    7.11  
    7.12 -Goal "inverse F = (lam X: {* H *}. I(X))";
    7.13 +Goal "inverse F = (%X: {* H *}. I(X))";
    7.14  by (afs [FactGroup_def, setinv_def] 1);
    7.15  qed "F_inverse";
    7.16  
    7.17 @@ -31,8 +31,8 @@
    7.18  qed "F_unit";
    7.19  
    7.20  Goal "F = (| carrier = {* H *}, \
    7.21 -\            bin_op  = (lam X: {* H *}. lam Y: {* H *}. X <#> Y), \
    7.22 -\            inverse = (lam X: {* H *}. I(X)),  unit = H |)";
    7.23 +\            bin_op  = (%X: {* H *}. %Y: {* H *}. X <#> Y), \
    7.24 +\            inverse = (%X: {* H *}. I(X)),  unit = H |)";
    7.25  by (afs [FactGroup_def, F_carrier, F_bin_op, F_inverse, F_unit] 1);
    7.26  by (auto_tac (claset() addSIs [restrict_ext], 
    7.27                simpset() addsimps [set_prod_def, setprod_def, setinv_def])); 
     8.1 --- a/src/HOL/GroupTheory/FactGroup.thy	Mon Dec 10 20:58:15 2001 +0100
     8.2 +++ b/src/HOL/GroupTheory/FactGroup.thy	Mon Dec 10 20:59:43 2001 +0100
     8.3 @@ -12,10 +12,10 @@
     8.4    FactGroup :: "(['a grouptype, 'a set] => ('a set) grouptype)"
     8.5  
     8.6     "FactGroup ==
     8.7 -     lam G: Group. lam H: {H. H <| G}.
     8.8 +     %G: Group. %H: {H. H <| G}.
     8.9        (| carrier = set_r_cos G H,
    8.10 -	 bin_op = (lam X: set_r_cos G H. lam Y: set_r_cos G H. set_prod G X Y),
    8.11 -	 inverse = (lam X: set_r_cos G H. set_inv G X), 
    8.12 +	 bin_op = (%X: set_r_cos G H. %Y: set_r_cos G H. set_prod G X Y),
    8.13 +	 inverse = (%X: set_r_cos G H. set_inv G X), 
    8.14  	 unit = H |)"
    8.15  
    8.16  syntax
     9.1 --- a/src/HOL/GroupTheory/Group.ML	Mon Dec 10 20:58:15 2001 +0100
     9.2 +++ b/src/HOL/GroupTheory/Group.ML	Mon Dec 10 20:59:43 2001 +0100
     9.3 @@ -155,8 +155,8 @@
     9.4  val SubgroupI = export subgroupI;
     9.5  
     9.6  Goal "H <<= G  ==> \
     9.7 -\      (|carrier = H, bin_op = lam x:H. lam y:H. x ## y, \
     9.8 -\       inverse = lam x:H. i(x), unit = e|)\\<in>Group";
     9.9 +\      (|carrier = H, bin_op = %x:H. %y:H. x ## y, \
    9.10 +\       inverse = %x:H. i(x), unit = e|)\\<in>Group";
    9.11  by (afs [subgroup_def, binop_def, inv_def, e_def] 1);
    9.12  qed "subgroupE2";
    9.13  val SubgroupE2 = export subgroupE2;
    10.1 --- a/src/HOL/GroupTheory/Group.thy	Mon Dec 10 20:58:15 2001 +0100
    10.2 +++ b/src/HOL/GroupTheory/Group.thy	Mon Dec 10 20:59:43 2001 +0100
    10.3 @@ -60,8 +60,8 @@
    10.4  
    10.5  defs
    10.6    subgroup_def  "subgroup == SIGMA G: Group. {H. H <= carrier G & 
    10.7 -        ((| carrier = H, bin_op = lam x: H. lam y: H. (bin_op G) x y, 
    10.8 -            inverse = lam x: H. (inverse G) x, unit = unit G |) : Group)}"
    10.9 +        ((| carrier = H, bin_op = %x: H. %y: H. (bin_op G) x y, 
   10.10 +            inverse = %x: H. (inverse G) x, unit = unit G |) : Group)}"
   10.11  
   10.12  syntax
   10.13    "@SG"  :: "['a set, 'a grouptype] => bool" ("_ <<= _" [51,50]50)
    11.1 --- a/src/HOL/GroupTheory/Homomorphism.ML	Mon Dec 10 20:58:15 2001 +0100
    11.2 +++ b/src/HOL/GroupTheory/Homomorphism.ML	Mon Dec 10 20:59:43 2001 +0100
    11.3 @@ -127,7 +127,7 @@
    11.4  Goal "RingAuto `` {R} ~= {}";
    11.5  by (stac RingAuto_apply 1);
    11.6  by Auto_tac; 
    11.7 -by (res_inst_tac [("x","lam y: (R.<cr>). y")] exI 1);
    11.8 +by (res_inst_tac [("x","%y: (R.<cr>). y")] exI 1);
    11.9  by (auto_tac (claset(), simpset() addsimps [inj_on_def])); 
   11.10  by (asm_full_simp_tac (simpset() addsimps [RingHom_def, restrictI, 
   11.11       R_binop_def, symmetric (rmult_def), rplus_closed, rmult_closed]) 1);
   11.12 @@ -234,7 +234,7 @@
   11.13  "[| ?R2 \\<in> Ring; group_of ?R2 \\<in> Group |]
   11.14     ==> (| carrier = RingAuto `` {?R2},
   11.15            bin_op =
   11.16 -            lam x:RingAuto `` {?R2}.
   11.17 +            %x:RingAuto `` {?R2}.
   11.18                 restrict ((BijGroup (?R2 .<cr>) .<f>) x) (RingAuto `` {?R2}),
   11.19            inverse = restrict (BijGroup (?R2 .<cr>) .<inv>) (RingAuto `` {?R2}),
   11.20            unit = BijGroup (?R2 .<cr>) .<e> |) \\<in> Group" *)
   11.21 @@ -249,9 +249,9 @@
   11.22  qed "R_Group";
   11.23  
   11.24  Goal "R \\<in> Ring ==> (| carrier = RingAuto `` {R},\
   11.25 -\          bin_op =  lam x:RingAuto `` {R}. lam y: RingAuto `` {R}.\
   11.26 +\          bin_op =  %x:RingAuto `` {R}. %y: RingAuto `` {R}.\
   11.27  \                             (BijGroup (R.<cr>) .<f>) x y ,\
   11.28 -\          inverse = lam x: RingAuto `` {R}. (BijGroup (R.<cr>) .<inv>) x,\
   11.29 +\          inverse = %x: RingAuto `` {R}. (BijGroup (R.<cr>) .<inv>) x,\
   11.30  \          unit = BijGroup (R.<cr>) .<e> |) \\<in> Group";
   11.31  by (rtac (R_Group RSN (2, RingAuto_are_Group)) 1);
   11.32  by (assume_tac 1);
   11.33 @@ -261,7 +261,7 @@
   11.34  (* "?R \\<in> Ring
   11.35     ==> (| carrier = RingAuto `` {?R},
   11.36            bin_op =
   11.37 -            lam x:RingAuto `` {?R}.
   11.38 +            %x:RingAuto `` {?R}.
   11.39                 restrict ((BijGroup (?R .<cr>) .<f>) x) (RingAuto `` {?R}),
   11.40            inverse = restrict (BijGroup (?R .<cr>) .<inv>) (RingAuto `` {?R}),
   11.41            unit = BijGroup (?R .<cr>) .<e> |) \\<in> Group" *)
    12.1 --- a/src/HOL/GroupTheory/PiSets.ML	Mon Dec 10 20:58:15 2001 +0100
    12.2 +++ b/src/HOL/GroupTheory/PiSets.ML	Mon Dec 10 20:59:43 2001 +0100
    12.3 @@ -34,7 +34,7 @@
    12.4  qed "inj_PiBij";
    12.5  
    12.6  
    12.7 -Goal "x \\<in> Graph A B \\<Longrightarrow> (lam a:A. SOME y. (a, y) \\<in> x) \\<in> Pi A B";
    12.8 +Goal "x \\<in> Graph A B \\<Longrightarrow> (%a:A. SOME y. (a, y) \\<in> x) \\<in> Pi A B";
    12.9  by (rtac restrictI 1);
   12.10  by (res_inst_tac [("P", "%xa. (a, xa)\\<in>x")] ex1E 1);
   12.11   by (force_tac (claset(), simpset() addsimps [Graph_def]) 1);
   12.12 @@ -51,7 +51,7 @@
   12.13  by (rtac subsetI 1);
   12.14  by (rtac image_eqI 1); 
   12.15  by (etac in_Graph_imp_in_Pi 2); 
   12.16 -(* x = PiBij A B (lam a:A. @ y. (a, y)\\<in>x) *)
   12.17 +(* x = PiBij A B (%a:A. @ y. (a, y)\\<in>x) *)
   12.18  by (asm_simp_tac (simpset() addsimps [in_Graph_imp_in_Pi, PiBij_def]) 1);
   12.19  by (auto_tac (claset(), simpset() addsimps [some1_equality, Graph_def])); 
   12.20  by (fast_tac (claset() addIs [someI2]) 1);
    13.1 --- a/src/HOL/GroupTheory/PiSets.thy	Mon Dec 10 20:58:15 2001 +0100
    13.2 +++ b/src/HOL/GroupTheory/PiSets.thy	Mon Dec 10 20:59:43 2001 +0100
    13.3 @@ -10,7 +10,7 @@
    13.4  constdefs
    13.5  (* bijection between Pi_sig and Pi_=> *)
    13.6    PiBij :: "['a set, 'a => 'b set, 'a => 'b] => ('a * 'b) set"
    13.7 -    "PiBij A B == lam f: Pi A B. {(x, y). x: A & y = f x}"
    13.8 +    "PiBij A B == %f: Pi A B. {(x, y). x: A & y = f x}"
    13.9  
   13.10    Graph ::  "['a set, 'a => 'b set] => ('a * 'b) set set"
   13.11     "Graph A B == {f. f \\<in> Pow(Sigma A B) & (\\<forall>x\\<in>A. \\<exists>!y. (x, y) \\<in> f)}"
    14.1 --- a/src/HOL/GroupTheory/Ring.thy	Mon Dec 10 20:58:15 2001 +0100
    14.2 +++ b/src/HOL/GroupTheory/Ring.thy	Mon Dec 10 20:59:43 2001 +0100
    14.3 @@ -42,7 +42,7 @@
    14.4  
    14.5  constdefs
    14.6    group_of :: "'a ringtype => 'a grouptype"
    14.7 -   "group_of == lam R: Ring. (| carrier = (R.<cr>), bin_op = (R.<f>),
    14.8 +   "group_of == %R: Ring. (| carrier = (R.<cr>), bin_op = (R.<f>),
    14.9  			        inverse = (R.<inv>), unit = (R.<e>) |)"
   14.10  
   14.11  locale ring = group +
    15.1 --- a/src/HOL/GroupTheory/RingConstr.thy	Mon Dec 10 20:58:15 2001 +0100
    15.2 +++ b/src/HOL/GroupTheory/RingConstr.thy	Mon Dec 10 20:59:43 2001 +0100
    15.3 @@ -11,7 +11,7 @@
    15.4  constdefs
    15.5    ring_of :: "['a grouptype, 'a semigrouptype] => 'a ringtype"
    15.6    "ring_of ==
    15.7 -     lam G: AbelianGroup. lam S: {M. M \\<in> Semigroup & (M.<cr>) = (G.<cr>)}.
    15.8 +     %G: AbelianGroup. %S: {M. M \\<in> Semigroup & (M.<cr>) = (G.<cr>)}.
    15.9                     (| carrier = (G.<cr>), bin_op = (G.<f>), 
   15.10                        inverse = (G.<inv>), unit = (G.<e>), Rmult = (S.<f>) |)"
   15.11  
   15.12 @@ -27,8 +27,8 @@
   15.13  	     ((R.<m>) ((R.<f>) y z) x = (R.<f>) ((R.<m>) y x) ((R.<m>) z x)))}"
   15.14  
   15.15    ring_from :: "['a grouptype, 'a semigrouptype] => 'a ringtype"
   15.16 -  "ring_from == lam G: AbelianGroup. 
   15.17 -     lam S: {M. M \\<in> Semigroup & (M.<cr>) = (G.<cr>) &
   15.18 +  "ring_from == %G: AbelianGroup. 
   15.19 +     %S: {M. M \\<in> Semigroup & (M.<cr>) = (G.<cr>) &
   15.20                  distr_l (G.<cr>) (M.<f>) (G.<f>) &
   15.21  	        distr_r (G.<cr>) (M.<f>) (G.<f>)}.
   15.22              (| carrier = (G.<cr>), bin_op = (G.<f>), 
    16.1 --- a/src/HOL/GroupTheory/Sylow.ML	Mon Dec 10 20:58:15 2001 +0100
    16.2 +++ b/src/HOL/GroupTheory/Sylow.ML	Mon Dec 10 20:59:43 2001 +0100
    16.3 @@ -86,7 +86,7 @@
    16.4  
    16.5  Goal "\\<exists>f \\<in> H\\<rightarrow>M1. inj_on f H";
    16.6  by (rtac (exists_x_in_M1 RS exE) 1);
    16.7 -by (res_inst_tac [("x", "lam z: H. x ## z")] bexI 1);
    16.8 +by (res_inst_tac [("x", "%z: H. x ## z")] bexI 1);
    16.9  by (rtac restrictI 2);
   16.10  by (asm_full_simp_tac (simpset() addsimps [H_def]) 2); 
   16.11  by (Clarify_tac 2);
   16.12 @@ -230,7 +230,7 @@
   16.13  val M_elem_map_carrier = M_elem_map RS someI_ex RS conjunct1;
   16.14  val M_elem_map_eq = M_elem_map RS someI_ex RS conjunct2;
   16.15  
   16.16 -Goal "(lam x:M. H #> (SOME g. g \\<in> carrier G & M1 #> g = x)) \\<in> M \\<rightarrow> {* H *}";
   16.17 +Goal "(%x:M. H #> (SOME g. g \\<in> carrier G & M1 #> g = x)) \\<in> M \\<rightarrow> {* H *}";
   16.18  by (rtac (setrcosI RS restrictI) 1);
   16.19  by (rtac (H_is_SG RS subgroup_imp_subset) 1);
   16.20  by (etac M_elem_map_carrier 1);
   16.21 @@ -265,7 +265,7 @@
   16.22  val H_elem_map_carrier = H_elem_map RS someI_ex RS conjunct1;
   16.23  val H_elem_map_eq = H_elem_map RS someI_ex RS conjunct2;
   16.24  
   16.25 -Goal "(lam C:{*H*}. M1 #> (@g. g \\<in> (G .<cr>) \\<and> H #> g = C)) \\<in> {* H *} \\<rightarrow> M";
   16.26 +Goal "(%C:{*H*}. M1 #> (@g. g \\<in> (G .<cr>) \\<and> H #> g = C)) \\<in> {* H *} \\<rightarrow> M";
   16.27  by (simp_tac (simpset() addsimps [setrcos_eq]) 1);
   16.28  by (deepen_tac (claset() addIs [someI2] 
   16.29              addSIs [restrictI, RelM_equiv, M_in_quot,
    17.1 --- a/src/HOL/Hilbert_Choice_lemmas.ML	Mon Dec 10 20:58:15 2001 +0100
    17.2 +++ b/src/HOL/Hilbert_Choice_lemmas.ML	Mon Dec 10 20:59:43 2001 +0100
    17.3 @@ -212,7 +212,7 @@
    17.4  
    17.5  section "Inverse of a PI-function (restricted domain)";
    17.6  
    17.7 -Goalw [Inv_def] "f ` A = B ==> (lam x: B. (Inv A f) x) : B funcset A";
    17.8 +Goalw [Inv_def] "f ` A = B ==> (%x:B. (Inv A f) x) : B funcset A";
    17.9  by (fast_tac (claset() addIs [restrict_in_funcset, someI2]) 1);
   17.10  qed "Inv_funcset";
   17.11  
   17.12 @@ -237,7 +237,7 @@
   17.13  qed "inj_on_Inv";
   17.14  
   17.15  Goal "[| inj_on f A;  f ` A = B |] \
   17.16 -\     ==> compose A (lam y:B. (Inv A f) y) f = (lam x: A. x)";
   17.17 +\     ==> compose A (%y:B. (Inv A f) y) f = (%x:A. x)";
   17.18  by (asm_simp_tac (simpset() addsimps [compose_def]) 1);
   17.19  by (rtac restrict_ext 1); 
   17.20  by Auto_tac; 
    18.1 --- a/src/HOL/ex/Tarski.ML	Mon Dec 10 20:58:15 2001 +0100
    18.2 +++ b/src/HOL/ex/Tarski.ML	Mon Dec 10 20:59:43 2001 +0100
    18.3 @@ -384,7 +384,7 @@
    18.4  by (afs [thm "P_def", fix_def] 1);
    18.5  qed "fixfE2";
    18.6  
    18.7 -Goal "[| A <= B; x \\<in> fix (lam y: A. f y) A |] ==> x \\<in> fix f B";
    18.8 +Goal "[| A <= B; x \\<in> fix (%y: A. f y) A |] ==> x \\<in> fix f B";
    18.9  by (forward_tac [export fixfE2] 1);
   18.10  by (dtac ((export fixfE1) RS subsetD) 1);
   18.11  by (asm_full_simp_tac (simpset() addsimps [fix_def, subsetD]) 1); 
   18.12 @@ -774,12 +774,12 @@
   18.13  by (afs [thm "intY1_def",interval_def, intY1_elem] 1);
   18.14  qed "intY1_f_closed";
   18.15  
   18.16 -Goal "(lam x: intY1. f x) \\<in> intY1 funcset intY1";
   18.17 +Goal "(%x: intY1. f x) \\<in> intY1 funcset intY1";
   18.18  by (rtac restrictI 1);
   18.19  by (etac intY1_f_closed 1); 
   18.20  qed "intY1_func";
   18.21  
   18.22 -Goal "monotone (lam x: intY1. f x) intY1 (induced intY1 r)";
   18.23 +Goal "monotone (%x: intY1. f x) intY1 (induced intY1 r)";
   18.24  by (auto_tac (claset(), 
   18.25              simpset() addsimps [monotone_def, induced_def, intY1_f_closed])); 
   18.26  by (blast_tac (claset() addIs [intY1_elem, CLF_E2 RS monotoneE]) 1); 
   18.27 @@ -817,7 +817,7 @@
   18.28  qed "z_in_interval";
   18.29  
   18.30  Goal "[| z \\<in> P; \\<forall>y\\<in>Y. (y, z) \\<in> induced P r |]\
   18.31 -\     ==> ((lam x: intY1. f x) z, z) \\<in> induced intY1 r";
   18.32 +\     ==> ((%x: intY1. f x) z, z) \\<in> induced intY1 r";
   18.33  by (afs [induced_def, intY1_f_closed, z_in_interval] 1);
   18.34  by (afs [fixfE2, fixfE1 RS subsetD, CompleteLatticeE11 RS reflE] 1);
   18.35  qed "f'z_in_int_rel";
    19.1 --- a/src/HOL/ex/Tarski.thy	Mon Dec 10 20:58:15 2001 +0100
    19.2 +++ b/src/HOL/ex/Tarski.thy	Mon Dec 10 20:59:43 2001 +0100
    19.3 @@ -135,7 +135,7 @@
    19.4    Y_ss "Y <= P"
    19.5  defines
    19.6    intY1_def "intY1 == interval r (lub Y cl) (Top cl)"
    19.7 -  v_def "v == glb {x. ((lam x: intY1. f x) x, x): induced intY1 r & x: intY1}
    19.8 +  v_def "v == glb {x. ((%x: intY1. f x) x, x): induced intY1 r & x: intY1}
    19.9  	          (| pset=intY1, order=induced intY1 r|)"
   19.10  
   19.11  end