separate theory for index structures
authorhaftmann
Mon Feb 08 10:36:02 2010 +0100 (2010-02-08)
changeset 3502922aab1c5e5a8
parent 35028 108662d50512
child 35030 f2f1e50bf65d
separate theory for index structures
NEWS
src/HOL/IsaMakefile
src/HOL/Library/Library.thy
src/HOL/Library/Structure_Syntax.thy
     1.1 --- a/NEWS	Fri Feb 05 14:33:50 2010 +0100
     1.2 +++ b/NEWS	Mon Feb 08 10:36:02 2010 +0100
     1.3 @@ -60,6 +60,9 @@
     1.4  
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 +* Index syntax for structures must be imported explicitly from library
     1.8 +theory Structure_Syntax.  INCOMPATIBILITY.
     1.9 +
    1.10  * new theory Algebras.thy contains generic algebraic structures and
    1.11  generic algebraic operations.  INCOMPATIBILTY: constants zero, one,
    1.12  plus, minus, uminus, times, inverse, divide, abs, sgn, less_eq and less
     2.1 --- a/src/HOL/IsaMakefile	Fri Feb 05 14:33:50 2010 +0100
     2.2 +++ b/src/HOL/IsaMakefile	Mon Feb 08 10:36:02 2010 +0100
     2.3 @@ -394,7 +394,7 @@
     2.4    Library/Library/document/root.tex Library/Library/document/root.bib	\
     2.5    Library/Transitive_Closure_Table.thy Library/While_Combinator.thy	\
     2.6    Library/Product_ord.thy Library/Char_nat.thy				\
     2.7 -  Library/Char_ord.thy Library/Option_ord.thy				\
     2.8 +  Library/Structure_Syntax.thy						\
     2.9    Library/Sublist_Order.thy Library/List_lexord.thy			\
    2.10    Library/Coinductive_List.thy Library/AssocList.thy			\
    2.11    Library/Formal_Power_Series.thy Library/Binomial.thy			\
     3.1 --- a/src/HOL/Library/Library.thy	Fri Feb 05 14:33:50 2010 +0100
     3.2 +++ b/src/HOL/Library/Library.thy	Mon Feb 08 10:36:02 2010 +0100
     3.3 @@ -50,6 +50,7 @@
     3.4    RBT
     3.5    SML_Quickcheck
     3.6    State_Monad
     3.7 +  Structure_Syntax
     3.8    Sum_Of_Squares
     3.9    Transitive_Closure_Table
    3.10    Univ_Poly
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Library/Structure_Syntax.thy	Mon Feb 08 10:36:02 2010 +0100
     4.3 @@ -0,0 +1,14 @@
     4.4 +(* Author: Florian Haftmann, TU Muenchen *)
     4.5 +
     4.6 +header {* Index syntax for structures *}
     4.7 +
     4.8 +theory Structure_Syntax
     4.9 +imports Pure
    4.10 +begin
    4.11 +
    4.12 +syntax
    4.13 +  "_index1"  :: index    ("\<^sub>1")
    4.14 +translations
    4.15 +  (index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>"
    4.16 +
    4.17 +end