Now with Andy Gordon's treatment of freshness to replace newN/K

Deleted the redundant theorem subset_empty_iff (subset_empty exists already)

Added the prlim command

New miniscoping rules for the bounded quantifiers and UN/INT operators

Got rid of Alls in List.
Added Ball_insert and Ball_Un in equalities.ML.

Got rid of Alls in favour of !x:set_of_list

binary oprations and relations;
nat;

added termless parameter;
added simplification procedures;

added term order;

improved error msg;