changeset 44433 | 9fbee4aab115 |
parent 44348 | 40101794c52f |
child 44848 | f4d0b060c7ca |
--- a/src/HOL/Groups.thy Tue Aug 23 19:49:21 2011 +0200 +++ b/src/HOL/Groups.thy Mon Aug 22 23:39:05 2011 +0200 @@ -103,11 +103,6 @@ hide_const (open) zero one -syntax - "_index1" :: index ("\<^sub>1") -translations - (index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>" - lemma Let_0 [simp]: "Let 0 f = f 0" unfolding Let_def ..