| changeset 5858 | beddc19c107a |
| parent 5069 | 3ea049f7979d |
| child 6162 | 484adda70b65 |
--- a/src/HOL/Quot/PER.ML Fri Nov 13 13:29:50 1998 +0100 +++ b/src/HOL/Quot/PER.ML Fri Nov 13 13:41:53 1998 +0100 @@ -12,7 +12,7 @@ (* Witness that quot is not empty *) Goal "?z:{s.? r.!y. y:s=y===r}"; -fr CollectI; +br CollectI 1; by (res_inst_tac [("x","x")] exI 1); by (rtac allI 1); by (rtac mem_Collect_eq 1);