src/HOL/UNITY/ROOT.ML
author kuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802 b16f976db515
parent 41892 2386fb64feaf
permissions -rw-r--r--
Quotient_Info stores only relation maps
     1 (*  Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2     Copyright   1998  University of Cambridge
     3 *)
     4 
     5 (*Verifying security protocols using UNITY*)
     6 no_document use_thys ["../Auth/Public"];
     7 
     8 use_thys [
     9   (*Basic meta-theory*)
    10   "UNITY_Main",
    11 
    12   (*Simple examples: no composition*)
    13   "Simple/Deadlock",
    14   "Simple/Common",
    15   "Simple/Network",
    16   "Simple/Token",
    17   "Simple/Channel",
    18   "Simple/Lift",
    19   "Simple/Mutex",
    20   "Simple/Reach",
    21   "Simple/Reachability",
    22 
    23   (*Verifying security protocols using UNITY*)
    24   "Simple/NSP_Bad",
    25 
    26   (*Example of composition*)
    27   "Comp/Handshake",
    28 
    29   (*Universal properties examples*)
    30   "Comp/Counter",
    31   "Comp/Counterc",
    32   "Comp/Priority",
    33 
    34   "Comp/TimerArray",
    35   "Comp/Progress",
    36 
    37   "Comp/Alloc",
    38   "Comp/AllocImpl",
    39   "Comp/Client",
    40 
    41   (*obsolete*)
    42   "ELT"
    43 ];