153 |
153 |
154 (* FIXME: put other record thms here, or declare as "no_atp" *) |
154 (* FIXME: put other record thms here, or declare as "no_atp" *) |
155 fun multi_base_blacklist ctxt ho_atp = |
155 fun multi_base_blacklist ctxt ho_atp = |
156 ["defs", "select_defs", "update_defs", "split", "splits", "split_asm", |
156 ["defs", "select_defs", "update_defs", "split", "splits", "split_asm", |
157 "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong", |
157 "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong", |
158 "weak_case_cong", "nibble_pair_of_char_simps", "nibble.simps", |
158 "weak_case_cong", "nat_of_char_simps", "nibble.simps", |
159 "nibble.distinct"] |
159 "nibble.distinct"] |
160 |> not (ho_atp orelse (Config.get ctxt instantiate_inducts)) ? |
160 |> not (ho_atp orelse (Config.get ctxt instantiate_inducts)) ? |
161 append ["induct", "inducts"] |
161 append ["induct", "inducts"] |
162 |> map (prefix Long_Name.separator) |
162 |> map (prefix Long_Name.separator) |
163 |
163 |