src/HOL/ROOT
author wenzelm
Sat, 13 Feb 2016 11:50:01 +0100
changeset 62285 747fc3692fca
parent 62242 a4e6ea45f416
child 62286 705d4c4003ea
permissions -rw-r--r--
unconditional test -- nothing special here;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
51397
03b586ee5930 support for 'chapter' specifications within session ROOT;
wenzelm
parents: 51263
diff changeset
     1
chapter HOL
03b586ee5930 support for 'chapter' specifications within session ROOT;
wenzelm
parents: 51263
diff changeset
     2
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
     3
session HOL (main) = Pure +
51421
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
     4
  description {*
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
     5
    Classical Higher-order Logic.
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
     6
  *}
56801
8dd9df88f647 some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
wenzelm
parents: 56781
diff changeset
     7
  global_theories
8dd9df88f647 some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
wenzelm
parents: 56781
diff changeset
     8
    Main
8dd9df88f647 some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
wenzelm
parents: 56781
diff changeset
     9
    Complex_Main
48901
5e0455e29339 more basic file dependencies -- no load command here;
wenzelm
parents: 48765
diff changeset
    10
  files
5e0455e29339 more basic file dependencies -- no load command here;
wenzelm
parents: 48765
diff changeset
    11
    "Tools/Quickcheck/Narrowing_Engine.hs"
5e0455e29339 more basic file dependencies -- no load command here;
wenzelm
parents: 48765
diff changeset
    12
    "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
    13
  document_files
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
    14
    "root.bib"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
    15
    "root.tex"
48338
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
    16
61152
13b2fd801692 HOL-Proofs is slow;
wenzelm
parents: 61140
diff changeset
    17
session "HOL-Proofs" (slow) = Pure +
51421
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
    18
  description {*
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
    19
    HOL-Main with explicit proof terms.
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
    20
  *}
62242
a4e6ea45f416 guard sessions that no longer work with SML/NJ -- memory problems;
wenzelm
parents: 62168
diff changeset
    21
  options [condition = ML_SYSTEM_POLYML, document = false, quick_and_dirty = false]
52488
cd65ee49a8ba discontinued system option "proofs" -- global state of Proofterm.proofs is persistently compiled into HOL-Proofs image;
wenzelm
parents: 52424
diff changeset
    22
  theories Proofs (*sequential change of global flag!*)
58372
bfd497f2f4c2 moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer)
blanchet
parents: 58371
diff changeset
    23
  theories "~~/src/HOL/Library/Old_Datatype"
48901
5e0455e29339 more basic file dependencies -- no load command here;
wenzelm
parents: 48765
diff changeset
    24
  files
5e0455e29339 more basic file dependencies -- no load command here;
wenzelm
parents: 48765
diff changeset
    25
    "Tools/Quickcheck/Narrowing_Engine.hs"
5e0455e29339 more basic file dependencies -- no load command here;
wenzelm
parents: 48765
diff changeset
    26
    "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
48338
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
    27
50844
b95ff3744815 populate "main" session group, e.g. relevant for Isabelle/jEdit logic selection;
wenzelm
parents: 50833
diff changeset
    28
session "HOL-Library" (main) in Library = HOL +
51421
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
    29
  description {*
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
    30
    Classical Higher-order Logic -- batteries included.
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
    31
  *}
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    32
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    33
    Library
59973
a51af4f12d47 proper test for session HOL-Library;
wenzelm
parents: 59922
diff changeset
    34
    Rewrite
51161
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51160
diff changeset
    35
    (*conflicting type class instantiations*)
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    36
    List_lexord
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    37
    Sublist_Order
51115
7dbd6832a689 consolidation of library theories on product orders
haftmann
parents: 51093
diff changeset
    38
    Product_Lexorder
7dbd6832a689 consolidation of library theories on product orders
haftmann
parents: 51093
diff changeset
    39
    Product_Order
51161
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51160
diff changeset
    40
    Finite_Lattice
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51160
diff changeset
    41
    (*data refinements and dependent applications*)
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51160
diff changeset
    42
    AList_Mapping
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51160
diff changeset
    43
    Code_Binary_Nat
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51160
diff changeset
    44
    Code_Char
55447
aa41ecbdc205 do not redefine outer syntax commands;
wenzelm
parents: 55417
diff changeset
    45
    Code_Prolog
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    46
    Code_Real_Approx_By_Float
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents: 49985
diff changeset
    47
    Code_Target_Numeral
51161
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51160
diff changeset
    48
    DAList
54429
be1bc181bcde explicit inclusion of data refinement theory into HOL-Library session
haftmann
parents: 54193
diff changeset
    49
    DAList_Multiset
51161
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51160
diff changeset
    50
    RBT_Mapping
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51160
diff changeset
    51
    RBT_Set
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51160
diff changeset
    52
    (*legacy tools*)
49985
5b4b0e4e5205 moved Refute to "HOL/Library" to speed up building "Main" even more
blanchet
parents: 49932
diff changeset
    53
    Refute
58372
bfd497f2f4c2 moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer)
blanchet
parents: 58371
diff changeset
    54
    Old_Datatype
51161
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51160
diff changeset
    55
    Old_Recdef
58110
019c0211ed1f took out legacy material from 'HOL/Library/Library.thy'
blanchet
parents: 58039
diff changeset
    56
    Old_SMT
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
    57
  document_files "root.bib" "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    58
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
    59
session "HOL-Hahn_Banach" in Hahn_Banach = HOL +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    60
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    61
    Author:     Gertrud Bauer, TU Munich
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    62
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    63
    The Hahn-Banach theorem for real vector spaces.
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    64
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    65
    This is the proof of the Hahn-Banach theorem for real vectorspaces,
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    66
    following H. Heuser, Funktionalanalysis, p. 228 -232. The Hahn-Banach
55018
2a526bd279ed moved 'Zorn' into 'Main', since it's a BNF dependency
blanchet
parents: 54961
diff changeset
    67
    theorem is one of the fundamental theorems of functional analysis. It is a
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    68
    conclusion of Zorn's lemma.
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    69
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    70
    Two different formaulations of the theorem are presented, one for general
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    71
    real vectorspaces and its application to normed vectorspaces.
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    72
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    73
    The theorem says, that every continous linearform, defined on arbitrary
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    74
    subspaces (not only one-dimensional subspaces), can be extended to a
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    75
    continous linearform on the whole vectorspace.
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    76
  *}
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    77
  theories Hahn_Banach
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
    78
  document_files "root.bib" "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    79
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
    80
session "HOL-Induct" in Induct = HOL +
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    81
  description {*
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    82
    Examples of (Co)Inductive Definitions.
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    83
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    84
    Comb proves the Church-Rosser theorem for combinators (see
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    85
    http://www.cl.cam.ac.uk/ftp/papers/reports/TR396-lcp-generic-automatic-proof-tools.ps.gz).
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    86
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    87
    Mutil is the famous Mutilated Chess Board problem (see
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    88
    http://www.cl.cam.ac.uk/ftp/papers/reports/TR394-lcp-mutilated-chess-board.dvi.gz).
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    89
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    90
    PropLog proves the completeness of a formalization of propositional logic
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    91
    (see
58372
bfd497f2f4c2 moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer)
blanchet
parents: 58371
diff changeset
    92
    http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz).
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    93
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    94
    Exp demonstrates the use of iterated inductive definitions to reason about
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    95
    mutually recursive relations.
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    96
  *}
58372
bfd497f2f4c2 moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer)
blanchet
parents: 58371
diff changeset
    97
  theories [document = false]
bfd497f2f4c2 moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer)
blanchet
parents: 58371
diff changeset
    98
    "~~/src/HOL/Library/Old_Datatype"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    99
  theories [quick_and_dirty]
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   100
    Common_Patterns
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   101
  theories
61935
6512e84cc9f5 clarified sessions;
wenzelm
parents: 61793
diff changeset
   102
    Nested_Datatype
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   103
    QuoDataType
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   104
    QuoNestedDataType
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   105
    Term
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   106
    SList
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   107
    ABexp
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   108
    Tree
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   109
    Ordinals
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   110
    Sigma_Algebra
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   111
    Comb
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   112
    PropLog
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   113
    Com
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   114
  document_files "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   115
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   116
session "HOL-IMP" in IMP = HOL +
59446
4427f04fca57 discontinued obsolete option "document_graph";
wenzelm
parents: 59190
diff changeset
   117
  options [document_variants = document]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   118
  theories [document = false]
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   119
    "~~/src/HOL/Library/While_Combinator"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   120
    "~~/src/HOL/Library/Char_ord"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   121
    "~~/src/HOL/Library/List_lexord"
51625
bd3358aac5d2 tuned document
nipkow
parents: 51562
diff changeset
   122
    "~~/src/HOL/Library/Quotient_List"
