--- a/src/HOL/Fun.ML Mon Dec 10 20:58:15 2001 +0100
+++ b/src/HOL/Fun.ML Mon Dec 10 20:59:43 2001 +0100
@@ -445,25 +445,25 @@
qed "inj_on_compose";
-(*** restrict / lam ***)
+(*** restrict / bounded abstraction ***)
-Goal "f`A <= B ==> (lam x: A. f x) : A funcset B";
+Goal "f`A <= B ==> (%x:A. f x) : A funcset B";
by (auto_tac (claset(),
simpset() addsimps [restrict_def, Pi_def]));
qed "restrict_in_funcset";
val prems = Goalw [restrict_def, Pi_def]
- "(!!x. x: A ==> f x: B x) ==> (lam x: A. f x) : Pi A B";
+ "(!!x. x: A ==> f x: B x) ==> (%x:A. f x) : Pi A B";
by (asm_simp_tac (simpset() addsimps prems) 1);
qed "restrictI";
-Goal "(lam y: A. f y) x = (if x : A then f x else arbitrary)";
+Goal "(%y:A. f y) x = (if x : A then f x else arbitrary)";
by (asm_simp_tac (simpset() addsimps [restrict_def]) 1);
qed "restrict_apply";
Addsimps [restrict_apply];
val prems = Goal
- "(!!x. x: A ==> f x = g x) ==> (lam x: A. f x) = (lam x: A. g x)";
+ "(!!x. x: A ==> f x = g x) ==> (%x:A. f x) = (%x:A. g x)";
by (rtac ext 1);
by (auto_tac (claset(),
simpset() addsimps prems@[restrict_def, Pi_def]));
@@ -474,12 +474,12 @@
qed "inj_on_restrict_eq";
-Goal "f : A funcset B ==> compose A (lam y:B. y) f = f";
+Goal "f : A funcset B ==> compose A (%y:B. y) f = f";
by (rtac ext 1);
by (auto_tac (claset(), simpset() addsimps [compose_def, Pi_def]));
qed "Id_compose";
-Goal "g : A funcset B ==> compose A g (lam x:A. x) = g";
+Goal "g : A funcset B ==> compose A g (%x:A. x) = g";
by (rtac ext 1);
by (auto_tac (claset(), simpset() addsimps [compose_def, Pi_def]));
qed "compose_Id";
--- a/src/HOL/Fun.thy Mon Dec 10 20:58:15 2001 +0100
+++ b/src/HOL/Fun.thy Mon Dec 10 20:59:43 2001 +0100
@@ -75,9 +75,11 @@
syntax
"@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3PI _:_./ _)" 10)
funcset :: "['a set, 'b set] => ('a => 'b) set" (infixr 60)
- "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a => 'b)" ("(3lam _:_./ _)" 10)
+ "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a => 'b)" ("(3%_:_./ _)" [0, 0, 3] 3)
+syntax (xsymbols)
+ "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a => 'b)" ("(3\\<lambda>_\<in>_./ _)" [0, 0, 3] 3)
- (*Giving funcset the arrow syntax (namely ->) clashes with other theories*)
+ (*Giving funcset an arrow syntax (-> or =>) clashes with many existing theories*)
syntax (xsymbols)
"@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\\<Pi> _\\<in>_./ _)" 10)
@@ -85,11 +87,11 @@
translations
"PI x:A. B" => "Pi A (%x. B)"
"A funcset B" => "Pi A (_K B)"
- "lam x:A. f" == "restrict (%x. f) A"
+ "%x:A. f" == "restrict (%x. f) A"
constdefs
compose :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)"
- "compose A g f == lam x : A. g(f x)"
+ "compose A g f == %x:A. g (f x)"
end
--- a/src/HOL/GroupTheory/Bij.ML Mon Dec 10 20:58:15 2001 +0100
+++ b/src/HOL/GroupTheory/Bij.ML Mon Dec 10 20:59:43 2001 +0100
@@ -46,11 +46,11 @@
(* restrict (Inv S f) S *)
-Goal "f \\<in> B ==> (lam x: S. (inv' f) x) \\<in> B";
+Goal "f \\<in> B ==> (%x:S. (inv' f) x) \\<in> B";
by (rtac BijI 1);
-(* 1. (lam x: S. (inv' f) x): S \\<rightarrow> S *)
+(* 1. (%x:S. (inv' f) x): S \\<rightarrow> S *)
by (afs [Inv_funcset] 1);
-(* 2. (lam x: S. (inv' f) x) ` S = S *)
+(* 2. (%x:S. (inv' f) x) ` S = S *)
by (asm_full_simp_tac (simpset() addsimps [inv_def]) 1);
by (rtac equalityI 1);
(* 2. <= *)
@@ -73,7 +73,7 @@
by (auto_tac (claset(), simpset() addsimps [funcsetI, inj_on_def]));
qed "restrict_id_Bij";
-Goal "f \\<in> B ==> (lam g: B. lam x: S. (inv' g) x) f = (lam x: S. (inv' f) x)";
+Goal "f \\<in> B ==> (%g:B. %x:S. (inv' g) x) f = (%x:S. (inv' f) x)";
by (Asm_full_simp_tac 1);
qed "eval_restrict_Inv";
@@ -95,7 +95,7 @@
val BG_def = thm "BG_def";
-Goal "[| x\\<in>B; y\\<in>B |] ==> (lam g: B. lam f: B. g o' f) x y = x o' y";
+Goal "[| x\\<in>B; y\\<in>B |] ==> (%g:B. %f:B. g o' f) x y = x o' y";
by (Asm_full_simp_tac 1);
qed "eval_restrict_comp2";
@@ -106,11 +106,11 @@
by (afs [BijGroup_def] 1);
qed "BG_carrier";
-Goal "bin_op BG == lam g: B. lam f: B. g o' f";
+Goal "bin_op BG == %g:B. %f:B. g o' f";
by (afs [BijGroup_def] 1);
qed "BG_bin_op";
-Goal "inverse BG == lam f: B. lam x: S. (inv' f) x";
+Goal "inverse BG == %f:B. %x:S. (inv' f) x";
by (afs [BijGroup_def] 1);
qed "BG_inverse";
@@ -126,7 +126,7 @@
Delsimps [B_def, BG_def, o'_def, inv'_def, e'_def];
-Goal "(lam g: B. lam f: B. g o' f) \\<in> B \\<rightarrow> B \\<rightarrow> B";
+Goal "(%g:B. %f:B. g o' f) \\<in> B \\<rightarrow> B \\<rightarrow> B";
by (simp_tac (simpset() addsimps [funcsetI, compose_Bij]) 1);
qed "restrict_compose_Bij";
--- a/src/HOL/GroupTheory/Bij.thy Mon Dec 10 20:58:15 2001 +0100
+++ b/src/HOL/GroupTheory/Bij.thy Mon Dec 10 20:59:43 2001 +0100
@@ -16,9 +16,9 @@
constdefs
BijGroup :: "'a set => (('a => 'a) grouptype)"
"BijGroup S == (| carrier = Bij S,
- bin_op = lam g: Bij S. lam f: Bij S. compose S g f,
- inverse = lam f: Bij S. lam x: S. (Inv S f) x,
- unit = lam x: S. x |)"
+ bin_op = %g: Bij S. %f: Bij S. compose S g f,
+ inverse = %f: Bij S. %x: S. (Inv S f) x,
+ unit = %x: S. x |)"
locale bij =
fixes
@@ -31,7 +31,7 @@
B_def "B == Bij S"
o'_def "g o' f == compose S g f"
inv'_def "inv' f == Inv S f"
- e'_def "e' == (lam x: S. x)"
+ e'_def "e' == (%x: S. x)"
locale bijgroup = bij +
fixes
--- a/src/HOL/GroupTheory/DirProd.ML Mon Dec 10 20:58:15 2001 +0100
+++ b/src/HOL/GroupTheory/DirProd.ML Mon Dec 10 20:59:43 2001 +0100
@@ -22,11 +22,11 @@
qed "P_carrier";
Goal "(P.<f>) = \
-\ (lam (x, x'): (P.<cr>). lam (y, y'): (P.<cr>). ( x ## y, x' ##' y'))";
+\ (%(x, x'): (P.<cr>). %(y, y'): (P.<cr>). ( x ## y, x' ##' y'))";
by (afs [ProdGroup_def, binop_def, binop'_def] 1);
qed "P_bin_op";
-Goal "(P.<inv>) = (lam (x, y): (P.<cr>). (i x, i' y))";
+Goal "(P.<inv>) = (%(x, y): (P.<cr>). (i x, i' y))";
by (afs [ProdGroup_def, inv_def, inv'_def] 1);
qed "P_inverse";
@@ -35,9 +35,9 @@
qed "P_unit";
Goal "P = (| carrier = P.<cr>, \
-\ bin_op = (lam (x, x'): (P.<cr>). lam (y, y'): (P.<cr>).\
+\ bin_op = (%(x, x'): (P.<cr>). %(y, y'): (P.<cr>).\
\ (x ## y, x' ##' y')), \
-\ inverse = (lam (x, y): (P.<cr>). (i x, i' y)), \
+\ inverse = (%(x, y): (P.<cr>). (i x, i' y)), \
\ unit = P.<e> |)";
by (afs [ProdGroup_def, P_carrier, P_bin_op, P_inverse, P_unit] 1);
by (afs [binop_def, binop'_def, inv_def, inv'_def] 1);
--- a/src/HOL/GroupTheory/DirProd.thy Mon Dec 10 20:58:15 2001 +0100
+++ b/src/HOL/GroupTheory/DirProd.thy Mon Dec 10 20:59:43 2001 +0100
@@ -12,12 +12,12 @@
ProdGroup :: "(['a grouptype, 'b grouptype] => ('a * 'b) grouptype)"
defs
- ProdGroup_def "ProdGroup == lam G: Group. lam G': Group.
+ ProdGroup_def "ProdGroup == %G: Group. %G': Group.
(| carrier = ((G.<cr>) \\<times> (G'.<cr>)),
- bin_op = (lam (x, x'): ((G.<cr>) \\<times> (G'.<cr>)).
- lam (y, y'): ((G.<cr>) \\<times> (G'.<cr>)).
+ bin_op = (%(x, x'): ((G.<cr>) \\<times> (G'.<cr>)).
+ %(y, y'): ((G.<cr>) \\<times> (G'.<cr>)).
((G.<f>) x y,(G'.<f>) x' y')),
- inverse = (lam (x, y): ((G.<cr>) \\<times> (G'.<cr>)). ((G.<inv>) x, (G'.<inv>) y)),
+ inverse = (%(x, y): ((G.<cr>) \\<times> (G'.<cr>)). ((G.<inv>) x, (G'.<inv>) y)),
unit = ((G.<e>),(G'.<e>)) |)"
syntax
--- a/src/HOL/GroupTheory/FactGroup.ML Mon Dec 10 20:58:15 2001 +0100
+++ b/src/HOL/GroupTheory/FactGroup.ML Mon Dec 10 20:59:43 2001 +0100
@@ -18,11 +18,11 @@
by (afs [FactGroup_def] 1);
qed "F_carrier";
-Goal "bin_op F = (lam X: {* H *}. lam Y: {* H *}. X <#> Y) ";
+Goal "bin_op F = (%X: {* H *}. %Y: {* H *}. X <#> Y) ";
by (afs [FactGroup_def, setprod_def] 1);
qed "F_bin_op";
-Goal "inverse F = (lam X: {* H *}. I(X))";
+Goal "inverse F = (%X: {* H *}. I(X))";
by (afs [FactGroup_def, setinv_def] 1);
qed "F_inverse";
@@ -31,8 +31,8 @@
qed "F_unit";
Goal "F = (| carrier = {* H *}, \
-\ bin_op = (lam X: {* H *}. lam Y: {* H *}. X <#> Y), \
-\ inverse = (lam X: {* H *}. I(X)), unit = H |)";
+\ bin_op = (%X: {* H *}. %Y: {* H *}. X <#> Y), \
+\ inverse = (%X: {* H *}. I(X)), unit = H |)";
by (afs [FactGroup_def, F_carrier, F_bin_op, F_inverse, F_unit] 1);
by (auto_tac (claset() addSIs [restrict_ext],
simpset() addsimps [set_prod_def, setprod_def, setinv_def]));
--- a/src/HOL/GroupTheory/FactGroup.thy Mon Dec 10 20:58:15 2001 +0100
+++ b/src/HOL/GroupTheory/FactGroup.thy Mon Dec 10 20:59:43 2001 +0100
@@ -12,10 +12,10 @@
FactGroup :: "(['a grouptype, 'a set] => ('a set) grouptype)"
"FactGroup ==
- lam G: Group. lam H: {H. H <| G}.
+ %G: Group. %H: {H. H <| G}.
(| carrier = set_r_cos G H,
- bin_op = (lam X: set_r_cos G H. lam Y: set_r_cos G H. set_prod G X Y),
- inverse = (lam X: set_r_cos G H. set_inv G X),
+ bin_op = (%X: set_r_cos G H. %Y: set_r_cos G H. set_prod G X Y),
+ inverse = (%X: set_r_cos G H. set_inv G X),
unit = H |)"
syntax
--- a/src/HOL/GroupTheory/Group.ML Mon Dec 10 20:58:15 2001 +0100
+++ b/src/HOL/GroupTheory/Group.ML Mon Dec 10 20:59:43 2001 +0100
@@ -155,8 +155,8 @@
val SubgroupI = export subgroupI;
Goal "H <<= G ==> \
-\ (|carrier = H, bin_op = lam x:H. lam y:H. x ## y, \
-\ inverse = lam x:H. i(x), unit = e|)\\<in>Group";
+\ (|carrier = H, bin_op = %x:H. %y:H. x ## y, \
+\ inverse = %x:H. i(x), unit = e|)\\<in>Group";
by (afs [subgroup_def, binop_def, inv_def, e_def] 1);
qed "subgroupE2";
val SubgroupE2 = export subgroupE2;
--- a/src/HOL/GroupTheory/Group.thy Mon Dec 10 20:58:15 2001 +0100
+++ b/src/HOL/GroupTheory/Group.thy Mon Dec 10 20:59:43 2001 +0100
@@ -60,8 +60,8 @@
defs
subgroup_def "subgroup == SIGMA G: Group. {H. H <= carrier G &
- ((| carrier = H, bin_op = lam x: H. lam y: H. (bin_op G) x y,
- inverse = lam x: H. (inverse G) x, unit = unit G |) : Group)}"
+ ((| carrier = H, bin_op = %x: H. %y: H. (bin_op G) x y,
+ inverse = %x: H. (inverse G) x, unit = unit G |) : Group)}"
syntax
"@SG" :: "['a set, 'a grouptype] => bool" ("_ <<= _" [51,50]50)
--- a/src/HOL/GroupTheory/Homomorphism.ML Mon Dec 10 20:58:15 2001 +0100
+++ b/src/HOL/GroupTheory/Homomorphism.ML Mon Dec 10 20:59:43 2001 +0100
@@ -127,7 +127,7 @@
Goal "RingAuto `` {R} ~= {}";
by (stac RingAuto_apply 1);
by Auto_tac;
-by (res_inst_tac [("x","lam y: (R.<cr>). y")] exI 1);
+by (res_inst_tac [("x","%y: (R.<cr>). y")] exI 1);
by (auto_tac (claset(), simpset() addsimps [inj_on_def]));
by (asm_full_simp_tac (simpset() addsimps [RingHom_def, restrictI,
R_binop_def, symmetric (rmult_def), rplus_closed, rmult_closed]) 1);
@@ -234,7 +234,7 @@
"[| ?R2 \\<in> Ring; group_of ?R2 \\<in> Group |]
==> (| carrier = RingAuto `` {?R2},
bin_op =
- lam x:RingAuto `` {?R2}.
+ %x:RingAuto `` {?R2}.
restrict ((BijGroup (?R2 .<cr>) .<f>) x) (RingAuto `` {?R2}),
inverse = restrict (BijGroup (?R2 .<cr>) .<inv>) (RingAuto `` {?R2}),
unit = BijGroup (?R2 .<cr>) .<e> |) \\<in> Group" *)
@@ -249,9 +249,9 @@
qed "R_Group";
Goal "R \\<in> Ring ==> (| carrier = RingAuto `` {R},\
-\ bin_op = lam x:RingAuto `` {R}. lam y: RingAuto `` {R}.\
+\ bin_op = %x:RingAuto `` {R}. %y: RingAuto `` {R}.\
\ (BijGroup (R.<cr>) .<f>) x y ,\
-\ inverse = lam x: RingAuto `` {R}. (BijGroup (R.<cr>) .<inv>) x,\
+\ inverse = %x: RingAuto `` {R}. (BijGroup (R.<cr>) .<inv>) x,\
\ unit = BijGroup (R.<cr>) .<e> |) \\<in> Group";
by (rtac (R_Group RSN (2, RingAuto_are_Group)) 1);
by (assume_tac 1);
@@ -261,7 +261,7 @@
(* "?R \\<in> Ring
==> (| carrier = RingAuto `` {?R},
bin_op =
- lam x:RingAuto `` {?R}.
+ %x:RingAuto `` {?R}.
restrict ((BijGroup (?R .<cr>) .<f>) x) (RingAuto `` {?R}),
inverse = restrict (BijGroup (?R .<cr>) .<inv>) (RingAuto `` {?R}),
unit = BijGroup (?R .<cr>) .<e> |) \\<in> Group" *)
--- a/src/HOL/GroupTheory/PiSets.ML Mon Dec 10 20:58:15 2001 +0100
+++ b/src/HOL/GroupTheory/PiSets.ML Mon Dec 10 20:59:43 2001 +0100
@@ -34,7 +34,7 @@
qed "inj_PiBij";
-Goal "x \\<in> Graph A B \\<Longrightarrow> (lam a:A. SOME y. (a, y) \\<in> x) \\<in> Pi A B";
+Goal "x \\<in> Graph A B \\<Longrightarrow> (%a:A. SOME y. (a, y) \\<in> x) \\<in> Pi A B";
by (rtac restrictI 1);
by (res_inst_tac [("P", "%xa. (a, xa)\\<in>x")] ex1E 1);
by (force_tac (claset(), simpset() addsimps [Graph_def]) 1);
@@ -51,7 +51,7 @@
by (rtac subsetI 1);
by (rtac image_eqI 1);
by (etac in_Graph_imp_in_Pi 2);
-(* x = PiBij A B (lam a:A. @ y. (a, y)\\<in>x) *)
+(* x = PiBij A B (%a:A. @ y. (a, y)\\<in>x) *)
by (asm_simp_tac (simpset() addsimps [in_Graph_imp_in_Pi, PiBij_def]) 1);
by (auto_tac (claset(), simpset() addsimps [some1_equality, Graph_def]));
by (fast_tac (claset() addIs [someI2]) 1);
--- a/src/HOL/GroupTheory/PiSets.thy Mon Dec 10 20:58:15 2001 +0100
+++ b/src/HOL/GroupTheory/PiSets.thy Mon Dec 10 20:59:43 2001 +0100
@@ -10,7 +10,7 @@
constdefs
(* bijection between Pi_sig and Pi_=> *)
PiBij :: "['a set, 'a => 'b set, 'a => 'b] => ('a * 'b) set"
- "PiBij A B == lam f: Pi A B. {(x, y). x: A & y = f x}"
+ "PiBij A B == %f: Pi A B. {(x, y). x: A & y = f x}"
Graph :: "['a set, 'a => 'b set] => ('a * 'b) set set"
"Graph A B == {f. f \\<in> Pow(Sigma A B) & (\\<forall>x\\<in>A. \\<exists>!y. (x, y) \\<in> f)}"
--- a/src/HOL/GroupTheory/Ring.thy Mon Dec 10 20:58:15 2001 +0100
+++ b/src/HOL/GroupTheory/Ring.thy Mon Dec 10 20:59:43 2001 +0100
@@ -42,7 +42,7 @@
constdefs
group_of :: "'a ringtype => 'a grouptype"
- "group_of == lam R: Ring. (| carrier = (R.<cr>), bin_op = (R.<f>),
+ "group_of == %R: Ring. (| carrier = (R.<cr>), bin_op = (R.<f>),
inverse = (R.<inv>), unit = (R.<e>) |)"
locale ring = group +
--- a/src/HOL/GroupTheory/RingConstr.thy Mon Dec 10 20:58:15 2001 +0100
+++ b/src/HOL/GroupTheory/RingConstr.thy Mon Dec 10 20:59:43 2001 +0100
@@ -11,7 +11,7 @@
constdefs
ring_of :: "['a grouptype, 'a semigrouptype] => 'a ringtype"
"ring_of ==
- lam G: AbelianGroup. lam S: {M. M \\<in> Semigroup & (M.<cr>) = (G.<cr>)}.
+ %G: AbelianGroup. %S: {M. M \\<in> Semigroup & (M.<cr>) = (G.<cr>)}.
(| carrier = (G.<cr>), bin_op = (G.<f>),
inverse = (G.<inv>), unit = (G.<e>), Rmult = (S.<f>) |)"
@@ -27,8 +27,8 @@
((R.<m>) ((R.<f>) y z) x = (R.<f>) ((R.<m>) y x) ((R.<m>) z x)))}"
ring_from :: "['a grouptype, 'a semigrouptype] => 'a ringtype"
- "ring_from == lam G: AbelianGroup.
- lam S: {M. M \\<in> Semigroup & (M.<cr>) = (G.<cr>) &
+ "ring_from == %G: AbelianGroup.
+ %S: {M. M \\<in> Semigroup & (M.<cr>) = (G.<cr>) &
distr_l (G.<cr>) (M.<f>) (G.<f>) &
distr_r (G.<cr>) (M.<f>) (G.<f>)}.
(| carrier = (G.<cr>), bin_op = (G.<f>),
--- a/src/HOL/GroupTheory/Sylow.ML Mon Dec 10 20:58:15 2001 +0100
+++ b/src/HOL/GroupTheory/Sylow.ML Mon Dec 10 20:59:43 2001 +0100
@@ -86,7 +86,7 @@
Goal "\\<exists>f \\<in> H\\<rightarrow>M1. inj_on f H";
by (rtac (exists_x_in_M1 RS exE) 1);
-by (res_inst_tac [("x", "lam z: H. x ## z")] bexI 1);
+by (res_inst_tac [("x", "%z: H. x ## z")] bexI 1);
by (rtac restrictI 2);
by (asm_full_simp_tac (simpset() addsimps [H_def]) 2);
by (Clarify_tac 2);
@@ -230,7 +230,7 @@
val M_elem_map_carrier = M_elem_map RS someI_ex RS conjunct1;
val M_elem_map_eq = M_elem_map RS someI_ex RS conjunct2;
-Goal "(lam x:M. H #> (SOME g. g \\<in> carrier G & M1 #> g = x)) \\<in> M \\<rightarrow> {* H *}";
+Goal "(%x:M. H #> (SOME g. g \\<in> carrier G & M1 #> g = x)) \\<in> M \\<rightarrow> {* H *}";
by (rtac (setrcosI RS restrictI) 1);
by (rtac (H_is_SG RS subgroup_imp_subset) 1);
by (etac M_elem_map_carrier 1);
@@ -265,7 +265,7 @@
val H_elem_map_carrier = H_elem_map RS someI_ex RS conjunct1;
val H_elem_map_eq = H_elem_map RS someI_ex RS conjunct2;
-Goal "(lam C:{*H*}. M1 #> (@g. g \\<in> (G .<cr>) \\<and> H #> g = C)) \\<in> {* H *} \\<rightarrow> M";
+Goal "(%C:{*H*}. M1 #> (@g. g \\<in> (G .<cr>) \\<and> H #> g = C)) \\<in> {* H *} \\<rightarrow> M";
by (simp_tac (simpset() addsimps [setrcos_eq]) 1);
by (deepen_tac (claset() addIs [someI2]
addSIs [restrictI, RelM_equiv, M_in_quot,
--- a/src/HOL/Hilbert_Choice_lemmas.ML Mon Dec 10 20:58:15 2001 +0100
+++ b/src/HOL/Hilbert_Choice_lemmas.ML Mon Dec 10 20:59:43 2001 +0100
@@ -212,7 +212,7 @@
section "Inverse of a PI-function (restricted domain)";
-Goalw [Inv_def] "f ` A = B ==> (lam x: B. (Inv A f) x) : B funcset A";
+Goalw [Inv_def] "f ` A = B ==> (%x:B. (Inv A f) x) : B funcset A";
by (fast_tac (claset() addIs [restrict_in_funcset, someI2]) 1);
qed "Inv_funcset";
@@ -237,7 +237,7 @@
qed "inj_on_Inv";
Goal "[| inj_on f A; f ` A = B |] \
-\ ==> compose A (lam y:B. (Inv A f) y) f = (lam x: A. x)";
+\ ==> compose A (%y:B. (Inv A f) y) f = (%x:A. x)";
by (asm_simp_tac (simpset() addsimps [compose_def]) 1);
by (rtac restrict_ext 1);
by Auto_tac;
--- a/src/HOL/ex/Tarski.ML Mon Dec 10 20:58:15 2001 +0100
+++ b/src/HOL/ex/Tarski.ML Mon Dec 10 20:59:43 2001 +0100
@@ -384,7 +384,7 @@
by (afs [thm "P_def", fix_def] 1);
qed "fixfE2";
-Goal "[| A <= B; x \\<in> fix (lam y: A. f y) A |] ==> x \\<in> fix f B";
+Goal "[| A <= B; x \\<in> fix (%y: A. f y) A |] ==> x \\<in> fix f B";
by (forward_tac [export fixfE2] 1);
by (dtac ((export fixfE1) RS subsetD) 1);
by (asm_full_simp_tac (simpset() addsimps [fix_def, subsetD]) 1);
@@ -774,12 +774,12 @@
by (afs [thm "intY1_def",interval_def, intY1_elem] 1);
qed "intY1_f_closed";
-Goal "(lam x: intY1. f x) \\<in> intY1 funcset intY1";
+Goal "(%x: intY1. f x) \\<in> intY1 funcset intY1";
by (rtac restrictI 1);
by (etac intY1_f_closed 1);
qed "intY1_func";
-Goal "monotone (lam x: intY1. f x) intY1 (induced intY1 r)";
+Goal "monotone (%x: intY1. f x) intY1 (induced intY1 r)";
by (auto_tac (claset(),
simpset() addsimps [monotone_def, induced_def, intY1_f_closed]));
by (blast_tac (claset() addIs [intY1_elem, CLF_E2 RS monotoneE]) 1);
@@ -817,7 +817,7 @@
qed "z_in_interval";
Goal "[| z \\<in> P; \\<forall>y\\<in>Y. (y, z) \\<in> induced P r |]\
-\ ==> ((lam x: intY1. f x) z, z) \\<in> induced intY1 r";
+\ ==> ((%x: intY1. f x) z, z) \\<in> induced intY1 r";
by (afs [induced_def, intY1_f_closed, z_in_interval] 1);
by (afs [fixfE2, fixfE1 RS subsetD, CompleteLatticeE11 RS reflE] 1);
qed "f'z_in_int_rel";
--- a/src/HOL/ex/Tarski.thy Mon Dec 10 20:58:15 2001 +0100
+++ b/src/HOL/ex/Tarski.thy Mon Dec 10 20:59:43 2001 +0100
@@ -135,7 +135,7 @@
Y_ss "Y <= P"
defines
intY1_def "intY1 == interval r (lub Y cl) (Top cl)"
- v_def "v == glb {x. ((lam x: intY1. f x) x, x): induced intY1 r & x: intY1}
+ v_def "v == glb {x. ((%x: intY1. f x) x, x): induced intY1 r & x: intY1}
(| pset=intY1, order=induced intY1 r|)"
end