src/HOL/UNITY/ROOT.ML
author wenzelm
Fri Mar 28 19:43:54 2008 +0100 (2008-03-28)
changeset 26462 dac4e2bce00d
parent 24147 edc90be09ac1
child 28529 7ff939586e83
permissions -rw-r--r--
avoid rebinding of existing facts;
paulson@4776
     1
(*  Title:      HOL/UNITY/ROOT
paulson@4776
     2
    ID:         $Id$
paulson@4776
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@4776
     4
    Copyright   1998  University of Cambridge
paulson@4776
     5
paulson@4776
     6
Root file for UNITY proofs.
paulson@4776
     7
*)
paulson@4776
     8
wenzelm@24147
     9
(*Verifying security protocols using UNITY*)
wenzelm@24147
    10
no_document use_thy "../Auth/Public";
paulson@11193
    11
wenzelm@24147
    12
use_thys [
wenzelm@24147
    13
  (*Basic meta-theory*)
wenzelm@24147
    14
  "UNITY_Main",
paulson@11193
    15
wenzelm@24147
    16
  (*Simple examples: no composition*)
wenzelm@24147
    17
  "Simple/Deadlock",
wenzelm@24147
    18
  "Simple/Common",
wenzelm@24147
    19
  "Simple/Network",
wenzelm@24147
    20
  "Simple/Token",
wenzelm@24147
    21
  "Simple/Channel",
wenzelm@24147
    22
  "Simple/Lift",
wenzelm@24147
    23
  "Simple/Mutex",
wenzelm@24147
    24
  "Simple/Reach",
wenzelm@24147
    25
  "Simple/Reachability",
paulson@11193
    26
wenzelm@24147
    27
  (*Verifying security protocols using UNITY*)
wenzelm@24147
    28
  "Simple/NSP_Bad",
paulson@9112
    29
wenzelm@24147
    30
  (*Example of composition*)
wenzelm@24147
    31
  "Comp/Handshake",
paulson@10782
    32
wenzelm@24147
    33
  (*Universal properties examples*)
wenzelm@24147
    34
  "Comp/Counter",
wenzelm@24147
    35
  "Comp/Counterc",
wenzelm@24147
    36
  "Comp/Priority",
wenzelm@24147
    37
wenzelm@24147
    38
  "Comp/TimerArray",
wenzelm@24147
    39
wenzelm@24147
    40
  (*obsolete*)
wenzelm@24147
    41
  "ELT"
wenzelm@24147
    42
];
paulson@9112
    43
paulson@13790
    44
(*Allocator example*)
wenzelm@21633
    45
(* FIXME some parts no longer work -- had been commented out for a long time *)
wenzelm@21633
    46
setmp quick_and_dirty true
wenzelm@24147
    47
  use_thy "Comp/Alloc";
paulson@8987
    48
wenzelm@24147
    49
use_thys ["Comp/AllocImpl", "Comp/Client"];