# HG changeset patch
# User wenzelm
# Date 1008014383 -3600
# Node ID 6978ab7cac641235ff11767f25c6279c9e157e62
# Parent  a8c219e76ae03f5aa1577b6eb5f359324e76739c
bounded abstraction now uses syntax "%" / "\<lambda>" instead of "lam";

diff -r a8c219e76ae0 -r 6978ab7cac64 src/HOL/Fun.ML
--- 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";
diff -r a8c219e76ae0 -r 6978ab7cac64 src/HOL/Fun.thy
--- 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
 
diff -r a8c219e76ae0 -r 6978ab7cac64 src/HOL/GroupTheory/Bij.ML
--- 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";
 
diff -r a8c219e76ae0 -r 6978ab7cac64 src/HOL/GroupTheory/Bij.thy
--- 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 
diff -r a8c219e76ae0 -r 6978ab7cac64 src/HOL/GroupTheory/DirProd.ML
--- 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);
diff -r a8c219e76ae0 -r 6978ab7cac64 src/HOL/GroupTheory/DirProd.thy
--- 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
diff -r a8c219e76ae0 -r 6978ab7cac64 src/HOL/GroupTheory/FactGroup.ML
--- 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])); 
diff -r a8c219e76ae0 -r 6978ab7cac64 src/HOL/GroupTheory/FactGroup.thy
--- 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
diff -r a8c219e76ae0 -r 6978ab7cac64 src/HOL/GroupTheory/Group.ML
--- 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;
diff -r a8c219e76ae0 -r 6978ab7cac64 src/HOL/GroupTheory/Group.thy
--- 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)
diff -r a8c219e76ae0 -r 6978ab7cac64 src/HOL/GroupTheory/Homomorphism.ML
--- 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" *)
diff -r a8c219e76ae0 -r 6978ab7cac64 src/HOL/GroupTheory/PiSets.ML
--- 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);
diff -r a8c219e76ae0 -r 6978ab7cac64 src/HOL/GroupTheory/PiSets.thy
--- 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)}"
diff -r a8c219e76ae0 -r 6978ab7cac64 src/HOL/GroupTheory/Ring.thy
--- 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 +
diff -r a8c219e76ae0 -r 6978ab7cac64 src/HOL/GroupTheory/RingConstr.thy
--- 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>), 
diff -r a8c219e76ae0 -r 6978ab7cac64 src/HOL/GroupTheory/Sylow.ML
--- 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,
diff -r a8c219e76ae0 -r 6978ab7cac64 src/HOL/Hilbert_Choice_lemmas.ML
--- 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; 
diff -r a8c219e76ae0 -r 6978ab7cac64 src/HOL/ex/Tarski.ML
--- 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";
diff -r a8c219e76ae0 -r 6978ab7cac64 src/HOL/ex/Tarski.thy
--- 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