equal
deleted
inserted
replaced
38 eresolve_tac prems 1, eresolve_tac prems 1]); |
38 eresolve_tac prems 1, eresolve_tac prems 1]); |
39 |
39 |
40 val set_cs2 = set_cs delrules [ballE] addSEs [BallE]; |
40 val set_cs2 = set_cs delrules [ballE] addSEs [BallE]; |
41 |
41 |
42 Addsimps [Let_def]; |
42 Addsimps [Let_def]; |
43 Addsimps [surjective_pairing RS sym]; |
|
44 |
43 |
45 (* To HOL.ML *) |
44 (* To HOL.ML *) |
46 |
45 |
47 val ex1_Eps_eq = prove_goal HOL.thy "\\<lbrakk> \\<exists>!x. P x; P y \\<rbrakk> \\<Longrightarrow> Eps P = y" |
46 val ex1_Eps_eq = prove_goal HOL.thy "\\<lbrakk> \\<exists>!x. P x; P y \\<rbrakk> \\<Longrightarrow> Eps P = y" |
48 (fn prems => [ |
47 (fn prems => [ |