src/HOL/HOL.thy
changeset 13456 42601eb7553f
parent 13438 527811f00c56
child 13550 5a176b8dda84
     1.1 --- a/src/HOL/HOL.thy	Mon Aug 05 14:35:33 2002 +0200
     1.2 +++ b/src/HOL/HOL.thy	Mon Aug 05 21:16:36 2002 +0200
     1.3 @@ -163,6 +163,11 @@
     1.4    uminus        :: "['a::minus] => 'a"              ("- _" [81] 80)
     1.5    *             :: "['a::times, 'a] => 'a"          (infixl 70)
     1.6  
     1.7 +syntax
     1.8 +  "_index1"  :: index    ("\<^sub>1")
     1.9 +translations
    1.10 +  (index) "\<^sub>1" == "_index 1"
    1.11 +
    1.12  local
    1.13  
    1.14  typed_print_translation {*