bd3358aac5d2 tuned document
nipkow
parents: 51562
diff changeset
   123
    "~~/src/HOL/Library/Extended"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   124
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   125
    BExp
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   126
    ASM
50050
fac2b27893ff new theory IMP/Finite_Reachable
nipkow
parents: 50023
diff changeset
   127
    Finite_Reachable
52394
fe33d456b36c more canonical name (2)
nipkow
parents: 52363
diff changeset
   128
    Denotational
52400
ded7b9c60dc2 tuned theory name
nipkow
parents: 52394
diff changeset
   129
    Compiler2
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   130
    Poly_Types
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   131
    Sec_Typing
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   132
    Sec_TypingT
52726
ee0bd6bababd merged Def_Init_Sound_X into Def_Init_X
nipkow
parents: 52722
diff changeset
   133
    Def_Init_Big
ee0bd6bababd merged Def_Init_Sound_X into Def_Init_X
nipkow
parents: 52722
diff changeset
   134
    Def_Init_Small
ee0bd6bababd merged Def_Init_Sound_X into Def_Init_X
nipkow
parents: 52722
diff changeset
   135
    Fold
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   136
    Live
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   137
    Live_True
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   138
    Hoare_Examples
52269
d867812da48b more VC -> VCG
nipkow
parents: 52248
diff changeset
   139
    VCG
52282
c79a3e15779e tuned theory name
nipkow
parents: 52277
diff changeset
   140
    Hoare_Total
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   141
    Collecting1
48765
fb1ed5230abc special code with lists no longer necessary, use sets
nipkow
parents: 48738
diff changeset
   142
    Collecting_Examples
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   143
    Abs_Int_Tests
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   144
    Abs_Int1_parity
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   145
    Abs_Int1_const
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   146
    Abs_Int3
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   147
    "Abs_Int_ITP/Abs_Int1_parity_ITP"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   148
    "Abs_Int_ITP/Abs_Int1_const_ITP"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   149
    "Abs_Int_ITP/Abs_Int3_ITP"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   150
    "Abs_Int_Den/Abs_Int_den2"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   151
    Procs_Dyn_Vars_Dyn
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   152
    Procs_Stat_Vars_Dyn
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   153
    Procs_Stat_Vars_Stat
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   154
    C_like
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   155
    OO
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   156
  document_files "root.bib" "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   157
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   158
session "HOL-IMPP" in IMPP = HOL +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   159
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   160
    Author:     David von Oheimb
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   161
    Copyright   1999 TUM
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   162
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   163
    IMPP -- An imperative language with procedures.
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   164
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   165
    This is an extension of IMP with local variables and mutually recursive
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   166
    procedures. For documentation see "Hoare Logic for Mutual Recursion and
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   167
    Local Variables" (http://isabelle.in.tum.de/Bali/papers/FSTTCS99.html).
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   168
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   169
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   170
  theories EvenOdd
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   171
61203
a8a8eca85801 New subdirectory for functional data structures
nipkow
parents: 61152
diff changeset
   172
session "HOL-Data_Structures" in Data_Structures = HOL +
a8a8eca85801 New subdirectory for functional data structures
nipkow
parents: 61152
diff changeset
   173
  options [document_variants = document]
a8a8eca85801 New subdirectory for functional data structures
nipkow
parents: 61152
diff changeset
   174
  theories [document = false]
a8a8eca85801 New subdirectory for functional data structures
nipkow
parents: 61152
diff changeset
   175
    "Less_False"
a8a8eca85801 New subdirectory for functional data structures
nipkow
parents: 61152
diff changeset
   176
  theories
a8a8eca85801 New subdirectory for functional data structures
nipkow
parents: 61152
diff changeset
   177
    Tree_Map
61232
c46faf9762f7 added AVL and lookup function
nipkow
parents: 61224
diff changeset
   178
    AVL_Map
61224
759b5299a9f2 added red black trees
nipkow
parents: 61203
diff changeset
   179
    RBT_Map
61469
cd82b1023932 added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents: 61368
diff changeset
   180
    Tree23_Map
61514
213556e498c2 added 234-Trees (slow)
nipkow
parents: 61469
diff changeset
   181
    Tree234_Map
61789
9ce1a397410a added Brother12_Map
nipkow
parents: 61784
diff changeset
   182
    Brother12_Map
62130
90a3016a6c12 added AA_Map; tuned titles
nipkow
parents: 62008
diff changeset
   183
    AA_Map
61525
87244a9cfe40 added splay trees
nipkow
parents: 61514
diff changeset
   184
    Splay_Map
61224
759b5299a9f2 added red black trees
nipkow
parents: 61203
diff changeset
   185
  document_files "root.tex" "root.bib"
61203
a8a8eca85801 New subdirectory for functional data structures
nipkow
parents: 61152
diff changeset
   186
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   187
session "HOL-Import" in Import = HOL +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   188
  theories HOL_Light_Maps
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   189
  theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   190
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   191
session "HOL-Number_Theory" in Number_Theory = HOL +
55321
eadea363deb6 Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents: 55240
diff changeset
   192
  description {*
eadea363deb6 Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents: 55240
diff changeset
   193
    Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler
55730
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents: 55663
diff changeset
   194
    Theorem, Wilson's Theorem, some lemmas for Quadratic Reciprocity.
55321
eadea363deb6 Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents: 55240
diff changeset
   195
  *}
eadea363deb6 Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents: 55240
diff changeset
   196
  theories [document = false]
eadea363deb6 Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents: 55240
diff changeset
   197
    "~~/src/HOL/Library/FuncSet"
eadea363deb6 Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents: 55240
diff changeset
   198
    "~~/src/HOL/Library/Multiset"
eadea363deb6 Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents: 55240
diff changeset
   199
    "~~/src/HOL/Algebra/Ring"
eadea363deb6 Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents: 55240
diff changeset
   200
    "~~/src/HOL/Algebra/FiniteProduct"
eadea363deb6 Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents: 55240
diff changeset
   201
  theories
eadea363deb6 Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents: 55240
diff changeset
   202
    Pocklington
55730
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents: 55663
diff changeset
   203
    Gauss
55321
eadea363deb6 Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents: 55240
diff changeset
   204
    Number_Theory
58023
62826b36ac5e generic euclidean algorithm (due to Manuel Eberl)
haftmann
parents: 57998
diff changeset
   205
    Euclidean_Algorithm
60804
080a979a985b formal class for factorial (semi)rings
haftmann
parents: 60751
diff changeset
   206
    Factorial_Ring
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   207
  document_files
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   208
    "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   209
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   210
session "HOL-Old_Number_Theory" in Old_Number_Theory = HOL +
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   211
  description {*
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   212
    Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   213
    Theorem, Wilson's Theorem, Quadratic Reciprocity.
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   214
  *}
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   215
  theories [document = false]
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   216
    "~~/src/HOL/Library/Infinite_Set"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   217
    "~~/src/HOL/Library/Permutation"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   218
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   219
    Fib
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   220
    Factorization
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   221
    Chinese
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   222
    WilsonRuss
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   223
    WilsonBij
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   224
    Quadratic_Reciprocity
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   225
    Primes
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   226
    Pocklington
58623
2db1df2c8467 more bibtex entries;
wenzelm
parents: 58433
diff changeset
   227
  document_files
2db1df2c8467 more bibtex entries;
wenzelm
parents: 58433
diff changeset
   228
    "root.bib"
2db1df2c8467 more bibtex entries;
wenzelm
parents: 58433
diff changeset
   229
    "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   230
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   231
session "HOL-Hoare" in Hoare = HOL +
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   232
  description {*
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   233
    Verification of imperative programs (verification conditions are generated
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   234
    automatically from pre/post conditions and loop invariants).
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   235
  *}
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   236
  theories Hoare
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   237
  document_files "root.bib" "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   238
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   239
session "HOL-Hoare_Parallel" in Hoare_Parallel = HOL +
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   240
  description {*
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   241
    Verification of shared-variable imperative programs a la Owicki-Gries.
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   242
    (verification conditions are generated automatically).
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   243
  *}
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   244
  theories Hoare_Parallel
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   245
  document_files "root.bib" "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   246
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   247
session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" +
59992
d8db5172c23f make SML/NJ more happy;
wenzelm
parents: 59973
diff changeset
   248
  options [condition = ML_SYSTEM_POLYML, document = false, browser_info = false]
51422
821a70e29e0b proper formatting, to facilitate line-based diff;
wenzelm
parents: 51421
diff changeset
   249
  theories
821a70e29e0b proper formatting, to facilitate line-based diff;
wenzelm
parents: 51421
diff changeset
   250
    Generate
821a70e29e0b proper formatting, to facilitate line-based diff;
wenzelm
parents: 51421
diff changeset
   251
    Generate_Binary_Nat
821a70e29e0b proper formatting, to facilitate line-based diff;
wenzelm
parents: 51421
diff changeset
   252
    Generate_Target_Nat
