src/HOL/UNITY/ROOT.ML

try to avoid races again (cf. 8c37cb84065f and fd3a36e48b09);

(*  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 [
  (*Basic meta-theory*)
  "UNITY_Main",

  (*Simple examples: no composition*)
  "Simple/Deadlock",
  "Simple/Common",
  "Simple/Network",
  "Simple/Token",
  "Simple/Channel",
  "Simple/Lift",
  "Simple/Mutex",
  "Simple/Reach",
  "Simple/Reachability",

  (*Verifying security protocols using UNITY*)
  "Simple/NSP_Bad",

  (*Example of composition*)
  "Comp/Handshake",

  (*Universal properties examples*)
  "Comp/Counter",
  "Comp/Counterc",
  "Comp/Priority",

  "Comp/TimerArray",
  "Comp/Progress",

  "Comp/Alloc",
  "Comp/AllocImpl",
  "Comp/Client",

  (*obsolete*)
  "ELT"
];