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