equal
deleted
inserted
replaced
33 "!!a. (!x y. a ~= f x y) ==> a ~: (UN x y. {f x y})"]; |
33 "!!a. (!x y. a ~= f x y) ==> a ~: (UN x y. {f x y})"]; |
34 |
34 |
35 |
35 |
36 (* Arithmetic *) |
36 (* Arithmetic *) |
37 |
37 |
38 goal Arithmetic.thy "!!x. 0<x ==> (x-1 = y) = (x = Suc(y))"; |
38 goal NatArith.thy "!!x. 0<x ==> (x-1 = y) = (x = Suc(y))"; |
39 by (asm_simp_tac (simpset() addsimps [diff_Suc] addsplits [nat.split]) 1); |
39 by (asm_simp_tac (simpset() addsimps [diff_Suc] addsplits [nat.split]) 1); |
40 qed "pred_suc"; |
40 qed "pred_suc"; |
41 |
41 |
42 |
42 |
43 Addsimps (hd_append :: set_lemmas); |
43 Addsimps (hd_append :: set_lemmas); |