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.
_index1: accomodate improved indexed syntax;
authorwenzelm
Sat, 01 May 2004 21:59:12 +0200
changeset 14690 f61ea8bfa81e
parent 14689 eafb91eda9e8
child 14691 e1eedc8cad37
_index1: accomodate improved indexed syntax;
src/HOL/HOL.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/HOL.thy	Sat May 01 21:58:52 2004 +0200
+++ b/src/HOL/HOL.thy	Sat May 01 21:59:12 2004 +0200
@@ -181,7 +181,7 @@
 syntax
   "_index1"  :: index    ("\<^sub>1")
 translations
-  (index) "\<^sub>1" == "_index 1"
+  (index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>"
 
 local
isabelle