| changeset 18371 | d93fdf00f8a6 |
| parent 17456 | bcf7544875b2 |
| child 18413 | 50c0c118e96d |
--- a/src/CCL/Set.ML Thu Dec 08 20:15:34 2005 +0100 +++ b/src/CCL/Set.ML Thu Dec 08 20:15:41 2005 +0100 @@ -234,7 +234,7 @@ val emptyE = make_elim emptyD; val [prem] = goal (the_context ()) "~ A={} ==> (EX x. x:A)"; -by (rtac (prem RS swap) 1); +by (rtac (prem RS Cla.swap) 1); by (rtac equalityI 1); by (ALLGOALS (fast_tac (FOL_cs addSIs [subsetI] addSEs [emptyD]))); qed "not_emptyD";