equal
deleted
inserted
replaced
270 |
270 |
271 (** Rewrite rules for boolean case-splitting: faster than |
271 (** Rewrite rules for boolean case-splitting: faster than |
272 addsplits[split_if] |
272 addsplits[split_if] |
273 **) |
273 **) |
274 |
274 |
275 bind_thm ("split_if_eq1", read_instantiate [("P", "%x. x = ?b")] split_if); |
275 bind_thm ("split_if_eq1", inst "P" "%x. x = ?b" split_if); |
276 bind_thm ("split_if_eq2", read_instantiate [("P", "%x. ?a = x")] split_if); |
276 bind_thm ("split_if_eq2", inst "P" "%x. ?a = x" split_if); |
277 |
277 |
278 bind_thm ("split_if_mem1", read_instantiate [("P", "%x. x : ?b")] split_if); |
278 bind_thm ("split_if_mem1", inst "P" "%x. x : ?b" split_if); |
279 bind_thm ("split_if_mem2", read_instantiate [("P", "%x. ?a : x")] split_if); |
279 bind_thm ("split_if_mem2", inst "P" "%x. ?a : x" split_if); |
280 |
280 |
281 val split_ifs = [split_if_eq1, split_if_eq2, |
281 val split_ifs = [split_if_eq1, split_if_eq2, |
282 split_if_mem1, split_if_mem2]; |
282 split_if_mem1, split_if_mem2]; |
283 |
283 |
284 (*Logically equivalent to split_if_mem2*) |
284 (*Logically equivalent to split_if_mem2*) |