Removes an inconsistent definition from Library.thy ,
so that the lexical order is the standard order for lists.
The prefix order is not built any more.
(* tactic script -- single steps *)
Goal "EX S. S ~: range (f :: 'a => 'a set)";
by (rtac exI 1);
by (rtac notI 1);
by (etac rangeE 1);
by (etac equalityCE 1);
by (dtac CollectD 1);
by (contr_tac 1);
by (swap_res_tac [CollectI] 1);
by (assume_tac 1);
qed "";
(* tactic script -- automatic *)
Goal "EX S. S ~: range (f :: 'a => 'a set)";
by (Best_tac 1);
qed "";