src/HOL/UNITY/ROOT.ML
author wenzelm
Mon Mar 16 18:24:30 2009 +0100 (2009-03-16)
changeset 30549 d2d7874648bd
parent 28866 30cd9d89a0fb
child 32624 3dec57ec3473
permissions -rw-r--r--
simplified method setup;
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@28866
    39
  "Comp/Progress",
wenzelm@24147
    40
wenzelm@24147
    41
  (*obsolete*)
wenzelm@24147
    42
  "ELT"
wenzelm@24147
    43
];
paulson@9112
    44
paulson@13790
    45
(*Allocator example*)
wenzelm@21633
    46
(* FIXME some parts no longer work -- had been commented out for a long time *)
wenzelm@28529
    47
setmp_noncritical quick_and_dirty true
wenzelm@24147
    48
  use_thy "Comp/Alloc";
paulson@8987
    49
wenzelm@24147
    50
use_thys ["Comp/AllocImpl", "Comp/Client"];