src/HOL/Library/Structure_Syntax.thy
author haftmann
Mon, 08 Feb 2010 14:22:22 +0100
changeset 35043 07dbdf60d5ad
parent 35029 22aab1c5e5a8
permissions -rw-r--r--
dropped accidental duplication of "lin" prefix from cs. 108662d50512

(* 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