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