src/HOL/HOL.thy

--- a/src/HOL/HOL.thy	Mon Aug 05 14:35:33 2002 +0200
+++ b/src/HOL/HOL.thy	Mon Aug 05 21:16:36 2002 +0200
@@ -163,6 +163,11 @@
   uminus        :: "['a::minus] => 'a"              ("- _" [81] 80)
   *             :: "['a::times, 'a] => 'a"          (infixl 70)
 
+syntax
+  "_index1"  :: index    ("\<^sub>1")
+translations
+  (index) "\<^sub>1" == "_index 1"
+
 local
 
 typed_print_translation {*