| changeset 9969 | 4753185f1dd2 |
| parent 9608 | a50dcf0475ad |
| child 10234 | c8726d4ee89a |
--- a/src/HOL/equalities.ML Fri Sep 15 11:34:46 2000 +0200 +++ b/src/HOL/equalities.ML Fri Sep 15 12:39:57 2000 +0200 @@ -104,8 +104,9 @@ by (Blast_tac 1); qed "mk_disjoint_insert"; -bind_thm ("insert_Collect", prove_goal (the_context ()) - "insert a (Collect P) = {u. u ~= a --> P u}" (K [Auto_tac])); +Goal "insert a (Collect P) = {u. u ~= a --> P u}"; +by Auto_tac; +qed "insert_Collect"; Goal "u: A ==> (UN x:A. insert a (B x)) = insert a (UN x:A. B x)"; by (Blast_tac 1);