--- a/NEWS Fri Feb 05 14:33:50 2010 +0100
+++ b/NEWS Mon Feb 08 10:36:02 2010 +0100
@@ -60,6 +60,9 @@
INCOMPATIBILITY.
+* Index syntax for structures must be imported explicitly from library
+theory Structure_Syntax. INCOMPATIBILITY.
+
* new theory Algebras.thy contains generic algebraic structures and
generic algebraic operations. INCOMPATIBILTY: constants zero, one,
plus, minus, uminus, times, inverse, divide, abs, sgn, less_eq and less
--- a/src/HOL/IsaMakefile Fri Feb 05 14:33:50 2010 +0100
+++ b/src/HOL/IsaMakefile Mon Feb 08 10:36:02 2010 +0100
@@ -394,7 +394,7 @@
Library/Library/document/root.tex Library/Library/document/root.bib \
Library/Transitive_Closure_Table.thy Library/While_Combinator.thy \
Library/Product_ord.thy Library/Char_nat.thy \
- Library/Char_ord.thy Library/Option_ord.thy \
+ Library/Structure_Syntax.thy \
Library/Sublist_Order.thy Library/List_lexord.thy \
Library/Coinductive_List.thy Library/AssocList.thy \
Library/Formal_Power_Series.thy Library/Binomial.thy \
--- a/src/HOL/Library/Library.thy Fri Feb 05 14:33:50 2010 +0100
+++ b/src/HOL/Library/Library.thy Mon Feb 08 10:36:02 2010 +0100
@@ -50,6 +50,7 @@
RBT
SML_Quickcheck
State_Monad
+ Structure_Syntax
Sum_Of_Squares
Transitive_Closure_Table
Univ_Poly
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Structure_Syntax.thy Mon Feb 08 10:36:02 2010 +0100
@@ -0,0 +1,14 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* Index syntax for structures *}
+
+theory Structure_Syntax
+imports Pure
+begin
+
+syntax
+ "_index1" :: index ("\<^sub>1")
+translations
+ (index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>"
+
+end