Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/UNITY/ROOT.ML
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 41892 2386fb64feaf
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
32624
3dec57ec3473 entry point theory for examples; reactivated half-dead example
haftmann
parents: 28866
diff changeset 
     1
 
(*  Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset 
     2
 
    Copyright   1998  University of Cambridge
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset 
     3
 
*)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset 
     4
 







24147






edc90be09ac1
misc cleanup of ML bindings (for multihreading);



wenzelm


parents: 
21633

diff
changeset




     5


(*Verifying security protocols using UNITY*)








33615






261abc2e3155
uniform use of simultabeous use_thys;



wenzelm


parents: 
32624

diff
changeset




     6


no_document use_thys ["../Auth/Public"];








11193






851c90b23a9e
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp



paulson


parents: 
10782

diff
changeset




     7









33615






261abc2e3155
uniform use of simultabeous use_thys;



wenzelm


parents: 
32624

diff
changeset




     8


use_thys [








41892






2386fb64feaf
eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;



wenzelm


parents: 
33615

diff
changeset




     9


  (*Basic meta-theory*)













2386fb64feaf
eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;



wenzelm


parents: 
33615

diff
changeset




    10


  "UNITY_Main",













2386fb64feaf
eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;



wenzelm


parents: 
33615

diff
changeset




    11














2386fb64feaf
eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;



wenzelm


parents: 
33615

diff
changeset




    12


  (*Simple examples: no composition*)













2386fb64feaf
eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;



wenzelm


parents: 
33615

diff
changeset




    13


  "Simple/Deadlock",













2386fb64feaf
eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;



wenzelm


parents: 
33615

diff
changeset




    14


  "Simple/Common",













2386fb64feaf
eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;



wenzelm


parents: 
33615

diff
changeset




    15


  "Simple/Network",













2386fb64feaf
eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;



wenzelm


parents: 
33615

diff
changeset




    16


  "Simple/Token",













2386fb64feaf
eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;



wenzelm


parents: 
33615

diff
changeset




    17


  "Simple/Channel",













2386fb64feaf
eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;



wenzelm


parents: 
33615

diff
changeset




    18


  "Simple/Lift",













2386fb64feaf
eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;



wenzelm


parents: 
33615

diff
changeset




    19


  "Simple/Mutex",













2386fb64feaf
eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;



wenzelm


parents: 
33615

diff
changeset




    20


  "Simple/Reach",













2386fb64feaf
eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;



wenzelm


parents: 
33615

diff
changeset




    21


  "Simple/Reachability",













2386fb64feaf
eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;



wenzelm


parents: 
33615

diff
changeset




    22














2386fb64feaf
eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;



wenzelm


parents: 
33615

diff
changeset




    23


  (*Verifying security protocols using UNITY*)













2386fb64feaf
eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;



wenzelm


parents: 
33615

diff
changeset




    24


  "Simple/NSP_Bad",













2386fb64feaf
eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;



wenzelm


parents: 
33615

diff
changeset




    25














2386fb64feaf
eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;



wenzelm


parents: 
33615

diff
changeset




    26


  (*Example of composition*)













2386fb64feaf
eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;



wenzelm


parents: 
33615

diff
changeset




    27


  "Comp/Handshake",













2386fb64feaf
eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;



wenzelm


parents: 
33615

diff
changeset




    28














2386fb64feaf
eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;



wenzelm


parents: 
33615

diff
changeset




    29


  (*Universal properties examples*)













2386fb64feaf
eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;



wenzelm


parents: 
33615

diff
changeset




    30


  "Comp/Counter",













2386fb64feaf
eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;



wenzelm


parents: 
33615

diff
changeset




    31


  "Comp/Counterc",













2386fb64feaf
eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;



wenzelm


parents: 
33615

diff
changeset




    32


  "Comp/Priority",













2386fb64feaf
eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;



wenzelm


parents: 
33615

diff
changeset




    33














2386fb64feaf
eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;



wenzelm


parents: 
33615

diff
changeset




    34


  "Comp/TimerArray",













2386fb64feaf
eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;



wenzelm


parents: 
33615

diff
changeset




    35


  "Comp/Progress",













2386fb64feaf
eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;



wenzelm


parents: 
33615

diff
changeset




    36














2386fb64feaf
eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;



wenzelm


parents: 
33615

diff
changeset




    37


  "Comp/Alloc",













2386fb64feaf
eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;



wenzelm


parents: 
33615

diff
changeset




    38


  "Comp/AllocImpl",













2386fb64feaf
eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;



wenzelm


parents: 
33615

diff
changeset




    39


  "Comp/Client",













2386fb64feaf
eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;



wenzelm


parents: 
33615

diff
changeset




    40














2386fb64feaf
eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;



wenzelm


parents: 
33615

diff
changeset




    41


  (*obsolete*)













2386fb64feaf
eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;



wenzelm


parents: 
33615

diff
changeset




    42


  "ELT"








33615






261abc2e3155
uniform use of simultabeous use_thys;



wenzelm


parents: 
32624

diff
changeset




    43


];















isabelle