1.1 --- a/src/Tools/isac/ProgLang/ListC.thy	Thu Aug 23 09:42:19 2018 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/ListC.thy	Thu Aug 23 11:01:03 2018 +0200
     1.3 @@ -40,13 +40,14 @@
     1.4  *}
     1.5  
     1.6  subsection {* Type 'xlist' for Lucas-Interpretation *}
     1.7 -(*TODO: ask for shorter deliminters in xlist *)
     1.8 -datatype 'a xlist =
     1.9 -    XNil    ("{|| ||}")
    1.10 -  | XCons 'a  "'a xlist"    (infixr "@#" 65)
    1.11 +(* cp fom ~~/src/HOL/List.thy
    1.12 +   TODO: ask for shorter deliminters in xlist *)
    1.13 +datatype  'a xlist =
    1.14 +    XNil  ("{|| ||}")
    1.15 +  | XCons (xhd: 'a)  (xtl: "'a xlist")  (infixr "@#" 65)
    1.16  
    1.17  syntax
    1.18 -  -- {* list Enumeration *}
    1.19 +   \<comment> \<open>list Enumeration\<close>
    1.20    "_xlist" :: "args => 'a xlist"    ("{|| (_) ||}")
    1.21  
    1.22  translations
    1.23 @@ -78,6 +79,7 @@
    1.24  NTH_NIL: "NTH 1 (x # xs) = x" and
    1.25  NTH_CONS: (*NO primrec, fun ..*)"1 < n ==> NTH n (x # xs) = NTH (n + -1) xs"
    1.26  
    1.27 +(* redefine together with identifiers (still) required for KEStore ..*)
    1.28  axiomatization where
    1.29  hd_thm:	"hd (x # xs) = x"
    1.30