equal
deleted
inserted
replaced
104 REPEAT_DETERM o resolve_tac |
104 REPEAT_DETERM o resolve_tac |
105 [chain_iterate, ch2ch_Rep_CFunR, ch2ch_Rep_CFunL]; |
105 [chain_iterate, ch2ch_Rep_CFunR, ch2ch_Rep_CFunL]; |
106 |
106 |
107 (* ----- general proofs ----------------------------------------------------- *) |
107 (* ----- general proofs ----------------------------------------------------- *) |
108 |
108 |
109 val all2E = prove_goal HOL.thy "[| !x y . P x y; P x y ==> R |] ==> R" |
109 val all2E = @{lemma "!x y . P x y ==> (P x y ==> R) ==> R" by simp} |
110 (fn prems =>[ |
110 |
111 resolve_tac prems 1, |
111 val dist_eqI = @{lemma "!!x::'a::po. ~ x << y ==> x ~= y" by (blast dest!: antisym_less_inverse)} |
112 cut_facts_tac prems 1, |
|
113 fast_tac HOL_cs 1]); |
|
114 |
|
115 val dist_eqI = prove_goal (the_context ()) "!!x::'a::po. ~ x << y ==> x ~= y" |
|
116 (fn prems => |
|
117 [blast_tac (@{claset} addDs [antisym_less_inverse]) 1]); |
|
118 |
112 |
119 in |
113 in |
120 |
114 |
121 fun theorems (((dname, _), cons) : eq, eqs : eq list) thy = |
115 fun theorems (((dname, _), cons) : eq, eqs : eq list) thy = |
122 let |
116 let |