src/HOL/UNITY/ROOT.ML
author wenzelm
Wed, 08 Oct 2008 19:20:29 +0200
changeset 28529 7ff939586e83
parent 24147 edc90be09ac1
child 28866 30cd9d89a0fb
permissions -rw-r--r--
setmp_noncritical makes it work with future scheduler;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     1
(*  Title:      HOL/UNITY/ROOT
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     2
    ID:         $Id$
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     4
    Copyright   1998  University of Cambridge
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     5
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     6
Root file for UNITY proofs.
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     7
*)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     8
24147
edc90be09ac1 misc cleanup of ML bindings (for multihreading);
wenzelm
parents: 21633
diff changeset
     9
(*Verifying security protocols using UNITY*)
edc90be09ac1 misc cleanup of ML bindings (for multihreading);
wenzelm
parents: 21633
diff changeset
    10
no_document use_thy "../Auth/Public";
11193
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents: 10782
diff changeset
    11
24147
edc90be09ac1 misc cleanup of ML bindings (for multihreading);
wenzelm
parents: 21633
diff changeset
    12
use_thys [
edc90be09ac1 misc cleanup of ML bindings (for multihreading);
wenzelm
parents: 21633
diff changeset
    13
  (*Basic meta-theory*)
edc90be09ac1 misc cleanup of ML bindings (for multihreading);
wenzelm
parents: 21633
diff changeset
    14
  "UNITY_Main",
11193
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents: 10782
diff changeset
    15
24147
edc90be09ac1 misc cleanup of ML bindings (for multihreading);
wenzelm
parents: 21633
diff changeset
    16
  (*Simple examples: no composition*)
edc90be09ac1 misc cleanup of ML bindings (for multihreading);
wenzelm
parents: 21633
diff changeset
    17
  "Simple/Deadlock",
edc90be09ac1 misc cleanup of ML bindings (for multihreading);
wenzelm
parents: 21633
diff changeset
    18
  "Simple/Common",
edc90be09ac1 misc cleanup of ML bindings (for multihreading);
wenzelm
parents: 21633
diff changeset
    19
  "Simple/Network",
edc90be09ac1 misc cleanup of ML bindings (for multihreading);
wenzelm
parents: 21633
diff changeset
    20
  "Simple/Token",
edc90be09ac1 misc cleanup of ML bindings (for multihreading);
wenzelm
parents: 21633
diff changeset
    21
  "Simple/Channel",
edc90be09ac1 misc cleanup of ML bindings (for multihreading);
wenzelm
parents: 21633
diff changeset
    22
  "Simple/Lift",
edc90be09ac1 misc cleanup of ML bindings (for multihreading);
wenzelm
parents: 21633
diff changeset
    23
  "Simple/Mutex",
edc90be09ac1 misc cleanup of ML bindings (for multihreading);
wenzelm
parents: 21633
diff changeset
    24
  "Simple/Reach",
edc90be09ac1 misc cleanup of ML bindings (for multihreading);
wenzelm
parents: 21633
diff changeset
    25
  "Simple/Reachability",
11193
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents: 10782
diff changeset
    26
24147
edc90be09ac1 misc cleanup of ML bindings (for multihreading);
wenzelm
parents: 21633
diff changeset
    27
  (*Verifying security protocols using UNITY*)
edc90be09ac1 misc cleanup of ML bindings (for multihreading);
wenzelm
parents: 21633
diff changeset
    28
  "Simple/NSP_Bad",
9112
44fc37919579 added the AllocImpl example
paulson
parents: 9000
diff changeset
    29
24147
edc90be09ac1 misc cleanup of ML bindings (for multihreading);
wenzelm
parents: 21633
diff changeset
    30
  (*Example of composition*)
edc90be09ac1 misc cleanup of ML bindings (for multihreading);
wenzelm
parents: 21633
diff changeset
    31
  "Comp/Handshake",
10782
ddb433987557 new examples by Sidi Ehmety
paulson
parents: 10265
diff changeset
    32
24147
edc90be09ac1 misc cleanup of ML bindings (for multihreading);
wenzelm
parents: 21633
diff changeset
    33
  (*Universal properties examples*)
edc90be09ac1 misc cleanup of ML bindings (for multihreading);
wenzelm
parents: 21633
diff changeset
    34
  "Comp/Counter",
edc90be09ac1 misc cleanup of ML bindings (for multihreading);
wenzelm
parents: 21633
diff changeset
    35
  "Comp/Counterc",
edc90be09ac1 misc cleanup of ML bindings (for multihreading);
wenzelm
parents: 21633
diff changeset
    36
  "Comp/Priority",
edc90be09ac1 misc cleanup of ML bindings (for multihreading);
wenzelm
parents: 21633
diff changeset
    37
edc90be09ac1 misc cleanup of ML bindings (for multihreading);
wenzelm
parents: 21633
diff changeset
    38
  "Comp/TimerArray",
edc90be09ac1 misc cleanup of ML bindings (for multihreading);
wenzelm
parents: 21633
diff changeset
    39
edc90be09ac1 misc cleanup of ML bindings (for multihreading);
wenzelm
parents: 21633
diff changeset
    40
  (*obsolete*)
edc90be09ac1 misc cleanup of ML bindings (for multihreading);
wenzelm
parents: 21633
diff changeset
    41
  "ELT"
edc90be09ac1 misc cleanup of ML bindings (for multihreading);
wenzelm
parents: 21633
diff changeset
    42
];
9112
44fc37919579 added the AllocImpl example
paulson
parents: 9000
diff changeset
    43
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 13785
diff changeset
    44
(*Allocator example*)
21633
d1cb78244e30 theory Alloc no longer works -- quick_and_dirty;
wenzelm
parents: 14203
diff changeset
    45
(* FIXME some parts no longer work -- had been commented out for a long time *)
28529
7ff939586e83 setmp_noncritical makes it work with future scheduler;
wenzelm
parents: 24147
diff changeset
    46
setmp_noncritical quick_and_dirty true
24147
edc90be09ac1 misc cleanup of ML bindings (for multihreading);
wenzelm
parents: 21633
diff changeset
    47
  use_thy "Comp/Alloc";
8987
718907f55f62 fixed the dependences
paulson
parents: 8334
diff changeset
    48
24147
edc90be09ac1 misc cleanup of ML bindings (for multihreading);
wenzelm
parents: 21633
diff changeset
    49
use_thys ["Comp/AllocImpl", "Comp/Client"];