821a70e29e0b proper formatting, to facilitate line-based diff;
wenzelm
parents: 51421
diff changeset
   253
    Generate_Efficient_Datastructures
821a70e29e0b proper formatting, to facilitate line-based diff;
wenzelm
parents: 51421
diff changeset
   254
    Generate_Pretty_Char
62242
a4e6ea45f416 guard sessions that no longer work with SML/NJ -- memory problems;
wenzelm
parents: 62168
diff changeset
   255
  theories [condition = "ML_SYSTEM_POLYML,ISABELLE_GHC"]
58039
469a375212c1 add testing framework for generated code
Andreas Lochbihler
parents: 58023
diff changeset
   256
    Code_Test_GHC
62242
a4e6ea45f416 guard sessions that no longer work with SML/NJ -- memory problems;
wenzelm
parents: 62168
diff changeset
   257
  theories [condition = "ML_SYSTEM_POLYML,ISABELLE_MLTON"]
58039
469a375212c1 add testing framework for generated code
Andreas Lochbihler
parents: 58023
diff changeset
   258
    Code_Test_MLton
62242
a4e6ea45f416 guard sessions that no longer work with SML/NJ -- memory problems;
wenzelm
parents: 62168
diff changeset
   259
  theories [condition = "ML_SYSTEM_POLYML,ISABELLE_OCAMLC"]
58039
469a375212c1 add testing framework for generated code
Andreas Lochbihler
parents: 58023
diff changeset
   260
    Code_Test_OCaml
62242
a4e6ea45f416 guard sessions that no longer work with SML/NJ -- memory problems;
wenzelm
parents: 62168
diff changeset
   261
  theories [condition = "ML_SYSTEM_POLYML,ISABELLE_POLYML"]
58039
469a375212c1 add testing framework for generated code
Andreas Lochbihler
parents: 58023
diff changeset
   262
    Code_Test_PolyML
62242
a4e6ea45f416 guard sessions that no longer work with SML/NJ -- memory problems;
wenzelm
parents: 62168
diff changeset
   263
  theories [condition = "ML_SYSTEM_POLYML,ISABELLE_SCALA"]
58039
469a375212c1 add testing framework for generated code
Andreas Lochbihler
parents: 58023
diff changeset
   264
    Code_Test_Scala
62242
a4e6ea45f416 guard sessions that no longer work with SML/NJ -- memory problems;
wenzelm
parents: 62168
diff changeset
   265
  theories [condition = "ML_SYSTEM_POLYML,ISABELLE_SMLNJ"]
58039
469a375212c1 add testing framework for generated code
Andreas Lochbihler
parents: 58023
diff changeset
   266
    Code_Test_SMLNJ
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   267
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   268
session "HOL-Metis_Examples" in Metis_Examples = HOL +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   269
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   270
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   271
    Author:     Jasmin Blanchette, TU Muenchen
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   272
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   273
    Testing Metis and Sledgehammer.
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   274
  *}
58423
e4d540c0dd57 clarified timeout for isatest;
wenzelm
parents: 58419
diff changeset
   275
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   276
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   277
    Abstraction
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   278
    Big_O
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   279
    Binary_Tree
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   280
    Clausification
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   281
    Message
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   282
    Proxies
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   283
    Tarski
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   284
    Trans_Closure
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   285
    Sets
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   286
55072
8488fdc4ddc0 minimized Nitpick's dependencies
blanchet
parents: 55071
diff changeset
   287
session "HOL-Nitpick_Examples" in Nitpick_Examples = HOL +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   288
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   289
    Author:     Jasmin Blanchette, TU Muenchen
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   290
    Copyright   2009
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   291
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   292
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   293
  theories [quick_and_dirty] Nitpick_Examples
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   294
50844
b95ff3744815 populate "main" session group, e.g. relevant for Isabelle/jEdit logic selection;
wenzelm
parents: 50833
diff changeset
   295
session "HOL-Algebra" (main) in Algebra = HOL +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   296
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   297
    Author: Clemens Ballarin, started 24 September 1999
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   298
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   299
    The Isabelle Algebraic Library.
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   300
  *}
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   301
  theories [document = false]
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   302
    (* Preliminaries from set and number theory *)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   303
    "~~/src/HOL/Library/FuncSet"
55159
608c157d743d Replacing the theory Library/Binomial by Number_Theory/Binomial
paulson <lp15@cam.ac.uk>
parents: 55123
diff changeset
   304
    "~~/src/HOL/Number_Theory/Primes"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   305
    "~~/src/HOL/Library/Permutation"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   306
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   307
    (*** New development, based on explicit structures ***)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   308
    (* Groups *)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   309
    FiniteProduct        (* Product operator for commutative groups *)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   310
    Sylow                (* Sylow's theorem *)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   311
    Bij                  (* Automorphism Groups *)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   312
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   313
    (* Rings *)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   314
    Divisibility         (* Rings *)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   315
    IntRing              (* Ideals and residue classes *)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   316
    UnivPoly             (* Polynomials *)
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   317
  document_files "root.bib" "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   318
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   319
session "HOL-Auth" in Auth = HOL +
51421
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   320
  description {*
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   321
    A new approach to verifying authentication protocols.
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   322
  *}
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   323
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   324
    Auth_Shared
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   325
    Auth_Public
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   326
    "Smartcard/Auth_Smartcard"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   327
    "Guard/Auth_Guard_Shared"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   328
    "Guard/Auth_Guard_Public"
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   329
  document_files "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   330
51236
f301ad90c48b more explicit session dependency, for improved parallel performance of HOL-UNITY test session -- NB: separate 'theories' sections are sequential;
wenzelm
parents: 51161
diff changeset
   331
session "HOL-UNITY" in UNITY = "HOL-Auth" +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   332
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   333
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   334
    Copyright   1998  University of Cambridge
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   335
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   336
    Verifying security protocols using Chandy and Misra's UNITY formalism.
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   337
  *}
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   338
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   339
    (*Basic meta-theory*)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   340
    "UNITY_Main"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   341
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   342
    (*Simple examples: no composition*)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   343
    "Simple/Deadlock"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   344
    "Simple/Common"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   345
    "Simple/Network"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   346
    "Simple/Token"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   347
    "Simple/Channel"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   348
    "Simple/Lift"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   349
    "Simple/Mutex"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   350
    "Simple/Reach"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   351
    "Simple/Reachability"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   352
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   353
    (*Verifying security protocols using UNITY*)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   354
    "Simple/NSP_Bad"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   355
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   356
    (*Example of composition*)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   357
    "Comp/Handshake"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   358
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   359
    (*Universal properties examples*)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   360
    "Comp/Counter"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   361
    "Comp/Counterc"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   362
    "Comp/Priority"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   363
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   364
    "Comp/TimerArray"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   365
    "Comp/Progress"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   366
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   367
    "Comp/Alloc"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   368
    "Comp/AllocImpl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   369
    "Comp/Client"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   370
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   371
    (*obsolete*)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   372
    "ELT"
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   373
  document_files "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   374
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   375
session "HOL-Unix" in Unix = HOL +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   376
  options [print_mode = "no_brackets,no_type_brackets"]
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   377
  theories Unix
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   378
  document_files "root.bib" "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   379
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   380
session "HOL-ZF" in ZF = HOL +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   381
  theories MainZF Games
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   382
  document_files "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   383
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   384
session "HOL-Imperative_HOL" in Imperative_HOL = HOL +
59446
4427f04fca57 discontinued obsolete option "document_graph";
wenzelm
parents: 59190
diff changeset
   385
  options [print_mode = "iff,no_brackets"]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   386
  theories [document = false]
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   387
    "~~/src/HOL/Library/Countable"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   388
    "~~/src/HOL/Library/Monad_Syntax"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   389
    "~~/src/HOL/Library/LaTeXsugar"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   390
  theories Imperative_HOL_ex
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   391
  document_files "root.bib" "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   392
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   393
session "HOL-Decision_Procs" in Decision_Procs = HOL +
51544
8c58fbbc1d5a tuned session specification;
wenzelm
parents: 51517
diff changeset
   394
  description {*
8c58fbbc1d5a tuned session specification;
wenzelm
parents: 51517
diff changeset
   395
    Various decision procedures, typically involving reflection.
8c58fbbc1d5a tuned session specification;
wenzelm
parents: 51517
diff changeset
   396
  *}
