equal
deleted
inserted
replaced
128 |
128 |
129 axiomatization where |
129 axiomatization where |
130 remdups_Nil: "remdups [] = []" and |
130 remdups_Nil: "remdups [] = []" and |
131 remdups_Cons: "remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)" |
131 remdups_Cons: "remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)" |
132 |
132 |
|
133 consts lastI :: "'a list \<Rightarrow> 'a" |
|
134 axiomatization where |
|
135 last_thmI: "lastI (x#xs) = (if xs = [] then x else lastI xs)" |
|
136 |
133 ML\<open>(** rule set for evaluating listexpr in scripts, will be extended in several thys **) |
137 ML\<open>(** rule set for evaluating listexpr in scripts, will be extended in several thys **) |
134 val list_rls = |
138 val list_rls = |
135 Rule.Rls {id = "list_rls", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord), |
139 Rule.Rls {id = "list_rls", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord), |
136 erls = Rule.Erls, srls = Rule.Erls, calc = [], errpatts = [], |
140 erls = Rule.Erls, srls = Rule.Erls, calc = [], errpatts = [], |
137 rules = [Rule.Thm ("refl", TermC.num_str @{thm refl}), (*'a<>b -> FALSE' by fun eval_equal*) |
141 rules = [Rule.Thm ("refl", TermC.num_str @{thm refl}), (*'a<>b -> FALSE' by fun eval_equal*) |