Command atp_minimize uses the naive linear algorithm now
because the binary chop one had turned out to be a little bit suboptimal.
Internally the binary chop one is still available.
(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
*)
(*Verifying security protocols using UNITY*)
no_document use_thy "../Auth/Public";
(*Basic meta-theory*)
use_thy "UNITY_Main";
(*Examples*)
use_thy "UNITY_Examples";