src/HOL/UNITY/UNITY_Examples.thy
author hoelzl
Thu Sep 02 10:14:32 2010 +0200 (2010-09-02)
changeset 39072 1030b1a166ef
parent 32624 3dec57ec3473
permissions -rw-r--r--
Add lessThan_Suc_eq_insert_0
     1 (*  Author:     Lawrence C Paulson Cambridge University Computer Laboratory
     2     Copyright   1998  University of Cambridge
     3 *)
     4 
     5 header {* Various examples for UNITY *}
     6 
     7 theory UNITY_Examples
     8 imports
     9   UNITY_Main
    10 
    11   (*Simple examples: no composition*)
    12   "Simple/Deadlock"
    13   "Simple/Common"
    14   "Simple/Network"
    15   "Simple/Token"
    16   "Simple/Channel"
    17   "Simple/Lift"
    18   "Simple/Mutex"
    19   "Simple/Reach"
    20   "Simple/Reachability"
    21 
    22   (*Verifying security protocols using UNITY*)
    23   "Simple/NSP_Bad"
    24 
    25   (*Example of composition*)
    26   "Comp/Handshake"
    27 
    28   (*Universal properties examples*)
    29   "Comp/Counter"
    30   "Comp/Counterc"
    31   "Comp/Priority"
    32 
    33   "Comp/TimerArray"
    34   "Comp/Progress"
    35 
    36   "Comp/Alloc"
    37   "Comp/AllocImpl"
    38   "Comp/Client"
    39 
    40   (*obsolete*)
    41   "ELT"
    42 
    43 begin
    44 
    45 end