58413
22dd971f6938 renamed ISABELLE_POLYML to ML_SYSTEM_POLYML, to avoid overlap with ISABELLE_POLYML_PATH;
wenzelm
parents: 58385
diff changeset
   397
  options [condition = ML_SYSTEM_POLYML, document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   398
  theories Decision_Procs
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   399
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   400
session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
62242
a4e6ea45f416 guard sessions that no longer work with SML/NJ -- memory problems;
wenzelm
parents: 62168
diff changeset
   401
  options [condition = ML_SYSTEM_POLYML, document = false, parallel_proofs = 0]
52424
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents: 52400
diff changeset
   402
  theories
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents: 52400
diff changeset
   403
    Hilbert_Classical
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents: 52400
diff changeset
   404
    XML_Data
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   405
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   406
session "HOL-Proofs-Extraction" in "Proofs/Extraction" = "HOL-Proofs" +
51421
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   407
  description {*
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   408
    Examples for program extraction in Higher-Order Logic.
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   409
  *}
59006
272d7fb92396 no quick_and_dirty for proof extraction, to avoid obscure errors like "corr: bad proof";
wenzelm
parents: 58849
diff changeset
   410
  options [condition = ML_SYSTEM_POLYML, parallel_proofs = 0, quick_and_dirty = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   411
  theories [document = false]
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51115
diff changeset
   412
    "~~/src/HOL/Library/Code_Target_Numeral"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   413
    "~~/src/HOL/Library/Monad_Syntax"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   414
    "~~/src/HOL/Number_Theory/Primes"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   415
    "~~/src/HOL/Number_Theory/UniqueFactorization"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   416
    "~~/src/HOL/Library/State_Monad"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   417
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   418
    Greatest_Common_Divisor
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   419
    Warshall
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   420
    Higman_Extraction
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   421
    Pigeonhole
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   422
    Euclid
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   423
  document_files "root.bib" "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   424
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   425
session "HOL-Proofs-Lambda" in "Proofs/Lambda" = "HOL-Proofs" +
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   426
  description {*
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   427
    Lambda Calculus in de Bruijn's Notation.
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   428
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   429
    This session defines lambda-calculus terms with de Bruijn indixes and
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   430
    proves confluence of beta, eta and beta+eta.
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   431
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   432
    The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   433
    theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html).
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   434
  *}
62242
a4e6ea45f416 guard sessions that no longer work with SML/NJ -- memory problems;
wenzelm
parents: 62168
diff changeset
   435
  options [condition = ML_SYSTEM_POLYML, print_mode = "no_brackets",
a4e6ea45f416 guard sessions that no longer work with SML/NJ -- memory problems;
wenzelm
parents: 62168
diff changeset
   436
    parallel_proofs = 0, quick_and_dirty = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   437
  theories [document = false]
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51115
diff changeset
   438
    "~~/src/HOL/Library/Code_Target_Int"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   439
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   440
    Eta
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   441
    StrongNorm
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   442
    Standardization
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   443
    WeakNorm
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   444
  document_files "root.bib" "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   445
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   446
session "HOL-Prolog" in Prolog = HOL +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   447
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   448
    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   449
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   450
    A bare-bones implementation of Lambda-Prolog.
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   451
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   452
    This is a simple exploratory implementation of Lambda-Prolog in HOL,
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   453
    including some minimal examples (in Test.thy) and a more typical example of
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   454
    a little functional language and its type system.
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   455
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   456
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   457
  theories Test Type
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   458
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   459
session "HOL-MicroJava" in MicroJava = HOL +
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   460
  description {*
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   461
    Formalization of a fragment of Java, together with a corresponding virtual
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   462
    machine and a specification of its bytecode verifier and a lightweight
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   463
    bytecode verifier, including proofs of type-safety.
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   464
  *}
59446
4427f04fca57 discontinued obsolete option "document_graph";
wenzelm
parents: 59190
diff changeset
   465
  theories [document = false]
4427f04fca57 discontinued obsolete option "document_graph";
wenzelm
parents: 59190
diff changeset
   466
    "~~/src/HOL/Library/While_Combinator"
4427f04fca57 discontinued obsolete option "document_graph";
wenzelm
parents: 59190
diff changeset
   467
  theories
4427f04fca57 discontinued obsolete option "document_graph";
wenzelm
parents: 59190
diff changeset
   468
    MicroJava
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   469
  document_files
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   470
    "introduction.tex"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   471
    "root.bib"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   472
    "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   473
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   474
session "HOL-NanoJava" in NanoJava = HOL +
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   475
  description {*
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   476
    Hoare Logic for a tiny fragment of Java.
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   477
  *}
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   478
  theories Example
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   479
  document_files "root.bib" "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   480
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   481
session "HOL-Bali" in Bali = HOL +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   482
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   483
    AxExample
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   484
    AxSound
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   485
    AxCompl
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   486
    Trans
60751
83f04804696c reactivated dead code;
wenzelm
parents: 60603
diff changeset
   487
    TypeSafe
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   488
  document_files "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   489
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   490
session "HOL-IOA" in IOA = HOL +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   491
  description {*
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   492
    Author:     Tobias Nipkow and Konrad Slind and Olaf Müller
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   493
    Copyright   1994--1996  TU Muenchen
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   494
55417
01fbfb60c33e adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents: 55370
diff changeset
   495
    The meta-theory of I/O-Automata in HOL. This formalization has been
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   496
    significantly changed and extended, see HOLCF/IOA. There are also the
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   497
    proofs of two communication protocols which formerly have been here.
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   498
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   499
    @inproceedings{Nipkow-Slind-IOA,
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   500
    author={Tobias Nipkow and Konrad Slind},
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   501
    title={{I/O} Automata in {Isabelle/HOL}},
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   502
    booktitle={Proc.\ TYPES Workshop 1994},
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   503
    publisher=Springer,
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   504
    series=LNCS,
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   505
    note={To appear}}
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   506
    ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   507
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   508
    and
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   509
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   510
    @inproceedings{Mueller-Nipkow,
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   511
    author={Olaf M\"uller and Tobias Nipkow},
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   512
    title={Combining Model Checking and Deduction for {I/O}-Automata},
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   513
    booktitle={Proc.\ TACAS Workshop},
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   514
    organization={Aarhus University, BRICS report},
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   515
    year=1995}
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   516
    ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   517
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   518
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   519
  theories Solve
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   520
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   521
session "HOL-Lattice" in Lattice = HOL +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   522
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   523
    Author:     Markus Wenzel, TU Muenchen
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   524
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   525
    Basic theory of lattices and orders.
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   526
  *}
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   527
  theories CompleteLattice
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   528
  document_files "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   529
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   530
session "HOL-ex" in ex = HOL +
51421
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   531
  description {*
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   532
    Miscellaneous examples for Higher-Order Logic.
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   533
  *}
58423
e4d540c0dd57 clarified timeout for isatest;
wenzelm
parents: 58419
diff changeset
   534
  options [condition = ML_SYSTEM_POLYML]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   535
  theories [document = false]
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   536
    "~~/src/HOL/Library/State_Monad"
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents: 49985
diff changeset
   537
    Code_Binary_Nat_examples
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   538
    "~~/src/HOL/Library/FuncSet"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   539
    Eval_Examples
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   540
    Normalization_by_Evaluation
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   541
    Hebrew
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   542
    Chinese
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   543
    Serbian
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   544
    "~~/src/HOL/Library/FinFun_Syntax"
49985
5b4b0e4e5205 moved Refute to "HOL/Library" to speed up building "Main" even more
blanchet
parents: 49932
diff changeset
   545
    "~~/src/HOL/Library/Refute"
56922
d411a81b8356 removed junk from library theory
haftmann
parents: 56818
diff changeset
   546
    "~~/src/HOL/Library/Transitive_Closure_Table"
55123
a389b50e6a42 no document for Cartouche_Examples: avoid problems typesetting "\001";
wenzelm
parents: 55075
diff changeset
   547
    Cartouche_Examples
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   548
  theories
59090
a0a05a4edb36 more examples;
wenzelm
parents: 59006
diff changeset
   549
    Commands
57507
a609065c9e15 revived unchecked theory (see cebaf814ca6e);
wenzelm
parents: 57434
diff changeset
   550
    Adhoc_Overloading_Examples
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   551
    Iff_Oracle
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   552
    Coercion_Examples
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   553
    Abstract_NAT
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   554
    Guess
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   555
    Fundefs
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   556
    Induction_Schema
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   557
    LocaleTest2
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   558
    Records
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   559
    While_Combinator_Example
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   560
    MonoidGroup
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   561
    BinEx
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   562
    Hex_Bin_Examples
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   563
    Antiquote
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   564
    Multiquote
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   565
    PER
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   566
    NatSum
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   567
    ThreeDivides
59190
3a594fd13ca4 3 old example lemmas by Amine listed in the top 100 theorems
kleing
parents: 59162
diff changeset
   568
    Cubic_Quartic
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents: 59667
diff changeset
   569
    Pythagoras
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   570
    Intuitionistic
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   571
    CTL
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   572
    Arith_Examples
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   573
    Tree23
58644
8171ef293634 New example Bubblesort
nipkow
parents: 58630
diff changeset
   574
    Bubblesort
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   575
    MergeSort
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   576
    Lagrange
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   577
    Groebner_Examples
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   578
    Unification
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   579
    Primrec
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   580
    Tarski
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   581
    Classical
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   582
    Set_Theory
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   583
    Termination
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   584
    Coherent
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   585
    PresburgerEx
51093
9d7aa2bb097b tuned, particulary name
haftmann
parents: 50988
diff changeset
   586
    Reflection_Examples
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   587
    Sqrt
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   588
    Sqrt_Script
61368
33a62b54f381 add a file with examples of debugging transfer
kuncar
parents: 61232
diff changeset
   589
    Transfer_Debug
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   590
    Transfer_Ex
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   591
    Transfer_Int_Nat
56922
d411a81b8356 removed junk from library theory
haftmann
parents: 56818
diff changeset
   592
    Transitive_Closure_Table_Ex
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   593
    HarmonicSeries
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   594
    Refute_Examples
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   595
    Execute_Choice
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   596
    Gauge_Integration
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   597
    Dedekind_Real
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   598
    Quicksort
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   599
    Birthday_Paradox
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   600
    List_to_Set_Comprehension_Examples
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   601
    Seq
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   602
    Simproc_Tests
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   603
    Executable_Relation
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   604
    FinFunPred
55663
12448c179851 more standard theory name;
wenzelm
parents: 55601
diff changeset
   605
    Set_Comprehension_Pointfree_Examples
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   606
    Parallel_Example
50138
ca989d793b34 new theory of immutable arrays
nipkow
parents: 50050
diff changeset
   607
    IArray_Examples
53430
d92578436d47 added examples for Simps_Case_Conv
noschinl
parents: 53306
diff changeset
   608
    Simps_Case_Conv_Examples
53935
59c6dbdf0a38 added Isabelle/ML example;
wenzelm
parents: 53808
diff changeset
   609
    ML
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents: 59667
diff changeset
   610
    Rewrite_Examples
56815
848d507584db added internal proof-producing SAT solver
boehmes
parents: 56801
diff changeset
   611
    SAT_Examples
58630
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58626
diff changeset
   612
    SOS
58418
a04b242a7a01 clarified SOS tool setup vs. examples;
wenzelm
parents: 58415
diff changeset
   613
    SOS_Cert
60603
09ecbd791d4a add examples from Freek's top 100 theorems (thms 30, 73, 77)
bulwahn
parents: 60470
diff changeset
   614
    Ballot
09ecbd791d4a add examples from Freek's top 100 theorems (thms 30, 73, 77)
bulwahn
parents: 60470
diff changeset
   615
    Erdoes_Szekeres
09ecbd791d4a add examples from Freek's top 100 theorems (thms 30, 73, 77)
bulwahn
parents: 60470
diff changeset
   616
    Sum_of_Powers
62285
747fc3692fca unconditional test -- nothing special here;
wenzelm
parents: 62242
diff changeset
   617
    Sudoku
51558
91f8bed6d0a4 allow build with skip_proofs enabled -- disable it for sessions that would fail due to embedded diagnostic commands, for example;
wenzelm
parents: 51553
diff changeset
   618
  theories [skip_proofs = false]
91f8bed6d0a4 allow build with skip_proofs enabled -- disable it for sessions that would fail due to embedded diagnostic commands, for example;
wenzelm
parents: 51553
diff changeset
   619
    Meson_Test
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   620
  document_files "root.bib" "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   621
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   622
session "HOL-Isar_Examples" in Isar_Examples = HOL +
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   623
  description {*
61935
6512e84cc9f5 clarified sessions;
wenzelm
parents: 61793
diff changeset
   624
    Miscellaneous Isabelle/Isar examples.
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   625
  *}
61939
3c8c390a8f0a tuned document;
wenzelm
parents: 61938
diff changeset
   626
  options [quick_and_dirty]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   627
  theories [document = false]
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   628
    "~~/src/HOL/Library/Lattice_Syntax"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   629
    "../Number_Theory/Primes"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   630
  theories
61939
3c8c390a8f0a tuned document;
wenzelm
parents: 61938
diff changeset
   631
    Knaster_Tarski
3c8c390a8f0a tuned document;
wenzelm
parents: 61938
diff changeset
   632
    Peirce
3c8c390a8f0a tuned document;
wenzelm
parents: 61938
diff changeset
   633
    Drinker
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   634
    Cantor
61938
e1205f814159 more proofs;
wenzelm
parents: 61935
diff changeset
   635
    Schroeder_Bernstein
61939
3c8c390a8f0a tuned document;
wenzelm
parents: 61938
diff changeset
   636
    Structured_Statements
3c8c390a8f0a tuned document;
wenzelm
parents: 61938
diff changeset
   637
    Basic_Logic
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   638
    Expr_Compiler
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   639
    Fibonacci
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   640
    Group
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   641
    Group_Context
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   642
    Group_Notepad
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   643
    Hoare_Ex
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   644
    Mutilated_Checkerboard
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   645
    Puzzle
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   646
    Summation
61935
6512e84cc9f5 clarified sessions;
wenzelm
parents: 61793
diff changeset
   647
    First_Order_Logic
6512e84cc9f5 clarified sessions;
wenzelm
parents: 61793
diff changeset
   648
    Higher_Order_Logic
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   649
  document_files
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   650
    "root.bib"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   651
    "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   652
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents: 60008
diff changeset
   653
session "HOL-Eisbach" in Eisbach = HOL +
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents: 60008
diff changeset
   654
  description {*
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents: 60008
diff changeset
   655
    The Eisbach proof method language and "match" method.
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents: 60008
diff changeset
   656
  *}
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents: 60008
diff changeset
   657
  theories
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents: 60008
diff changeset
   658
    Eisbach
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents: 60008
diff changeset
   659
    Tests
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents: 60008
diff changeset
   660
    Examples
62168
e97452d79102 Eisbach works for other object-logics, e.g. Eisbach_FOL.thy;
wenzelm
parents: 62155
diff changeset
   661
    Examples_FOL
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents: 60008
diff changeset
   662
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   663
session "HOL-SET_Protocol" in SET_Protocol = HOL +
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   664
  description {*
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   665
    Verification of the SET Protocol.
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   666
  *}
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   667
  theories [document = false] "~~/src/HOL/Library/Nat_Bijection"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   668
  theories SET_Protocol
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   669
  document_files "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   670
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   671
session "HOL-Matrix_LP" in Matrix_LP = HOL +
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   672
  description {*
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   673
    Two-dimensional matrices and linear programming.
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   674
  *}
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   675
  theories Cplex
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   676
  document_files "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   677
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   678
session "HOL-TLA" in TLA = HOL +
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   679
  description {*
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   680
    Lamport's Temporal Logic of Actions.
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   681
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   682
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   683
  theories TLA
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   684
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   685
session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" +
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   686
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   687
  theories Inc
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   688
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   689
session "HOL-TLA-Buffer" in "TLA/Buffer" = "HOL-TLA" +
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   690
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   691
  theories DBuffer
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   692
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   693
session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" +
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   694
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   695
  theories MemoryImplementation
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   696
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   697
session "HOL-TPTP" in TPTP = HOL +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   698
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   699
    Author:     Jasmin Blanchette, TU Muenchen
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   700
    Author:     Nik Sultana, University of Cambridge
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   701
    Copyright   2011
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   702
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   703
    TPTP-related extensions.
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   704
  *}
59992
d8db5172c23f make SML/NJ more happy;
wenzelm
parents: 59973
diff changeset
   705
  options [condition = ML_SYSTEM_POLYML, document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   706
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   707
    ATP_Theory_Export
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   708
    MaSh_Eval
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   709
    TPTP_Interpret
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   710
    THF_Arith
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents: 55450
diff changeset
   711
    TPTP_Proof_Reconstruction
52488
cd65ee49a8ba discontinued system option "proofs" -- global state of Proofterm.proofs is persistently compiled into HOL-Proofs image;
wenzelm
parents: 52424
diff changeset
   712
  theories
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   713
    ATP_Problem_Import
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   714
50844
b95ff3744815 populate "main" session group, e.g. relevant for Isabelle/jEdit logic selection;
wenzelm
parents: 50833
diff changeset
   715
session "HOL-Multivariate_Analysis" (main) in Multivariate_Analysis = HOL +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   716
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   717
    Multivariate_Analysis
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   718
    Determinants
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents: 56079
diff changeset
   719
    PolyRoots
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents: 56079
diff changeset
   720
    Complex_Analysis_Basics
59741
5b762cd73a8e Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents: 59667
diff changeset
   721
    Complex_Transcendental
60809
457abb82fb9e the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents: 60804
diff changeset
   722
    Cauchy_Integral_Thm
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   723
  document_files
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   724
    "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   725
59922
1b6283aa7c94 rearranged sessions to save approx. 1min elapsed time, 5min CPU time;
wenzelm
parents: 59903
diff changeset
   726
session "HOL-Multivariate_Analysis-ex" in "Multivariate_Analysis/ex" = "HOL-Multivariate_Analysis" +
1b6283aa7c94 rearranged sessions to save approx. 1min elapsed time, 5min CPU time;
wenzelm
parents: 59903
diff changeset
   727
  theories
1b6283aa7c94 rearranged sessions to save approx. 1min elapsed time, 5min CPU time;
wenzelm
parents: 59903
diff changeset
   728
    Approximations
1b6283aa7c94 rearranged sessions to save approx. 1min elapsed time, 5min CPU time;
wenzelm
parents: 59903
diff changeset
   729
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   730
session "HOL-Probability" in "Probability" = "HOL-Multivariate_Analysis" +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   731
  theories [document = false]
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   732
    "~~/src/HOL/Library/Countable"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   733
    "~~/src/HOL/Library/Permutation"
56994
8d5e5ec1cac3 fixed document generation for HOL-Probability
hoelzl
parents: 56940
diff changeset
   734
    "~~/src/HOL/Library/Order_Continuity"
8d5e5ec1cac3 fixed document generation for HOL-Probability
hoelzl
parents: 56940
diff changeset
   735
    "~~/src/HOL/Library/Diagonal_Subsequence"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   736
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   737
    Probability
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   738
  document_files "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   739
61946
844881193616 put example into separate session, to restrict precious session image to library theories
haftmann
parents: 61939
diff changeset
   740
session "HOL-Probability-ex" in "Probability/ex" = "HOL-Probability" +
844881193616 put example into separate session, to restrict precious session image to library theories
haftmann
parents: 61939
diff changeset
   741
  theories
844881193616 put example into separate session, to restrict precious session image to library theories
haftmann
parents: 61939
diff changeset
   742
    "Dining_Cryptographers"
844881193616 put example into separate session, to restrict precious session image to library theories
haftmann
parents: 61939
diff changeset
   743
    "Koepf_Duermuth_Countermeasure"
844881193616 put example into separate session, to restrict precious session image to library theories
haftmann
parents: 61939
diff changeset
   744
    "Measure_Not_CCC"
844881193616 put example into separate session, to restrict precious session image to library theories
haftmann
parents: 61939
diff changeset
   745
59898
81c70bdbd908 clarified "main" group, e.g. relevant for Isabelle/jEdit menu;
wenzelm
parents: 59810
diff changeset
   746
session "HOL-Nominal" in Nominal = HOL +
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   747
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   748
  theories Nominal
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   749
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   750
session "HOL-Nominal-Examples" in "Nominal/Examples" = "HOL-Nominal" +
58423
e4d540c0dd57 clarified timeout for isatest;
wenzelm
parents: 58419
diff changeset
   751
  options [condition = ML_SYSTEM_POLYML, document = false]
58329
a31404ec7414 run larger nominal examples only 'ISABELLE_FULL_TEST'
blanchet
parents: 58313
diff changeset
   752
  theories
59162
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   753
    Class3
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   754
    CK_Machine
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   755
    Compile
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   756
    Contexts
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   757
    Crary
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   758
    CR_Takahashi
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   759
    CR
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   760
    Fsub
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   761
    Height
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   762
    Lambda_mu
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   763
    Lam_Funs
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   764
    LocalWeakening
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   765
    Pattern
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   766
    SN
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   767
    SOS
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   768
    Standardization
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   769
    Support
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   770
    Type_Preservation
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   771
    Weakening
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   772
    W
58329
a31404ec7414 run larger nominal examples only 'ISABELLE_FULL_TEST'
blanchet
parents: 58313
diff changeset
   773
  theories [quick_and_dirty]
a31404ec7414 run larger nominal examples only 'ISABELLE_FULL_TEST'
blanchet
parents: 58313
diff changeset
   774
    VC_Condition
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   775
55054
e1f3714bc508 moved subset of 'HOL-Cardinals' needed for BNF into 'HOL'
blanchet
parents: 55033
diff changeset
   776
session "HOL-Cardinals" in Cardinals = HOL +
51421
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   777
  description {*
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   778
    Ordinals and Cardinals, Full Theories.
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   779
  *}
49511
9f5bfef8bd82 created separate session "HOL-BNF-LFP" as a step towards eventual integration in "HOL" in the middle term
blanchet
parents: 49510
diff changeset
   780
  options [document = false]
59747
7325ffa35038 bounded powerset
traytel
parents: 59743
diff changeset
   781
  theories
7325ffa35038 bounded powerset
traytel
parents: 59743
diff changeset
   782
    Cardinals
7325ffa35038 bounded powerset
traytel
parents: 59743
diff changeset
   783
    Bounded_Set
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   784
  document_files
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   785
    "intro.tex"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   786
    "root.tex"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   787
    "root.bib"
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents: 48932
diff changeset
   788
58309
a09ec6daaa19 renamed 'BNF_Examples' to 'Datatype_Examples' (cf. 'datatypes.pdf')
blanchet
parents: 58308
diff changeset
   789
session "HOL-Datatype_Examples" in Datatype_Examples = HOL +
51421
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   790
  description {*
58312
710f56e192fe updated ROOT
blanchet
parents: 58309
diff changeset
   791
    (Co)datatype Examples, including large ones from John Harrison.
51421
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   792
  *}
49932
9d3bc26485eb back to parallel HOL-BNF-Examples, which seems to have suffered from Future.map on canceled persistent futures;
wenzelm
parents: 49903
diff changeset
   793
  options [document = false]
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents: 48932
diff changeset
   794
  theories
58372
bfd497f2f4c2 moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer)
blanchet
parents: 58371
diff changeset
   795
    "~~/src/HOL/Library/Old_Datatype"
56454
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents: 56215
diff changeset
   796
    Compat
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents: 48932
diff changeset
   797
    Lambda_Term
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents: 48932
diff changeset
   798
    Process
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents: 48932
diff changeset
   799
    TreeFsetI
49872
c6a686c9be2a update ROOT with teh directory change in BNF
popescua
parents: 49693
diff changeset
   800
    "Derivation_Trees/Gram_Lang"
c6a686c9be2a update ROOT with teh directory change in BNF
popescua
parents: 49693
diff changeset
   801
    "Derivation_Trees/Parallel"
50517
8f6c11103820 renamed theory
traytel
parents: 50480
diff changeset
   802
    Koenig
60921
487050067be9 actually process lift_bnf regression suite
traytel
parents: 60809
diff changeset
   803
    Lift_BNF
61745
e23e0ff98657 Ported old example to use (co)datatypes
traytel
parents: 61670
diff changeset
   804
    Milner_Tofte
54961
e60428f432bc new codatatype example: stream processors
traytel
parents: 54481
diff changeset
   805
    Stream_Processor
53122
bc87b7af4767 renamed theory files to be closer to (new) command names
blanchet
parents: 52726
diff changeset
   806
    Misc_Codatatype
bc87b7af4767 renamed theory files to be closer to (new) command names
blanchet
parents: 52726
diff changeset
   807
    Misc_Datatype
54193
bc07627c5dcd added 'primcorec' examples
blanchet
parents: 53935
diff changeset
   808
    Misc_Primcorec
53306
45f13517693a added example
blanchet
parents: 53164
diff changeset
   809
    Misc_Primrec
58849
ef7700ecce83 discontinued pointless option: timing is always on (overall theory only);
wenzelm
parents: 58842
diff changeset
   810
  theories [condition = ISABELLE_FULL_TEST]
58308
0ccba1b6d00b move datatype benchmarks
blanchet
parents: 58110
diff changeset
   811
    Brackin
58313
57d2e5006d29 renamed example theory for consistency
blanchet
parents: 58312
diff changeset
   812
    IsaFoR
58433
d518f892cec6 made N2M tests conditional, since they appear to cause Isatest timeouts and are kind of slow
blanchet
parents: 58423
diff changeset
   813
    Misc_N2M
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents: 48932
diff changeset
   814
50844
b95ff3744815 populate "main" session group, e.g. relevant for Isabelle/jEdit logic selection;
wenzelm
parents: 50833
diff changeset
   815
session "HOL-Word" (main) in Word = HOL +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   816
  theories Word
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   817
  document_files "root.bib" "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   818
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   819
session "HOL-Word-Examples" in "Word/Examples" = "HOL-Word" +
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   820
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   821
  theories WordExamples
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   822
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   823
session "HOL-Statespace" in Statespace = HOL +
51558
91f8bed6d0a4 allow build with skip_proofs enabled -- disable it for sessions that would fail due to embedded diagnostic commands, for example;
wenzelm
parents: 51553
diff changeset
   824
  theories [skip_proofs = false]
91f8bed6d0a4 allow build with skip_proofs enabled -- disable it for sessions that would fail due to embedded diagnostic commands, for example;
wenzelm
parents: 51553
diff changeset
   825
    StateSpaceEx
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   826
  document_files "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   827
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   828
session "HOL-NSA" in NSA = HOL +
51421
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   829
  description {*
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   830
    Nonstandard analysis.
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   831
  *}
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   832
  theories Hypercomplex
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   833
  document_files "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   834
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   835
session "HOL-NSA-Examples" in "NSA/Examples" = "HOL-NSA" +
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   836
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   837
  theories NSPrimes
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   838
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   839
session "HOL-Mirabelle" in Mirabelle = HOL +
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   840
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   841
  theories Mirabelle_Test
48589
fb446a780d50 separate session HOL-Mirabelle-ex -- cannot run isolated shell scripts within build tool;
wenzelm
parents: 48588
diff changeset
   842
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   843
session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
60008
dfbd51a5eab1 make SML/NJ more happy;
wenzelm
parents: 59992
diff changeset
   844
  options [condition = ML_SYSTEM_POLYML, document = false, timeout = 60]
49448
8a232a4e3fd8 reactivate HOL-Mirabelle-ex with increased chances that it works most of the time (cf. bec1add86e79, a93d920707bb, be27a453aacc);
wenzelm
parents: 49439
diff changeset
   845
  theories Ex
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   846
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   847
session "HOL-Word-SMT_Examples" in SMT_Examples = "HOL-Word" +
62242
a4e6ea45f416 guard sessions that no longer work with SML/NJ -- memory problems;
wenzelm
parents: 62168
diff changeset
   848
  options [condition = ML_SYSTEM_POLYML, document = false, quick_and_dirty]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   849
  theories
52722
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents: 52499
diff changeset
   850
    Boogie
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   851
    SMT_Examples
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   852
    SMT_Word_Examples
50666
6f48853f08d5 actually run Z3 for "SMT_Tests" when "ISABELLE_FULL_TEST" is enabled
blanchet
parents: 50665
diff changeset
   853
    SMT_Tests
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   854
  files
58367
8af1e68d7e1a renamed SMT certificate files, following 'SMT2' -> 'SMT' renaming
blanchet
parents: 58351
diff changeset
   855
    "Boogie_Dijkstra.certs"
8af1e68d7e1a renamed SMT certificate files, following 'SMT2' -> 'SMT' renaming
blanchet
parents: 58351
diff changeset
   856
    "Boogie_Max.certs"
8af1e68d7e1a renamed SMT certificate files, following 'SMT2' -> 'SMT' renaming
blanchet
parents: 58351
diff changeset
   857
    "SMT_Examples.certs"
8af1e68d7e1a renamed SMT certificate files, following 'SMT2' -> 'SMT' renaming
blanchet
parents: 58351
diff changeset
   858
    "SMT_Word_Examples.certs"
8af1e68d7e1a renamed SMT certificate files, following 'SMT2' -> 'SMT' renaming
blanchet
parents: 58351
diff changeset
   859
    "VCC_Max.certs"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   860
50844
b95ff3744815 populate "main" session group, e.g. relevant for Isabelle/jEdit logic selection;
wenzelm
parents: 50833
diff changeset
   861
session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" +
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   862
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   863
  theories SPARK
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   864
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   865
session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
59810
e749a0f2f401 HOL-SPARK .prv files are subject to system option spark_prv;
wenzelm
parents: 59777
diff changeset
   866
  options [document = false, spark_prv = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   867
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   868
    "Gcd/Greatest_Common_Divisor"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   869
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   870
    "Liseq/Longest_Increasing_Subsequence"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   871
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   872
    "RIPEMD-160/F"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   873
    "RIPEMD-160/Hash"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   874
    "RIPEMD-160/K_L"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   875
    "RIPEMD-160/K_R"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   876
    "RIPEMD-160/R_L"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   877
    "RIPEMD-160/Round"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   878
    "RIPEMD-160/R_R"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   879
    "RIPEMD-160/S_L"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   880
    "RIPEMD-160/S_R"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   881
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   882
    "Sqrt/Sqrt"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   883
  files
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   884
    "Gcd/greatest_common_divisor/g_c_d.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   885
    "Gcd/greatest_common_divisor/g_c_d.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   886
    "Gcd/greatest_common_divisor/g_c_d.siv"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   887
    "Liseq/liseq/liseq_length.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   888
    "Liseq/liseq/liseq_length.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   889
    "Liseq/liseq/liseq_length.siv"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   890
    "RIPEMD-160/rmd/f.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   891
    "RIPEMD-160/rmd/f.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   892
    "RIPEMD-160/rmd/f.siv"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   893
    "RIPEMD-160/rmd/hash.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   894
    "RIPEMD-160/rmd/hash.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   895
    "RIPEMD-160/rmd/hash.siv"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   896
    "RIPEMD-160/rmd/k_l.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   897
    "RIPEMD-160/rmd/k_l.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   898
    "RIPEMD-160/rmd/k_l.siv"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   899
    "RIPEMD-160/rmd/k_r.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   900
    "RIPEMD-160/rmd/k_r.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   901
    "RIPEMD-160/rmd/k_r.siv"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   902
    "RIPEMD-160/rmd/r_l.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   903
    "RIPEMD-160/rmd/r_l.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   904
    "RIPEMD-160/rmd/r_l.siv"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   905
    "RIPEMD-160/rmd/round.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   906
    "RIPEMD-160/rmd/round.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   907
    "RIPEMD-160/rmd/round.siv"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   908
    "RIPEMD-160/rmd/r_r.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   909
    "RIPEMD-160/rmd/r_r.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   910
    "RIPEMD-160/rmd/r_r.siv"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   911
    "RIPEMD-160/rmd/s_l.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   912
    "RIPEMD-160/rmd/s_l.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   913
    "RIPEMD-160/rmd/s_l.siv"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   914
    "RIPEMD-160/rmd/s_r.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   915
    "RIPEMD-160/rmd/s_r.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   916
    "RIPEMD-160/rmd/s_r.siv"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   917
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   918
session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +
59810
e749a0f2f401 HOL-SPARK .prv files are subject to system option spark_prv;
wenzelm
parents: 59777
diff changeset
   919
  options [show_question_marks = false, spark_prv = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   920
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   921
    Example_Verification
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   922
    VC_Principles
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   923
    Reference
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   924
    Complex_Types
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   925
  files
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   926
    "complex_types_app/initialize.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   927
    "complex_types_app/initialize.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   928
    "complex_types_app/initialize.siv"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   929
    "loop_invariant/proc1.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   930
    "loop_invariant/proc1.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   931
    "loop_invariant/proc1.siv"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   932
    "loop_invariant/proc2.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   933
    "loop_invariant/proc2.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   934
    "loop_invariant/proc2.siv"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   935
    "simple_greatest_common_divisor/g_c_d.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   936
    "simple_greatest_common_divisor/g_c_d.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   937
    "simple_greatest_common_divisor/g_c_d.siv"
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   938
  document_files
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   939
    "complex_types.ads"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   940
    "complex_types_app.adb"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   941
    "complex_types_app.ads"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   942
    "Gcd.adb"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   943
    "Gcd.ads"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   944
    "intro.tex"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   945
    "loop_invariant.adb"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   946
    "loop_invariant.ads"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   947
    "root.bib"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   948
    "root.tex"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   949
    "Simple_Gcd.adb"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   950
    "Simple_Gcd.ads"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   951
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   952
session "HOL-Mutabelle" in Mutabelle = HOL +
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   953
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   954
  theories MutabelleExtra
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   955
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   956
session "HOL-Quickcheck_Examples" in Quickcheck_Examples = HOL +
50179
978200ae8473 timeout in proper place (HOL-Quickcheck_Examples approx. 1min, HOL-Quickcheck_Benchmark approx. 1h);
wenzelm
parents: 50161
diff changeset
   957
  options [document = false]
48588
23456b2a769d added Quickcheck_Benchmark (cf. 1959baa22632);
wenzelm
parents: 48512
diff changeset
   958
  theories
48690
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
   959
    Quickcheck_Examples
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
   960
    Quickcheck_Lattice_Examples
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
   961
    Completeness
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
   962
    Quickcheck_Interfaces
57584
155b7e3b729e proper condition wrt. ISABELLE_GHC (cf. 8840fa17e17c);
wenzelm
parents: 57544
diff changeset
   963
  theories [condition = ISABELLE_GHC]
57544
8840fa17e17c reactivate session Quickcheck_Examples
Andreas Lochbihler
parents: 57543
diff changeset
   964
    Hotel_Example
48598
7f4561d43d39 updated ROOT according to 3defa60a7ae3;
wenzelm
parents: 48589
diff changeset
   965
    Quickcheck_Narrowing_Examples
48588
23456b2a769d added Quickcheck_Benchmark (cf. 1959baa22632);
wenzelm
parents: 48512
diff changeset
   966
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   967
session "HOL-Quickcheck_Benchmark" in Quickcheck_Benchmark = HOL +
50571
b649e33e4821 HOL-Quickcheck_Benchmark works without timeout (NB: isatest imposes global timeout already);
wenzelm
parents: 50568
diff changeset
   968
  theories [condition = ISABELLE_FULL_TEST, quick_and_dirty]
50568
ee090b5712f3 reverting d466ebc27810 as the previous changeset should allow to run Find_Unused_Assms_Examples again
bulwahn
parents: 50517
diff changeset
   969
    Find_Unused_Assms_Examples
48618
1f7e068b4613 moved another larger quickcheck example to Quickcheck_Benchmark
bulwahn
parents: 48614
diff changeset
   970
    Needham_Schroeder_No_Attacker_Example
1f7e068b4613 moved another larger quickcheck example to Quickcheck_Benchmark
bulwahn
parents: 48614
diff changeset
   971
    Needham_Schroeder_Guided_Attacker_Example
48690
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
   972
    Needham_Schroeder_Unguided_Attacker_Example
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   973
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   974
session "HOL-Quotient_Examples" in Quotient_Examples = HOL +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   975
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   976
    Author:     Cezary Kaliszyk and Christian Urban
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   977
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   978
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   979
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   980
    DList
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   981
    FSet
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   982
    Quotient_Int
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   983
    Quotient_Message
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   984
    Lift_FSet
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   985
    Lift_Set
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   986
    Lift_Fun
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   987
    Quotient_Rat
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   988
    Lift_DList
53682
1b55aeda0e46 include Int_Pow into Quotient_Examples; add end of the theory
kuncar
parents: 53430
diff changeset
   989
    Int_Pow
60237
d47387d4a3c6 add testing file for code_dt extension of lifting
kuncar
parents: 60119
diff changeset
   990
    Lifting_Code_Dt_Test
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   991
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   992
session "HOL-Predicate_Compile_Examples" in Predicate_Compile_Examples = HOL +
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   993
  options [document = false]
62242
a4e6ea45f416 guard sessions that no longer work with SML/NJ -- memory problems;
wenzelm
parents: 62168
diff changeset
   994
  theories [condition = ML_SYSTEM_POLYML]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   995
    Examples
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   996
    Predicate_Compile_Tests
61140
78ece168f5b5 reactivate examples with predicate compiler and quickcheck
Andreas Lochbihler
parents: 60921
diff changeset
   997
    Predicate_Compile_Quickcheck_Examples
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   998
    Specialisation_Examples
48690
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
   999
    IMP_1
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
  1000
    IMP_2
55450
9eddc17749f7 reactivate some examples that still appear to work;
wenzelm
parents: 55447
diff changeset
  1001
    (* FIXME since 21-Jul-2011
61140
78ece168f5b5 reactivate examples with predicate compiler and quickcheck
Andreas Lochbihler
parents: 60921
diff changeset
  1002
    Hotel_Example_Small_Generator *)
48690
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
  1003
    IMP_3
61140
78ece168f5b5 reactivate examples with predicate compiler and quickcheck
Andreas Lochbihler
parents: 60921
diff changeset
  1004
    IMP_4
62242
a4e6ea45f416 guard sessions that no longer work with SML/NJ -- memory problems;
wenzelm
parents: 62168
diff changeset
  1005
  theories [condition = ISABELLE_SWIPL]
48690
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
  1006
    Code_Prolog_Examples
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
  1007
    Context_Free_Grammar_Example
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
  1008
    Hotel_Example_Prolog
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
  1009
    Lambda_Example
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
  1010
    List_Examples
62242
a4e6ea45f416 guard sessions that no longer work with SML/NJ -- memory problems;
wenzelm
parents: 62168
diff changeset
  1011
  theories [condition = ISABELLE_SWIPL, quick_and_dirty]
48690
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
  1012
    Reg_Exp_Example
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1013
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
  1014
session HOLCF (main) in HOLCF = HOL +
48338
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
  1015
  description {*
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
  1016
    Author:     Franz Regensburger
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
  1017
    Author:     Brian Huffman
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
  1018
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
  1019
    HOLCF -- a semantic extension of HOL by the LCF logic.
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
  1020
  *}
48470
7483aa690b4f clarified "document" again, eliminated redundant "no_document";
wenzelm
parents: 48458
diff changeset
  1021
  theories [document = false]
48338
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
  1022
    "~~/src/HOL/Library/Nat_Bijection"
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
  1023
    "~~/src/HOL/Library/Countable"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1024
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1025
    Plain_HOLCF
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1026
    Fixrec
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1027
    HOLCF
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
  1028
  document_files "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1029
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
  1030
session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1031
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1032
    Domain_ex
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1033
    Fixrec_ex
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1034
    New_Domain
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
  1035
  document_files "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1036
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
  1037
session "HOLCF-Library" in "HOLCF/Library" = HOLCF +
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
  1038
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1039
  theories HOLCF_Library
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1040
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
  1041
session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF +
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1042
  description {*
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1043
    IMP -- A WHILE-language and its Semantics.
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1044
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1045
    This is the HOLCF-based denotational semantics of a simple WHILE-language.
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1046
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
  1047
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1048
  theories HoareEx
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
  1049
  document_files "root.tex"
48338
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
  1050
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
  1051
session "HOLCF-ex" in "HOLCF/ex" = HOLCF +
51421
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
  1052
  description {*
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
  1053
    Miscellaneous examples for HOLCF.
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
  1054
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
  1055
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1056
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1057
    Dnat
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1058
    Dagstuhl
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1059
    Focus_ex
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1060
    Fix2
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1061
    Hoare
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1062
    Concurrency_Monad
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1063
    Loop
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1064
    Powerdomain_ex
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1065
    Domain_Proofs
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1066
    Letrec
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1067
    Pattern_Match
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1068
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
  1069
session "HOLCF-FOCUS" in "HOLCF/FOCUS" = HOLCF +
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1070
  description {*
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1071
    FOCUS: a theory of stream-processing functions Isabelle/HOLCF.
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1072
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1073
    For introductions to FOCUS, see
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1074
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1075
    "The Design of Distributed Systems - An Introduction to FOCUS"
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1076
    http://www4.in.tum.de/publ/html.php?e=2
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1077
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1078
    "Specification and Refinement of a Buffer of Length One"
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1079
    http://www4.in.tum.de/publ/html.php?e=15
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1080
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1081
    "Specification and Development of Interactive Systems: Focus on Streams,
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1082
    Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1083
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
  1084
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1085
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1086
    Fstreams
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1087
    FOCUS
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1088
    Buffer_adm
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1089
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
  1090
session IOA in "HOLCF/IOA" = HOLCF +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1091
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1092
    Author:     Olaf Mueller
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1093
    Copyright   1997 TU München
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1094
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1095
    A formalization of I/O automata in HOLCF.
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1096
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1097
    The distribution contains simulation relations, temporal logic, and an
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1098
    abstraction theory. Everything is based upon a domain-theoretic model of
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1099
    finite and infinite sequences.
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1100
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
  1101
  options [document = false]
62008
cbedaddc9351 clarified directory structure;
wenzelm
parents: 61946
diff changeset
  1102
  theories "Abstraction"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1103
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
  1104
session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1105
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1106
    Author:     Olaf Mueller
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1107
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1108
    The Alternating Bit Protocol performed in I/O-Automata.
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1109
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
  1110
  options [document = false]
59503
9937bc07202b check unused theory;
wenzelm
parents: 59446
diff changeset
  1111
  theories
9937bc07202b check unused theory;
wenzelm
parents: 59446
diff changeset
  1112
    Correctness
9937bc07202b check unused theory;
wenzelm
parents: 59446
diff changeset
  1113
    Spec
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1114
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
  1115
session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1116
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1117
    Author:     Tobias Nipkow & Konrad Slind
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1118
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1119
    A network transmission protocol, performed in the
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1120
    I/O automata formalization by Olaf Mueller.
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1121
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
  1122
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1123
  theories Correctness
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1124
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
  1125
session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1126
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1127
    Author:     Olaf Mueller
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1128
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1129
    Memory storage case study.
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1130
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
  1131
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1132
  theories Correctness
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1133
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
  1134
session "IOA-ex" in "HOLCF/IOA/ex" = IOA +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1135
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1136
    Author:     Olaf Mueller
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1137
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
  1138
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1139
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1140
    TrivEx
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1141
    TrivEx2
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1142
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
  1143
session "HOL-Record_Benchmark" in Record_Benchmark = HOL +
51421
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
  1144
  description {*
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
  1145
    Some benchmark on large record.
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
  1146
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
  1147
  options [document = false]
58849
ef7700ecce83 discontinued pointless option: timing is always on (overall theory only);
wenzelm
parents: 58842
diff changeset
  1148
  theories [condition = ISABELLE_FULL_TEST]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1149
    Record_Benchmark
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1150