1.1 --- a/src/Tools/isac/ProgLang/Atools.thy	Thu Aug 23 09:42:19 2018 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/Atools.thy	Thu Aug 23 11:01:03 2018 +0200
     1.3 @@ -521,7 +521,7 @@
     1.4  open Term;
     1.5  
     1.6  in
     1.7 -fun termlessI (_: Rule.subst) uv = Term_Ord.termless uv;
     1.8 +fun termlessI (_: Rule.subst) uv = LibraryC.termless uv;
     1.9  fun term_ordI (_: Rule.subst) uv = Term_Ord.term_ord uv;
    1.10  end;
    1.11  
    1.12 @@ -701,4 +701,7 @@
    1.13  setup {* KEStore_Elems.add_rlss
    1.14    [("list_rls", (Context.theory_name @{theory}, LTool.prep_rls @{theory} list_rls))] *}
    1.15  
    1.16 +ML \<open>
    1.17 +\<close> ML \<open>
    1.18 +\<close> 
    1.19  end

     2.1 --- a/src/Tools/isac/ProgLang/ListC.thy	Thu Aug 23 09:42:19 2018 +0200
     2.2 +++ b/src/Tools/isac/ProgLang/ListC.thy	Thu Aug 23 11:01:03 2018 +0200
     2.3 @@ -40,13 +40,14 @@
     2.4  *}
     2.5  
     2.6  subsection {* Type 'xlist' for Lucas-Interpretation *}
     2.7 -(*TODO: ask for shorter deliminters in xlist *)
     2.8 -datatype 'a xlist =
     2.9 -    XNil    ("{|| ||}")
    2.10 -  | XCons 'a  "'a xlist"    (infixr "@#" 65)
    2.11 +(* cp fom ~~/src/HOL/List.thy
    2.12 +   TODO: ask for shorter deliminters in xlist *)
    2.13 +datatype  'a xlist =
    2.14 +    XNil  ("{|| ||}")
    2.15 +  | XCons (xhd: 'a)  (xtl: "'a xlist")  (infixr "@#" 65)
    2.16  
    2.17  syntax
    2.18 -  -- {* list Enumeration *}
    2.19 +   \<comment> \<open>list Enumeration\<close>
    2.20    "_xlist" :: "args => 'a xlist"    ("{|| (_) ||}")
    2.21  
    2.22  translations
    2.23 @@ -78,6 +79,7 @@
    2.24  NTH_NIL: "NTH 1 (x # xs) = x" and
    2.25  NTH_CONS: (*NO primrec, fun ..*)"1 < n ==> NTH n (x # xs) = NTH (n + -1) xs"
    2.26  
    2.27 +(* redefine together with identifiers (still) required for KEStore ..*)
    2.28  axiomatization where
    2.29  hd_thm:	"hd (x # xs) = x"
    2.30  

     3.1 --- a/src/Tools/isac/ProgLang/termC.sml	Thu Aug 23 09:42:19 2018 +0200
     3.2 +++ b/src/Tools/isac/ProgLang/termC.sml	Thu Aug 23 11:01:03 2018 +0200
     3.3 @@ -188,7 +188,7 @@
     3.4  fun str_of_int n = 
     3.5    if n < 0 then "-" ^ ((string_of_int o abs) n)
     3.6    else string_of_int n;
     3.7 -val int_of_str = Thy_Output.integer;
     3.8 +val int_of_str = Value.parse_int;
     3.9  fun int_of_str_opt str = 
    3.10    let
    3.11      val ss = Symbol.explode str

     4.1 --- a/src/Tools/isac/library.sml	Thu Aug 23 09:42:19 2018 +0200
     4.2 +++ b/src/Tools/isac/library.sml	Thu Aug 23 11:01:03 2018 +0200
     4.3 @@ -71,6 +71,7 @@
     4.4      val takelast: int * 'a list -> 'a list
     4.5      val takerest: int * 'a list -> 'a list
     4.6      val takewhile: 'a list -> ('a -> bool) -> 'a list -> 'a list
     4.7 +    val termless: term * term -> bool
     4.8      val thd3: 'a * 'b * 'c -> 'c
     4.9      val triple2pair: 'a * 'b * 'c -> 'a * 'b
    4.10      val ~~~ : 'a list * 'b list -> ('a * 'b) list
    4.11 @@ -291,4 +292,6 @@
    4.12  val it = "[(bdv,x),(err,#0)]" : string*)
    4.13  (*\\\------------------------------>>>  term ----------------------------------------------///*)
    4.14  
    4.15 +fun termless tu = (Term_Ord.term_ord tu = LESS);
    4.16 +
    4.17  end; (*struct*) open LibraryC