| changeset 4605 | 579e0ef2df6b |
| parent 4477 | b3e5857d8d99 |
| child 4609 | b435c5a320b0 |
--- a/src/HOL/equalities.ML Fri Feb 06 11:18:29 1998 +0100 +++ b/src/HOL/equalities.ML Fri Feb 06 18:55:18 1998 +0100 @@ -45,6 +45,9 @@ goal thy "!!a. a:A ==> insert a A = A"; by (Blast_tac 1); qed "insert_absorb"; +(* Addsimps [insert_absorb] causes recursive (ie quadtratic) calls + in case of nested inserts! +*) goal thy "insert x (insert x A) = insert x A"; by (Blast_tac 1);