# HG changeset patch
# User haftmann
# Date 1265621762 -3600
# Node ID 22aab1c5e5a83438d6b9e0c632356926a7f861b3
# Parent  108662d5051240fec0a5cceef30fd0b06fc1a565
separate theory for index structures

diff -r 108662d50512 -r 22aab1c5e5a8 NEWS
--- 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
diff -r 108662d50512 -r 22aab1c5e5a8 src/HOL/IsaMakefile
--- 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			\
diff -r 108662d50512 -r 22aab1c5e5a8 src/HOL/Library/Library.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
diff -r 108662d50512 -r 22aab1c5e5a8 src/HOL/Library/Structure_Syntax.thy
--- /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