# HG changeset patch
# User wenzelm
# Date 1028574996 -7200
# Node ID 42601eb7553fa58a4afe7dabed806589a6cd1242
# Parent  f88a91ff8ac62af9ccf0c094975dfbf3c02d155d
special syntax for index "1" (plain numeral hidden by "1" symbol in HOL);

diff -r f88a91ff8ac6 -r 42601eb7553f 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 {*