src/HOL/UNITY/ROOT.ML

use command_def

(*  Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1998  University of Cambridge
*)

(*Verifying security protocols using UNITY*)
no_document use_thys ["../Auth/Public"];

use_thys [
  "UNITY_Main",     (*Basic meta-theory*)
  "UNITY_Examples"  (*Examples*)
];