Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
special syntax for index "1" (plain numeral hidden by "1" symbol in HOL);
authorwenzelm
Mon, 05 Aug 2002 21:16:36 +0200
changeset 13456 42601eb7553f
parent 13455 f88a91ff8ac6
child 13457 7ddcf40a80b3
special syntax for index "1" (plain numeral hidden by "1" symbol in HOL);
src/HOL/HOL.thy file | annotate | diff | comparison | revisions 
--- 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 {*
isabelle