1.1 --- a/src/Tools/isac/ProgLang/ListC.thy	Sun Aug 28 12:32:57 2016 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/ListC.thy	Thu Sep 08 13:28:36 2016 +0200
     1.3 @@ -39,19 +39,19 @@
     1.4  subsection {* Type 'xlist' for Lucas-Interpretation *}
     1.5  (*TODO: ask for shorter deliminters in xlist *)
     1.6  datatype 'a xlist =
     1.7 -    XNil    ("[|| ||]")
     1.8 +    XNil    ("{|| ||}")
     1.9    | XCons 'a  "'a xlist"    (infixr "@#" 65)
    1.10  
    1.11  syntax
    1.12    -- {* list Enumeration *}
    1.13 -  "_xlist" :: "args => 'a xlist"    ("[||(_)||]")
    1.14 +  "_xlist" :: "args => 'a xlist"    ("{|| (_) ||}")
    1.15  
    1.16  translations
    1.17 -  "[||x, xs||]" == "x@#[||xs||]"
    1.18 -  "[||x||]" == "x@#[|| ||]"
    1.19 +  "{||x, xs||}" == "x@#{||xs||}"
    1.20 +  "{||x||}" == "x@#{|| ||}"
    1.21  
    1.22 -term "[|| ||]"
    1.23 -term "[||1,2,3||]"
    1.24 +term "{|| ||}"
    1.25 +term "{||1,2,3||}"
    1.26  
    1.27  subsection {* Functions for 'xlist' *}
    1.28  (* TODO: 
    1.29 @@ -62,7 +62,7 @@
    1.30  *)
    1.31  
    1.32  primrec xfoldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a xlist \<Rightarrow> 'b \<Rightarrow> 'b" where
    1.33 -xfoldr_Nil:  "xfoldr f [|| ||] = id" |
    1.34 +xfoldr_Nil:  "xfoldr f {|| ||} = id" |
    1.35  xfoldr_Cons: "xfoldr f (x @# xs) = f x \<circ> xfoldr f xs"
    1.36  
    1.37  primrec LENGTH   :: "'a list => real"