| changeset 10834 | a7897aebbffc |
| parent 9969 | 4753185f1dd2 |
| child 11395 | 2eeaa1077b73 |
--- a/src/HOL/ex/PiSets.ML Tue Jan 09 15:29:17 2001 +0100 +++ b/src/HOL/ex/PiSets.ML Tue Jan 09 15:32:27 2001 +0100 @@ -38,7 +38,7 @@ -Goal "PiBij A B `` (Pi A B) = Graph A B"; +Goal "PiBij A B ` (Pi A B) = Graph A B"; by (rtac equalityI 1); by (force_tac (claset(), simpset() addsimps [image_def,PiBij_in_Graph]) 1); by (rtac subsetI 1);