Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/GroupTheory/RingConstr.thy
changeset 12459 6978ab7cac64
parent 11448 aa519e0cc050 
--- 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>),
isabelle