1.1 --- a/src/Tools/isac/ProgLang/ListC.thy	Sun Apr 19 11:07:02 2020 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/ListC.thy	Sun Apr 19 12:22:37 2020 +0200
     1.3 @@ -72,7 +72,7 @@
     1.4  NTH_NIL: "NTH 1 (x # xs) = x" and
     1.5  NTH_CONS: (*NO primrec, fun ..*)"1 < n ==> NTH n (x # xs) = NTH (n + -1) xs"
     1.6  
     1.7 -(* redefine together with identifiers (still) required for KEStore ..*)
     1.8 +(* redefine together with identifiers (still) required for Know_Store ..*)
     1.9  axiomatization where
    1.10  hd_thm:	"hd (x # xs) = x"
    1.11