equal
deleted
inserted
replaced
70 consts NTH :: "[real, 'a list] => 'a" |
70 consts NTH :: "[real, 'a list] => 'a" |
71 axiomatization where |
71 axiomatization where |
72 NTH_NIL: "NTH 1 (x # xs) = x" and |
72 NTH_NIL: "NTH 1 (x # xs) = x" and |
73 NTH_CONS: (*NO primrec, fun ..*)"1 < n ==> NTH n (x # xs) = NTH (n + -1) xs" |
73 NTH_CONS: (*NO primrec, fun ..*)"1 < n ==> NTH n (x # xs) = NTH (n + -1) xs" |
74 |
74 |
75 (* redefine together with identifiers (still) required for KEStore ..*) |
75 (* redefine together with identifiers (still) required for Know_Store ..*) |
76 axiomatization where |
76 axiomatization where |
77 hd_thm: "hd (x # xs) = x" |
77 hd_thm: "hd (x # xs) = x" |
78 |
78 |
79 axiomatization where |
79 axiomatization where |
80 tl_Nil: "tl [] = []" and |
80 tl_Nil: "tl [] = []" and |