src/HOL/ROOT
author wenzelm
Thu, 17 Aug 2017 14:40:42 +0200
changeset 66445 407de0768126
parent 66444 6d2d993fa76e
child 66453 cc19f7ca2ed6
permissions -rw-r--r--
more complete session (amending e77ea0ea7f2c);
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
  *}
65374
a5b38d8d3c1e tuned syntax;
wenzelm
parents: 65099
diff changeset
     7
  theories
a5b38d8d3c1e tuned syntax;
wenzelm
parents: 65099
diff changeset
     8
    Main (global)
a5b38d8d3c1e tuned syntax;
wenzelm
parents: 65099
diff changeset
     9
    Complex_Main (global)
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
63888
5a9a1985e9fb sessions that are relevant for routine timing measurements;
wenzelm
parents: 63885
diff changeset
    17
session "HOL-Proofs" (timing) = 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
  *}
65456
31e8a86971a8 explicit theory qualifier for session "HOL-Proofs": its theory name space overlaps with session "HOL", even for further imports;
wenzelm
parents: 65448
diff changeset
    21
  options [document = false, theory_qualifier = "HOL",
31e8a86971a8 explicit theory qualifier for session "HOL-Proofs": its theory name space overlaps with session "HOL", even for further imports;
wenzelm
parents: 65448
diff changeset
    22
    quick_and_dirty = false, record_proofs = 2, parallel_proofs = 0]
65543
8369b33fda0a clarified session imports;
wenzelm
parents: 65538
diff changeset
    23
  sessions
8369b33fda0a clarified session imports;
wenzelm
parents: 65538
diff changeset
    24
    "HOL-Library"
65530
09c00a304c00 include imports that morally belong to Main and are used in HOL-Proofs applications;
wenzelm
parents: 65509
diff changeset
    25
  theories
09c00a304c00 include imports that morally belong to Main and are used in HOL-Proofs applications;
wenzelm
parents: 65509
diff changeset
    26
    "HOL-Library.Old_Datatype"
48901
5e0455e29339 more basic file dependencies -- no load command here;
wenzelm
parents: 48765
diff changeset
    27
  files
5e0455e29339 more basic file dependencies -- no load command here;
wenzelm
parents: 48765
diff changeset
    28
    "Tools/Quickcheck/Narrowing_Engine.hs"
5e0455e29339 more basic file dependencies -- no load command here;
wenzelm
parents: 48765
diff changeset
    29
    "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
48338
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
    30
63888
5a9a1985e9fb sessions that are relevant for routine timing measurements;
wenzelm
parents: 63885
diff changeset
    31
session "HOL-Library" (main timing) in Library = HOL +
51421
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
    32
  description {*
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
    33
    Classical Higher-order Logic -- batteries included.
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
    34
  *}
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    35
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    36
    Library
64588
293ab573d034 clarified library contents
haftmann
parents: 64582
diff changeset
    37
    (*conflicting type class instantiations and dependent applications*)
293ab573d034 clarified library contents
haftmann
parents: 64582
diff changeset
    38
    Finite_Lattice
293ab573d034 clarified library contents
haftmann
parents: 64582
diff changeset
    39
    List_lexord
63763
0f61ea70d384 clarified session: use all theories in directory HOL/Library;
wenzelm
parents: 63731
diff changeset
    40
    Prefix_Order
51115
7dbd6832a689 consolidation of library theories on product orders
haftmann
parents: 51093
diff changeset
    41
    Product_Lexorder
7dbd6832a689 consolidation of library theories on product orders
haftmann
parents: 51093
diff changeset
    42
    Product_Order
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 65678
diff changeset
    43
    Subseq_Order
51161
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51160
diff changeset
    44
    (*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
    45
    AList_Mapping
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51160
diff changeset
    46
    Code_Binary_Nat
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51160
diff changeset
    47
    Code_Char
55447
aa41ecbdc205 do not redefine outer syntax commands;
wenzelm
parents: 55417
diff changeset
    48
    Code_Prolog
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    49
    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
    50
    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
    51
    DAList
54429
be1bc181bcde explicit inclusion of data refinement theory into HOL-Library session
haftmann
parents: 54193
diff changeset
    52
    DAList_Multiset
51161
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51160
diff changeset
    53
    RBT_Mapping
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51160
diff changeset
    54
    RBT_Set
66015
70643edecb7a specific output setup is not supposed to intrude regular import theory
haftmann
parents: 65956
diff changeset
    55
    (*printing modifications*)
70643edecb7a specific output setup is not supposed to intrude regular import theory
haftmann
parents: 65956
diff changeset
    56
    OptionalSugar
64588
293ab573d034 clarified library contents
haftmann
parents: 64582
diff changeset
    57
    (*prototypic tools*)
293ab573d034 clarified library contents
haftmann
parents: 64582
diff changeset
    58
    Predicate_Compile_Quickcheck
51161
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51160
diff changeset
    59
    (*legacy tools*)
58372
bfd497f2f4c2 moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer)
blanchet
parents: 58371
diff changeset
    60
    Old_Datatype
51161
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51160
diff changeset
    61
    Old_Recdef
64588
293ab573d034 clarified library contents
haftmann
parents: 64582
diff changeset
    62
    Refute
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
    63
  document_files "root.bib" "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    64
65550
e957b1f00449 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65549
diff changeset
    65
session "HOL-Analysis" (main timing) in Analysis = "HOL-Computational_Algebra" +
65375
wenzelm
parents: 65374
diff changeset
    66
  theories
65462
db1827610513 less global theories -- conflict with AFP entries;
wenzelm
parents: 65456
diff changeset
    67
    Analysis
65375
wenzelm
parents: 65374
diff changeset
    68
  document_files
wenzelm
parents: 65374
diff changeset
    69
    "root.tex"
wenzelm
parents: 65374
diff changeset
    70
wenzelm
parents: 65374
diff changeset
    71
session "HOL-Analysis-ex" in "Analysis/ex" = "HOL-Analysis" +
wenzelm
parents: 65374
diff changeset
    72
  theories
wenzelm
parents: 65374
diff changeset
    73
    Approximations
wenzelm
parents: 65374
diff changeset
    74
    Circle_Area
wenzelm
parents: 65374
diff changeset
    75
65678
aaba2e0c247c more timing;
wenzelm
parents: 65576
diff changeset
    76
session "HOL-Computational_Algebra" (timing) in "Computational_Algebra" = "HOL-Library" +
65417
fc41a5650fb1 session containing computational algebra
haftmann
parents: 65416
diff changeset
    77
  theories
fc41a5650fb1 session containing computational algebra
haftmann
parents: 65416
diff changeset
    78
    Computational_Algebra
fc41a5650fb1 session containing computational algebra
haftmann
parents: 65416
diff changeset
    79
    (*conflicting type class instantiations and dependent applications*)
fc41a5650fb1 session containing computational algebra
haftmann
parents: 65416
diff changeset
    80
    Field_as_Ring
fc41a5650fb1 session containing computational algebra
haftmann
parents: 65416
diff changeset
    81
    Polynomial_Factorial
fc41a5650fb1 session containing computational algebra
haftmann
parents: 65416
diff changeset
    82
65550
e957b1f00449 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65549
diff changeset
    83
session "HOL-Hahn_Banach" in Hahn_Banach = "HOL-Library" +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    84
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    85
    Author:     Gertrud Bauer, TU Munich
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    86
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    87
    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
    88
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    89
    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
    90
    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
    91
    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
    92
    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
    93
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    94
    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
    95
    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
    96
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    97
    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
    98
    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
    99
    continous linearform on the whole vectorspace.
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   100
  *}
65573
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   101
  sessions
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   102
    "HOL-Analysis"
65543
8369b33fda0a clarified session imports;
wenzelm
parents: 65538
diff changeset
   103
  theories
8369b33fda0a clarified session imports;
wenzelm
parents: 65538
diff changeset
   104
    Hahn_Banach
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   105
  document_files "root.bib" "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   106
65550
e957b1f00449 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65549
diff changeset
   107
session "HOL-Induct" in Induct = "HOL-Library" +
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   108
  description {*
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   109
    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
   110
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   111
    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
   112
    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
   113
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   114
    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
   115
    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
   116
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   117
    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
   118
    (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
   119
    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
   120
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   121
    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
   122
    mutually recursive relations.
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   123
  *}
58372
bfd497f2f4c2 moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer)
blanchet
parents: 58371
diff changeset
   124
  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
   125
    "~~/src/HOL/Library/Old_Datatype"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   126
  theories [quick_and_dirty]
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   127
    Common_Patterns
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   128
  theories
61935
6512e84cc9f5 clarified sessions;
wenzelm
parents: 61793
diff changeset
   129
    Nested_Datatype
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   130
    QuoDataType
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   131
    QuoNestedDataType
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   132
    Term
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   133
    SList
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   134
    ABexp
65562
f9753d949afc renamed theory to avoid conflict with loaded theory "Tree" from HOL-Library;
wenzelm
parents: 65552
diff changeset
   135
    Infinitely_Branching_Tree
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   136
    Ordinals
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   137
    Sigma_Algebra
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   138
    Comb
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   139
    PropLog
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   140
    Com
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   141
  document_files "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   142
65573
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   143
session "HOL-IMP" (timing) in IMP = "HOL-Library" +
59446
4427f04fca57 discontinued obsolete option "document_graph";
wenzelm
parents: 59190
diff changeset
   144
  options [document_variants = document]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   145
  theories [document = false]
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   146
    "~~/src/HOL/Library/While_Combinator"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   147
    "~~/src/HOL/Library/Char_ord"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   148
    "~~/src/HOL/Library/List_lexord"
51625
bd3358aac5d2 tuned document
nipkow
parents: 51562
diff changeset
   149
    "~~/src/HOL/Library/Quotient_List"
bd3358aac5d2 tuned document
nipkow
parents: 51562
diff changeset
   150
    "~~/src/HOL/Library/Extended"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   151
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   152
    BExp
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   153
    ASM
50050
fac2b27893ff new theory IMP/Finite_Reachable
nipkow
parents: 50023
diff changeset
   154
    Finite_Reachable
52394
fe33d456b36c more canonical name (2)
nipkow
parents: 52363
diff changeset
   155
    Denotational
52400
ded7b9c60dc2 tuned theory name
nipkow
parents: 52394
diff changeset
   156
    Compiler2
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   157
    Poly_Types
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   158
    Sec_Typing
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   159
    Sec_TypingT
52726
ee0bd6bababd merged Def_Init_Sound_X into Def_Init_X
nipkow
parents: 52722
diff changeset
   160
    Def_Init_Big
ee0bd6bababd merged Def_Init_Sound_X into Def_Init_X
nipkow
parents: 52722
diff changeset
   161
    Def_Init_Small
ee0bd6bababd merged Def_Init_Sound_X into Def_Init_X
nipkow
parents: 52722
diff changeset
   162
    Fold
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   163
    Live
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   164
    Live_True
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   165
    Hoare_Examples
63538
d7b5e2a222c2 added new vcg based on existentially quantified while-rule
nipkow
parents: 63537
diff changeset
   166
    Hoare_Sound_Complete
52269
d867812da48b more VC -> VCG
nipkow
parents: 52248
diff changeset
   167
    VCG
52282
c79a3e15779e tuned theory name
nipkow
parents: 52277
diff changeset
   168
    Hoare_Total
63538
d7b5e2a222c2 added new vcg based on existentially quantified while-rule
nipkow
parents: 63537
diff changeset
   169
    VCG_Total_EX
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   170
    Collecting1
48765
fb1ed5230abc special code with lists no longer necessary, use sets
nipkow
parents: 48738
diff changeset
   171
    Collecting_Examples
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   172
    Abs_Int_Tests
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   173
    Abs_Int1_parity
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   174
    Abs_Int1_const
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   175
    Abs_Int3
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   176
    Procs_Dyn_Vars_Dyn
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   177
    Procs_Stat_Vars_Dyn
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   178
    Procs_Stat_Vars_Stat
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   179
    C_like
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   180
    OO
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   181
  document_files "root.bib" "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   182
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   183
session "HOL-IMPP" in IMPP = HOL +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   184
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   185
    Author:     David von Oheimb
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   186
    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
   187
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   188
    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
   189
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   190
    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
   191
    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
   192
    Local Variables" (http://isabelle.in.tum.de/Bali/papers/FSTTCS99.html).
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   193
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   194
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   195
  theories EvenOdd
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   196
63888
5a9a1985e9fb sessions that are relevant for routine timing measurements;
wenzelm
parents: 63885
diff changeset
   197
session "HOL-Data_Structures" (timing) in Data_Structures = HOL +
61203
a8a8eca85801 New subdirectory for functional data structures
nipkow
parents: 61152
diff changeset
   198
  options [document_variants = document]
65573
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   199
  sessions
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   200
    "HOL-Number_Theory"
61203
a8a8eca85801 New subdirectory for functional data structures
nipkow
parents: 61152
diff changeset
   201
  theories [document = false]
65538
a39ef48fbee0 tuned imports;
wenzelm
parents: 65535
diff changeset
   202
    Less_False
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62696
diff changeset
   203
    "~~/src/HOL/Library/Multiset"
64323
nipkow
parents: 64282
diff changeset
   204
    "~~/src/HOL/Number_Theory/Fib"
61203
a8a8eca85801 New subdirectory for functional data structures
nipkow
parents: 61152
diff changeset
   205
  theories
63829
6a05c8cbf7de More on balancing; renamed theory to Balance
nipkow
parents: 63827
diff changeset
   206
    Balance
61203
a8a8eca85801 New subdirectory for functional data structures
nipkow
parents: 61152
diff changeset
   207
    Tree_Map
61232
c46faf9762f7 added AVL and lookup function
nipkow
parents: 61224
diff changeset
   208
    AVL_Map
61224
759b5299a9f2 added red black trees
nipkow
parents: 61203
diff changeset
   209
    RBT_Map
61469
cd82b1023932 added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents: 61368
diff changeset
   210
    Tree23_Map
61514
213556e498c2 added 234-Trees (slow)
nipkow
parents: 61469
diff changeset
   211
    Tree234_Map
61789
9ce1a397410a added Brother12_Map
nipkow
parents: 61784
diff changeset
   212
    Brother12_Map
62130
90a3016a6c12 added AA_Map; tuned titles
nipkow
parents: 62008
diff changeset
   213
    AA_Map
61525
87244a9cfe40 added splay trees
nipkow
parents: 61514
diff changeset
   214
    Splay_Map
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62696
diff changeset
   215
    Leftist_Heap
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents: 66270
diff changeset
   216
    Binomial_Heap
61224
759b5299a9f2 added red black trees
nipkow
parents: 61203
diff changeset
   217
  document_files "root.tex" "root.bib"
61203
a8a8eca85801 New subdirectory for functional data structures
nipkow
parents: 61152
diff changeset
   218
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   219
session "HOL-Import" in Import = HOL +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   220
  theories HOL_Light_Maps
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   221
  theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   222
65550
e957b1f00449 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65549
diff changeset
   223
session "HOL-Number_Theory" (timing) in Number_Theory = "HOL-Computational_Algebra" +
55321
eadea363deb6 Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents: 55240
diff changeset
   224
  description {*
eadea363deb6 Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents: 55240
diff changeset
   225
    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
   226
    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
   227
  *}
65543
8369b33fda0a clarified session imports;
wenzelm
parents: 65538
diff changeset
   228
  sessions
8369b33fda0a clarified session imports;
wenzelm
parents: 65538
diff changeset
   229
    "HOL-Algebra"
55321
eadea363deb6 Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents: 55240
diff changeset
   230
  theories [document = false]
eadea363deb6 Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents: 55240
diff changeset
   231
    "~~/src/HOL/Library/FuncSet"
eadea363deb6 Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents: 55240
diff changeset
   232
    "~~/src/HOL/Library/Multiset"
eadea363deb6 Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents: 55240
diff changeset
   233
    "~~/src/HOL/Algebra/Ring"
eadea363deb6 Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents: 55240
diff changeset
   234
    "~~/src/HOL/Algebra/FiniteProduct"
eadea363deb6 Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents: 55240
diff changeset
   235
  theories
eadea363deb6 Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents: 55240
diff changeset
   236
    Number_Theory
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   237
  document_files
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   238
    "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   239
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   240
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
   241
  description {*
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   242
    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
   243
    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
   244
  *}
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   245
  theories Hoare
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   246
  document_files "root.bib" "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   247
63888
5a9a1985e9fb sessions that are relevant for routine timing measurements;
wenzelm
parents: 63885
diff changeset
   248
session "HOL-Hoare_Parallel" (timing) 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
   249
  description {*
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   250
    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
   251
    (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
   252
  *}
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   253
  theories Hoare_Parallel
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   254
  document_files "root.bib" "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   255
65550
e957b1f00449 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65549
diff changeset
   256
session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Number_Theory" +
62354
fdd6989cc8a0 SML/NJ is no longer supported;
wenzelm
parents: 62286
diff changeset
   257
  options [document = false, browser_info = false]
65573
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   258
  sessions
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   259
    "HOL-Data_Structures"
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   260
    "HOL-ex"
51422
821a70e29e0b proper formatting, to facilitate line-based diff;
wenzelm
parents: 51421
diff changeset
   261
  theories
821a70e29e0b proper formatting, to facilitate line-based diff;
wenzelm
parents: 51421
diff changeset
   262
    Generate
821a70e29e0b proper formatting, to facilitate line-based diff;
wenzelm
parents: 51421
diff changeset
   263
    Generate_Binary_Nat
821a70e29e0b proper formatting, to facilitate line-based diff;
wenzelm
parents: 51421
diff changeset
   264
    Generate_Target_Nat
821a70e29e0b proper formatting, to facilitate line-based diff;
wenzelm
parents: 51421
diff changeset
   265
    Generate_Efficient_Datastructures
821a70e29e0b proper formatting, to facilitate line-based diff;
wenzelm
parents: 51421
diff changeset
   266
    Generate_Pretty_Char
64582
3d20ded18f14 unconditional Code_Test_PolyML and Code_Test_Scala: compiler is always present;
wenzelm
parents: 64569
diff changeset
   267
    Code_Test_PolyML
3d20ded18f14 unconditional Code_Test_PolyML and Code_Test_Scala: compiler is always present;
wenzelm
parents: 64569
diff changeset
   268
    Code_Test_Scala
62354
fdd6989cc8a0 SML/NJ is no longer supported;
wenzelm
parents: 62286
diff changeset
   269
  theories [condition = "ISABELLE_GHC"]
58039
469a375212c1 add testing framework for generated code
Andreas Lochbihler
parents: 58023
diff changeset
   270
    Code_Test_GHC
62354
fdd6989cc8a0 SML/NJ is no longer supported;
wenzelm
parents: 62286
diff changeset
   271
  theories [condition = "ISABELLE_MLTON"]
58039
469a375212c1 add testing framework for generated code
Andreas Lochbihler
parents: 58023
diff changeset
   272
    Code_Test_MLton
62354
fdd6989cc8a0 SML/NJ is no longer supported;
wenzelm
parents: 62286
diff changeset
   273
  theories [condition = "ISABELLE_OCAMLC"]
58039
469a375212c1 add testing framework for generated code
Andreas Lochbihler
parents: 58023
diff changeset
   274
    Code_Test_OCaml
62354
fdd6989cc8a0 SML/NJ is no longer supported;
wenzelm
parents: 62286
diff changeset
   275
  theories [condition = "ISABELLE_SMLNJ"]
58039
469a375212c1 add testing framework for generated code
Andreas Lochbihler
parents: 58023
diff changeset
   276
    Code_Test_SMLNJ
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   277
65573
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   278
session "HOL-Metis_Examples" (timing) in Metis_Examples = "HOL-Library" +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   279
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   280
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   281
    Author:     Jasmin Blanchette, TU Muenchen
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   282
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   283
    Testing Metis and Sledgehammer.
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   284
  *}
58423
e4d540c0dd57 clarified timeout for isatest;
wenzelm
parents: 58419
diff changeset
   285
  options [document = false]
65573
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   286
  sessions
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   287
    "HOL-Decision_Procs"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   288
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   289
    Abstraction
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   290
    Big_O
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   291
    Binary_Tree
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   292
    Clausification
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   293
    Message
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   294
    Proxies
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   295
    Tarski
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   296
    Trans_Closure
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   297
    Sets
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   298
65573
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   299
session "HOL-Nitpick_Examples" in Nitpick_Examples = "HOL-Library" +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   300
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   301
    Author:     Jasmin Blanchette, TU Muenchen
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   302
    Copyright   2009
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   303
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   304
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   305
  theories [quick_and_dirty] Nitpick_Examples
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   306
64389
6273d4c8325b added Nunchaku integration
blanchet
parents: 64379
diff changeset
   307
session "HOL-Nunchaku" in Nunchaku = HOL +
6273d4c8325b added Nunchaku integration
blanchet
parents: 64379
diff changeset
   308
  description {*
6273d4c8325b added Nunchaku integration
blanchet
parents: 64379
diff changeset
   309
    Author:     Jasmin Blanchette, Inria Nancy, LORIA, MPII
6273d4c8325b added Nunchaku integration
blanchet
parents: 64379
diff changeset
   310
    Copyright   2015, 2016
6273d4c8325b added Nunchaku integration
blanchet
parents: 64379
diff changeset
   311
6273d4c8325b added Nunchaku integration
blanchet
parents: 64379
diff changeset
   312
    Nunchaku: Yet another counterexample generator for Isabelle/HOL.
6273d4c8325b added Nunchaku integration
blanchet
parents: 64379
diff changeset
   313
  *}
6273d4c8325b added Nunchaku integration
blanchet
parents: 64379
diff changeset
   314
  options [document = false]
6273d4c8325b added Nunchaku integration
blanchet
parents: 64379
diff changeset
   315
  theories Nunchaku
6273d4c8325b added Nunchaku integration
blanchet
parents: 64379
diff changeset
   316
65550
e957b1f00449 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65549
diff changeset
   317
session "HOL-Algebra" (main timing) in Algebra = "HOL-Computational_Algebra" +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   318
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   319
    Author: Clemens Ballarin, started 24 September 1999
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   320
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   321
    The Isabelle Algebraic Library.
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   322
  *}
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   323
  theories [document = false]
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   324
    (* Preliminaries from set and number theory *)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   325
    "~~/src/HOL/Library/FuncSet"
65417
fc41a5650fb1 session containing computational algebra
haftmann
parents: 65416
diff changeset
   326
    "~~/src/HOL/Computational_Algebra/Primes"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   327
    "~~/src/HOL/Library/Permutation"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   328
  theories
65099
30d0b2f1df76 Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents: 65050
diff changeset
   329
    (* Orders and Lattices *)
30d0b2f1df76 Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents: 65050
diff changeset
   330
    Galois_Connection    (* Knaster-Tarski theorem and Galois connections *)
30d0b2f1df76 Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents: 65050
diff changeset
   331
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   332
    (* Groups *)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   333
    FiniteProduct        (* Product operator for commutative groups *)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   334
    Sylow                (* Sylow's theorem *)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   335
    Bij                  (* Automorphism Groups *)
65416
f707dbcf11e3 more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents: 65382
diff changeset
   336
    More_Group
f707dbcf11e3 more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents: 65382
diff changeset
   337
    More_Finite_Product
f707dbcf11e3 more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents: 65382
diff changeset
   338
    Multiplicative_Group
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   339
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   340
    (* Rings *)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   341
    Divisibility         (* Rings *)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   342
    IntRing              (* Ideals and residue classes *)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   343
    UnivPoly             (* Polynomials *)
65416
f707dbcf11e3 more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents: 65382
diff changeset
   344
    More_Ring
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   345
  document_files "root.bib" "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   346
65573
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   347
session "HOL-Auth" (timing) in Auth = "HOL-Library" +
51421
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   348
  description {*
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   349
    A new approach to verifying authentication protocols.
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   350
  *}
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   351
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   352
    Auth_Shared
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   353
    Auth_Public
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   354
    "Smartcard/Auth_Smartcard"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   355
    "Guard/Auth_Guard_Shared"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   356
    "Guard/Auth_Guard_Public"
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   357
  document_files "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   358
63888
5a9a1985e9fb sessions that are relevant for routine timing measurements;
wenzelm
parents: 63885
diff changeset
   359
session "HOL-UNITY" (timing) in UNITY = "HOL-Auth" +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   360
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   361
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   362
    Copyright   1998  University of Cambridge
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   363
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   364
    Verifying security protocols using Chandy and Misra's UNITY formalism.
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   365
  *}
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   366
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   367
    (*Basic meta-theory*)
65538
a39ef48fbee0 tuned imports;
wenzelm
parents: 65535
diff changeset
   368
    UNITY_Main
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   369
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   370
    (*Simple examples: no composition*)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   371
    "Simple/Deadlock"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   372
    "Simple/Common"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   373
    "Simple/Network"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   374
    "Simple/Token"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   375
    "Simple/Channel"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   376
    "Simple/Lift"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   377
    "Simple/Mutex"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   378
    "Simple/Reach"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   379
    "Simple/Reachability"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   380
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   381
    (*Verifying security protocols using UNITY*)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   382
    "Simple/NSP_Bad"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   383
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   384
    (*Example of composition*)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   385
    "Comp/Handshake"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   386
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   387
    (*Universal properties examples*)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   388
    "Comp/Counter"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   389
    "Comp/Counterc"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   390
    "Comp/Priority"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   391
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   392
    "Comp/TimerArray"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   393
    "Comp/Progress"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   394
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   395
    "Comp/Alloc"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   396
    "Comp/AllocImpl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   397
    "Comp/Client"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   398
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   399
    (*obsolete*)
65538
a39ef48fbee0 tuned imports;
wenzelm
parents: 65535
diff changeset
   400
    ELT
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   401
  document_files "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   402
65573
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   403
session "HOL-Unix" in Unix = "HOL-Library" +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   404
  options [print_mode = "no_brackets,no_type_brackets"]
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   405
  theories Unix
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   406
  document_files "root.bib" "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   407
65573
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   408
session "HOL-ZF" in ZF = "HOL-Library" +
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   409
  theories
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   410
    MainZF
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   411
    Games
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   412
  document_files "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   413
65550
e957b1f00449 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65549
diff changeset
   414
session "HOL-Imperative_HOL" in Imperative_HOL = "HOL-Library" +
59446
4427f04fca57 discontinued obsolete option "document_graph";
wenzelm
parents: 59190
diff changeset
   415
  options [print_mode = "iff,no_brackets"]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   416
  theories [document = false]
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   417
    "~~/src/HOL/Library/Countable"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   418
    "~~/src/HOL/Library/Monad_Syntax"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   419
    "~~/src/HOL/Library/LaTeXsugar"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   420
  theories Imperative_HOL_ex
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   421
  document_files "root.bib" "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   422
65550
e957b1f00449 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65549
diff changeset
   423
session "HOL-Decision_Procs" (timing) in Decision_Procs = "HOL-Algebra" +
51544
8c58fbbc1d5a tuned session specification;
wenzelm
parents: 51517
diff changeset
   424
  description {*
8c58fbbc1d5a tuned session specification;
wenzelm
parents: 51517
diff changeset
   425
    Various decision procedures, typically involving reflection.
8c58fbbc1d5a tuned session specification;
wenzelm
parents: 51517
diff changeset
   426
  *}
62354
fdd6989cc8a0 SML/NJ is no longer supported;
wenzelm
parents: 62286
diff changeset
   427
  options [document = false]
65543
8369b33fda0a clarified session imports;
wenzelm
parents: 65538
diff changeset
   428
  theories
8369b33fda0a clarified session imports;
wenzelm
parents: 65538
diff changeset
   429
    Decision_Procs
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   430
63000
d0dfdd413a7f remove "slow" session tags
Lars Hupel <lars.hupel@mytum.de>
parents: 62999
diff changeset
   431
session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
64597
1c252d8b6ca6 test parallel proof terms in this small session (somewhat slow for bigger applications);
wenzelm
parents: 64591
diff changeset
   432
  options [document = false]
65573
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   433
  sessions
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   434
    "HOL-Isar_Examples"
52424
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents: 52400
diff changeset
   435
  theories
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents: 52400
diff changeset
   436
    Hilbert_Classical
62363
7b5468422352 moved examples to avoid dependency on bulky HOL-Proofs session, e.g. relevant for "isabelle makedist";
wenzelm
parents: 62357
diff changeset
   437
    Proof_Terms
52424
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents: 52400
diff changeset
   438
    XML_Data
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   439
63888
5a9a1985e9fb sessions that are relevant for routine timing measurements;
wenzelm
parents: 63885
diff changeset
   440
session "HOL-Proofs-Extraction" (timing) in "Proofs/Extraction" = "HOL-Proofs" +
51421
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   441
  description {*
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   442
    Examples for program extraction in Higher-Order Logic.
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   443
  *}
62354
fdd6989cc8a0 SML/NJ is no longer supported;
wenzelm
parents: 62286
diff changeset
   444
  options [parallel_proofs = 0, quick_and_dirty = false]
65543
8369b33fda0a clarified session imports;
wenzelm
parents: 65538
diff changeset
   445
  sessions
8369b33fda0a clarified session imports;
wenzelm
parents: 65538
diff changeset
   446
    "HOL-Library"
8369b33fda0a clarified session imports;
wenzelm
parents: 65538
diff changeset
   447
    "HOL-Computational_Algebra"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   448
  theories [document = false]
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51115
diff changeset
   449
    "~~/src/HOL/Library/Code_Target_Numeral"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   450
    "~~/src/HOL/Library/Monad_Syntax"
65417
fc41a5650fb1 session containing computational algebra
haftmann
parents: 65416
diff changeset
   451
    "~~/src/HOL/Computational_Algebra/Primes"
66270
403d84138c5c State_Monad ~> Open_State_Syntax
Lars Hupel <lars.hupel@mytum.de>
parents: 66031
diff changeset
   452
    "~~/src/HOL/Library/Open_State_Syntax"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   453
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   454
    Greatest_Common_Divisor
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   455
    Warshall
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   456
    Higman_Extraction
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   457
    Pigeonhole
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   458
    Euclid
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   459
  document_files "root.bib" "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   460
63888
5a9a1985e9fb sessions that are relevant for routine timing measurements;
wenzelm
parents: 63885
diff changeset
   461
session "HOL-Proofs-Lambda" (timing) 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
   462
  description {*
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   463
    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
   464
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   465
    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
   466
    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
   467
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   468
    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
   469
    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
   470
  *}
62354
fdd6989cc8a0 SML/NJ is no longer supported;
wenzelm
parents: 62286
diff changeset
   471
  options [print_mode = "no_brackets",
62242
a4e6ea45f416 guard sessions that no longer work with SML/NJ -- memory problems;
wenzelm
parents: 62168
diff changeset
   472
    parallel_proofs = 0, quick_and_dirty = false]
65543
8369b33fda0a clarified session imports;
wenzelm
parents: 65538
diff changeset
   473
  sessions
8369b33fda0a clarified session imports;
wenzelm
parents: 65538
diff changeset
   474
    "HOL-Library"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   475
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   476
    Eta
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   477
    StrongNorm
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   478
    Standardization
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   479
    WeakNorm
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   480
  document_files "root.bib" "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   481
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   482
session "HOL-Prolog" in Prolog = HOL +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   483
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   484
    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
   485
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   486
    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
   487
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   488
    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
   489
    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
   490
    a little functional language and its type system.
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   491
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   492
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   493
  theories Test Type
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   494
65550
e957b1f00449 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65549
diff changeset
   495
session "HOL-MicroJava" (timing) in MicroJava = "HOL-Library" +
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   496
  description {*
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   497
    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
   498
    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
   499
    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
   500
  *}
65573
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   501
  sessions
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   502
    "HOL-Eisbach"
59446
4427f04fca57 discontinued obsolete option "document_graph";
wenzelm
parents: 59190
diff changeset
   503
  theories [document = false]
4427f04fca57 discontinued obsolete option "document_graph";
wenzelm
parents: 59190
diff changeset
   504
    "~~/src/HOL/Library/While_Combinator"
4427f04fca57 discontinued obsolete option "document_graph";
wenzelm
parents: 59190
diff changeset
   505
  theories
4427f04fca57 discontinued obsolete option "document_graph";
wenzelm
parents: 59190
diff changeset
   506
    MicroJava
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   507
  document_files
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   508
    "introduction.tex"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   509
    "root.bib"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   510
    "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   511
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   512
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
   513
  description {*
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   514
    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
   515
  *}
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   516
  theories Example
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   517
  document_files "root.bib" "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   518
65573
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   519
session "HOL-Bali" (timing) in Bali = "HOL-Library" +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   520
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   521
    AxExample
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   522
    AxSound
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   523
    AxCompl
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   524
    Trans
60751
83f04804696c reactivated dead code;
wenzelm
parents: 60603
diff changeset
   525
    TypeSafe
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   526
  document_files "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   527
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   528
session "HOL-IOA" in IOA = HOL +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   529
  description {*
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   530
    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
   531
    Copyright   1994--1996  TU Muenchen
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   532
55417
01fbfb60c33e adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents: 55370
diff changeset
   533
    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
   534
    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
   535
    proofs of two communication protocols which formerly have been here.
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   536
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   537
    @inproceedings{Nipkow-Slind-IOA,
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   538
    author={Tobias Nipkow and Konrad Slind},
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   539
    title={{I/O} Automata in {Isabelle/HOL}},
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   540
    booktitle={Proc.\ TYPES Workshop 1994},
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   541
    publisher=Springer,
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   542
    series=LNCS,
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   543
    note={To appear}}
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   544
    ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   545
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   546
    and
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   547
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   548
    @inproceedings{Mueller-Nipkow,
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   549
    author={Olaf M\"uller and Tobias Nipkow},
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   550
    title={Combining Model Checking and Deduction for {I/O}-Automata},
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   551
    booktitle={Proc.\ TACAS Workshop},
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   552
    organization={Aarhus University, BRICS report},
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   553
    year=1995}
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   554
    ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   555
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   556
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   557
  theories Solve
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   558
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   559
session "HOL-Lattice" in Lattice = HOL +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   560
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   561
    Author:     Markus Wenzel, TU Muenchen
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   562
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   563
    Basic theory of lattices and orders.
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   564
  *}
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   565
  theories CompleteLattice
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   566
  document_files "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   567
65678
aaba2e0c247c more timing;
wenzelm
parents: 65576
diff changeset
   568
session "HOL-ex" (timing) in ex = "HOL-Library" +
51421
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   569
  description {*
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   570
    Miscellaneous examples for Higher-Order Logic.
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   571
  *}
65548
b7caa2b8bdbf removed pointless document;
wenzelm
parents: 65544
diff changeset
   572
  options [document = false]
65543
8369b33fda0a clarified session imports;
wenzelm
parents: 65538
diff changeset
   573
  sessions
8369b33fda0a clarified session imports;
wenzelm
parents: 65538
diff changeset
   574
    "HOL-Number_Theory"
65548
b7caa2b8bdbf removed pointless document;
wenzelm
parents: 65544
diff changeset
   575
  theories
57507
a609065c9e15 revived unchecked theory (see cebaf814ca6e);
wenzelm
parents: 57434
diff changeset
   576
    Adhoc_Overloading_Examples
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   577
    Antiquote
65549
wenzelm
parents: 65548
diff changeset
   578
    Argo_Examples
wenzelm
parents: 65548
diff changeset
   579
    Arith_Examples
wenzelm
parents: 65548
diff changeset
   580
    Ballot
wenzelm
parents: 65548
diff changeset
   581
    BinEx
wenzelm
parents: 65548
diff changeset
   582
    Birthday_Paradox
wenzelm
parents: 65548
diff changeset
   583
    Bubblesort
wenzelm
parents: 65548
diff changeset
   584
    CTL
wenzelm
parents: 65548
diff changeset
   585
    Cartouche_Examples
65563
e83c9e94e891 actually use theory;
wenzelm
parents: 65562
diff changeset
   586
    Case_Product
65549
wenzelm
parents: 65548
diff changeset
   587
    Chinese
wenzelm
parents: 65548
diff changeset
   588
    Classical
wenzelm
parents: 65548
diff changeset
   589
    Code_Binary_Nat_examples
wenzelm
parents: 65548
diff changeset
   590
    Code_Timing
wenzelm
parents: 65548
diff changeset
   591
    Coercion_Examples
wenzelm
parents: 65548
diff changeset
   592
    Coherent
wenzelm
parents: 65548
diff changeset
   593
    Commands
wenzelm
parents: 65548
diff changeset
   594
    Computations
59190
3a594fd13ca4 3 old example lemmas by Amine listed in the top 100 theorems
kleing
parents: 59162
diff changeset
   595
    Cubic_Quartic
65549
wenzelm
parents: 65548
diff changeset
   596
    Dedekind_Real
wenzelm
parents: 65548
diff changeset
   597
    Erdoes_Szekeres
wenzelm
parents: 65548
diff changeset
   598
    Eval_Examples
wenzelm
parents: 65548
diff changeset
   599
    Executable_Relation
wenzelm
parents: 65548
diff changeset
   600
    Execute_Choice
wenzelm
parents: 65548
diff changeset
   601
    Functions
wenzelm
parents: 65548
diff changeset
   602
    Gauge_Integration
wenzelm
parents: 65548
diff changeset
   603
    Groebner_Examples
wenzelm
parents: 65548
diff changeset
   604
    Guess
wenzelm
parents: 65548
diff changeset
   605
    HarmonicSeries
wenzelm
parents: 65548
diff changeset
   606
    Hebrew
wenzelm
parents: 65548
diff changeset
   607
    Hex_Bin_Examples
wenzelm
parents: 65548
diff changeset
   608
    IArray_Examples
wenzelm
parents: 65548
diff changeset
   609
    Iff_Oracle
wenzelm
parents: 65548
diff changeset
   610
    Induction_Schema
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   611
    Intuitionistic
65549
wenzelm
parents: 65548
diff changeset
   612
    Lagrange
wenzelm
parents: 65548
diff changeset
   613
    List_to_Set_Comprehension_Examples
wenzelm
parents: 65548
diff changeset
   614
    LocaleTest2
wenzelm
parents: 65548
diff changeset
   615
    ML
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   616
    MergeSort
65549
wenzelm
parents: 65548
diff changeset
   617
    MonoidGroup
wenzelm
parents: 65548
diff changeset
   618
    Multiquote
wenzelm
parents: 65548
diff changeset
   619
    NatSum
wenzelm
parents: 65548
diff changeset
   620
    Normalization_by_Evaluation
wenzelm
parents: 65548
diff changeset
   621
    PER
wenzelm
parents: 65548
diff changeset
   622
    Parallel_Example
wenzelm
parents: 65548
diff changeset
   623
    Peano_Axioms
wenzelm
parents: 65548
diff changeset
   624
    Perm_Fragments
wenzelm
parents: 65548
diff changeset
   625
    PresburgerEx
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   626
    Primrec
65549
wenzelm
parents: 65548
diff changeset
   627
    Pythagoras
wenzelm
parents: 65548
diff changeset
   628
    Quicksort
wenzelm
parents: 65548
diff changeset
   629
    Records
wenzelm
parents: 65548
diff changeset
   630
    Reflection_Examples
wenzelm
parents: 65548
diff changeset
   631
    Refute_Examples
wenzelm
parents: 65548
diff changeset
   632
    Rewrite_Examples
wenzelm
parents: 65548
diff changeset
   633
    SAT_Examples
wenzelm
parents: 65548
diff changeset
   634
    SOS
wenzelm
parents: 65548
diff changeset
   635
    SOS_Cert
wenzelm
parents: 65548
diff changeset
   636
    Seq
wenzelm
parents: 65548
diff changeset
   637
    Serbian
wenzelm
parents: 65548
diff changeset
   638
    Set_Comprehension_Pointfree_Examples
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   639
    Set_Theory
65549
wenzelm
parents: 65548
diff changeset
   640
    Simproc_Tests
wenzelm
parents: 65548
diff changeset
   641
    Simps_Case_Conv_Examples
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   642
    Sqrt
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   643
    Sqrt_Script
65549
wenzelm
parents: 65548
diff changeset
   644
    Sudoku
wenzelm
parents: 65548
diff changeset
   645
    Sum_of_Powers
wenzelm
parents: 65548
diff changeset
   646
    Tarski
wenzelm
parents: 65548
diff changeset
   647
    Termination
wenzelm
parents: 65548
diff changeset
   648
    ThreeDivides
61368
33a62b54f381 add a file with examples of debugging transfer
kuncar
parents: 61232
diff changeset
   649
    Transfer_Debug
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   650
    Transfer_Ex
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   651
    Transfer_Int_Nat
56922
d411a81b8356 removed junk from library theory
haftmann
parents: 56818
diff changeset
   652
    Transitive_Closure_Table_Ex
65549
wenzelm
parents: 65548
diff changeset
   653
    Tree23
wenzelm
parents: 65548
diff changeset
   654
    Unification
wenzelm
parents: 65548
diff changeset
   655
    While_Combinator_Example
64015
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents: 63980
diff changeset
   656
    Word_Type
64978
5b9ba120d222 added veriT preprocessing proof reconstruction example
blanchet
parents: 64959
diff changeset
   657
    veriT_Preprocessing
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
   658
  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
   659
    Meson_Test
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   660
65550
e957b1f00449 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65549
diff changeset
   661
session "HOL-Isar_Examples" in Isar_Examples = "HOL-Computational_Algebra" +
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   662
  description {*
61935
6512e84cc9f5 clarified sessions;
wenzelm
parents: 61793
diff changeset
   663
    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
   664
  *}
61939
3c8c390a8f0a tuned document;
wenzelm
parents: 61938
diff changeset
   665
  options [quick_and_dirty]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   666
  theories [document = false]
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   667
    "~~/src/HOL/Library/Lattice_Syntax"
65417
fc41a5650fb1 session containing computational algebra
haftmann
parents: 65416
diff changeset
   668
    "../Computational_Algebra/Primes"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   669
  theories
61939
3c8c390a8f0a tuned document;
wenzelm
parents: 61938
diff changeset
   670
    Knaster_Tarski
3c8c390a8f0a tuned document;
wenzelm
parents: 61938
diff changeset
   671
    Peirce
3c8c390a8f0a tuned document;
wenzelm
parents: 61938
diff changeset
   672
    Drinker
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   673
    Cantor
61939
3c8c390a8f0a tuned document;
wenzelm
parents: 61938
diff changeset
   674
    Structured_Statements
3c8c390a8f0a tuned document;
wenzelm
parents: 61938
diff changeset
   675
    Basic_Logic
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   676
    Expr_Compiler
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   677
    Fibonacci
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   678
    Group
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   679
    Group_Context
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   680
    Group_Notepad
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   681
    Hoare_Ex
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   682
    Mutilated_Checkerboard
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   683
    Puzzle
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   684
    Summation
61935
6512e84cc9f5 clarified sessions;
wenzelm
parents: 61793
diff changeset
   685
    First_Order_Logic
6512e84cc9f5 clarified sessions;
wenzelm
parents: 61793
diff changeset
   686
    Higher_Order_Logic
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   687
  document_files
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   688
    "root.bib"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   689
    "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   690
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents: 60008
diff changeset
   691
session "HOL-Eisbach" in Eisbach = HOL +
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents: 60008
diff changeset
   692
  description {*
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents: 60008
diff changeset
   693
    The Eisbach proof method language and "match" method.
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents: 60008
diff changeset
   694
  *}
66444
6d2d993fa76e clarified imports;
wenzelm
parents: 66443
diff changeset
   695
  sessions
6d2d993fa76e clarified imports;
wenzelm
parents: 66443
diff changeset
   696
    FOL
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents: 60008
diff changeset
   697
  theories
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents: 60008
diff changeset
   698
    Eisbach
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents: 60008
diff changeset
   699
    Tests
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents: 60008
diff changeset
   700
    Examples
62168
e97452d79102 Eisbach works for other object-logics, e.g. Eisbach_FOL.thy;
wenzelm
parents: 62155
diff changeset
   701
    Examples_FOL
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents: 60008
diff changeset
   702
65550
e957b1f00449 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65549
diff changeset
   703
session "HOL-SET_Protocol" (timing) in SET_Protocol = "HOL-Library" +
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   704
  description {*
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   705
    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
   706
  *}
65543
8369b33fda0a clarified session imports;
wenzelm
parents: 65538
diff changeset
   707
  theories [document = false]
8369b33fda0a clarified session imports;
wenzelm
parents: 65538
diff changeset
   708
    "~~/src/HOL/Library/Nat_Bijection"
8369b33fda0a clarified session imports;
wenzelm
parents: 65538
diff changeset
   709
  theories
8369b33fda0a clarified session imports;
wenzelm
parents: 65538
diff changeset
   710
    SET_Protocol
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   711
  document_files "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   712
65569
3cb6f3281ef1 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65563
diff changeset
   713
session "HOL-Matrix_LP" in Matrix_LP = "HOL-Library" +
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   714
  description {*
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   715
    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
   716
  *}
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   717
  theories Cplex
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   718
  document_files "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   719
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   720
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
   721
  description {*
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   722
    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
   723
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   724
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   725
  theories TLA
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   726
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   727
session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" +
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   728
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   729
  theories Inc
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   730
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   731
session "HOL-TLA-Buffer" in "TLA/Buffer" = "HOL-TLA" +
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   732
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   733
  theories DBuffer
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   734
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   735
session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" +
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   736
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   737
  theories MemoryImplementation
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   738
65573
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   739
session "HOL-TPTP" in TPTP = "HOL-Library" +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   740
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   741
    Author:     Jasmin Blanchette, TU Muenchen
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   742
    Author:     Nik Sultana, University of Cambridge
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   743
    Copyright   2011
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   744
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   745
    TPTP-related extensions.
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   746
  *}
62354
fdd6989cc8a0 SML/NJ is no longer supported;
wenzelm
parents: 62286
diff changeset
   747
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   748
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   749
    ATP_Theory_Export
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   750
    MaSh_Eval
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   751
    TPTP_Interpret
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   752
    THF_Arith
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents: 55450
diff changeset
   753
    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
   754
  theories
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   755
    ATP_Problem_Import
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   756
65382
de848ac5e0d7 more main sessions and global theories;
wenzelm
parents: 65381
diff changeset
   757
session "HOL-Probability" (main timing) in "Probability" = "HOL-Analysis" +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   758
  theories [document = false]
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   759
    "~~/src/HOL/Library/Countable"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   760
    "~~/src/HOL/Library/Permutation"
56994
8d5e5ec1cac3 fixed document generation for HOL-Probability
hoelzl
parents: 56940
diff changeset
   761
    "~~/src/HOL/Library/Order_Continuity"
8d5e5ec1cac3 fixed document generation for HOL-Probability
hoelzl
parents: 56940
diff changeset
   762
    "~~/src/HOL/Library/Diagonal_Subsequence"
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents: 63829
diff changeset
   763
    "~~/src/HOL/Library/Finite_Map"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   764
  theories
65382
de848ac5e0d7 more main sessions and global theories;
wenzelm
parents: 65381
diff changeset
   765
    Probability (global)
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   766
  document_files "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   767
63888
5a9a1985e9fb sessions that are relevant for routine timing measurements;
wenzelm
parents: 63885
diff changeset
   768
session "HOL-Probability-ex" (timing) in "Probability/ex" = "HOL-Probability" +
61946
844881193616 put example into separate session, to restrict precious session image to library theories
haftmann
parents: 61939
diff changeset
   769
  theories
65538
a39ef48fbee0 tuned imports;
wenzelm
parents: 65535
diff changeset
   770
    Dining_Cryptographers
a39ef48fbee0 tuned imports;
wenzelm
parents: 65535
diff changeset
   771
    Koepf_Duermuth_Countermeasure
a39ef48fbee0 tuned imports;
wenzelm
parents: 65535
diff changeset
   772
    Measure_Not_CCC
61946
844881193616 put example into separate session, to restrict precious session image to library theories
haftmann
parents: 61939
diff changeset
   773
59898
81c70bdbd908 clarified "main" group, e.g. relevant for Isabelle/jEdit menu;
wenzelm
parents: 59810
diff changeset
   774
session "HOL-Nominal" in Nominal = HOL +
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   775
  options [document = false]
65573
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   776
  sessions
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   777
    "HOL-Library"
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   778
  theories
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   779
    Nominal
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   780
63888
5a9a1985e9fb sessions that are relevant for routine timing measurements;
wenzelm
parents: 63885
diff changeset
   781
session "HOL-Nominal-Examples" (timing) in "Nominal/Examples" = "HOL-Nominal" +
62354
fdd6989cc8a0 SML/NJ is no longer supported;
wenzelm
parents: 62286
diff changeset
   782
  options [document = false]
58329
a31404ec7414 run larger nominal examples only 'ISABELLE_FULL_TEST'
blanchet
parents: 58313
diff changeset
   783
  theories
59162
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   784
    Class3
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   785
    CK_Machine
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   786
    Compile
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   787
    Contexts
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   788
    Crary
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   789
    CR_Takahashi
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   790
    CR
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   791
    Fsub
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   792
    Height
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   793
    Lambda_mu
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   794
    Lam_Funs
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   795
    LocalWeakening
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   796
    Pattern
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   797
    SN
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   798
    SOS
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   799
    Standardization
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   800
    Support
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   801
    Type_Preservation
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   802
    Weakening
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   803
    W
58329
a31404ec7414 run larger nominal examples only 'ISABELLE_FULL_TEST'
blanchet
parents: 58313
diff changeset
   804
  theories [quick_and_dirty]
a31404ec7414 run larger nominal examples only 'ISABELLE_FULL_TEST'
blanchet
parents: 58313
diff changeset
   805
    VC_Condition
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   806
65573
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   807
session "HOL-Cardinals" (timing) in Cardinals = "HOL-Library" +
51421
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   808
  description {*
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   809
    Ordinals and Cardinals, Full Theories.
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   810
  *}
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
   811
  options [document = false]
59747
7325ffa35038 bounded powerset
traytel
parents: 59743
diff changeset
   812
  theories
7325ffa35038 bounded powerset
traytel
parents: 59743
diff changeset
   813
    Cardinals
7325ffa35038 bounded powerset
traytel
parents: 59743
diff changeset
   814
    Bounded_Set
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   815
  document_files
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   816
    "intro.tex"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   817
    "root.tex"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   818
    "root.bib"
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents: 48932
diff changeset
   819
65574
10f4a17e5928 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65573
diff changeset
   820
session "HOL-Datatype_Examples" (timing) in Datatype_Examples = "HOL-Library" +
51421
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   821
  description {*
62286
705d4c4003ea clarified ISABELLE_FULL_TEST vs. benchmarks: src/Benchmarks is not in ROOTS and thus not covered by "isabelle build -a" by default;
wenzelm
parents: 62285
diff changeset
   822
    (Co)datatype Examples.
51421
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   823
  *}
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
   824
  options [document = false]
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents: 48932
diff changeset
   825
  theories
56454
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents: 56215
diff changeset
   826
    Compat
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents: 48932
diff changeset
   827
    Lambda_Term
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents: 48932
diff changeset
   828
    Process
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents: 48932
diff changeset
   829
    TreeFsetI
49872
c6a686c9be2a update ROOT with teh directory change in BNF
popescua
parents: 49693
diff changeset
   830
    "Derivation_Trees/Gram_Lang"
65574
10f4a17e5928 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65573
diff changeset
   831
    "Derivation_Trees/Parallel_Composition"
50517
8f6c11103820 renamed theory
traytel
parents: 50480
diff changeset
   832
    Koenig
60921
487050067be9 actually process lift_bnf regression suite
traytel
parents: 60809
diff changeset
   833
    Lift_BNF
61745
e23e0ff98657 Ported old example to use (co)datatypes
traytel
parents: 61670
diff changeset
   834
    Milner_Tofte
54961
e60428f432bc new codatatype example: stream processors
traytel
parents: 54481
diff changeset
   835
    Stream_Processor
53122
bc87b7af4767 renamed theory files to be closer to (new) command names
blanchet
parents: 52726
diff changeset
   836
    Misc_Codatatype
bc87b7af4767 renamed theory files to be closer to (new) command names
blanchet
parents: 52726
diff changeset
   837
    Misc_Datatype
54193
bc07627c5dcd added 'primcorec' examples
blanchet
parents: 53935
diff changeset
   838
    Misc_Primcorec
53306
45f13517693a added example
blanchet
parents: 53164
diff changeset
   839
    Misc_Primrec
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents: 48932
diff changeset
   840
65573
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   841
session "HOL-Corec_Examples" (timing) in Corec_Examples = "HOL-Library" +
62694
f50d7efc8fe3 added two 'corec' examples
blanchet
parents: 62479
diff changeset
   842
  description {*
f50d7efc8fe3 added two 'corec' examples
blanchet
parents: 62479
diff changeset
   843
    Corecursion Examples.
f50d7efc8fe3 added two 'corec' examples
blanchet
parents: 62479
diff changeset
   844
  *}
f50d7efc8fe3 added two 'corec' examples
blanchet
parents: 62479
diff changeset
   845
  options [document = false]
f50d7efc8fe3 added two 'corec' examples
blanchet
parents: 62479
diff changeset
   846
  theories
f50d7efc8fe3 added two 'corec' examples
blanchet
parents: 62479
diff changeset
   847
    LFilter
62734
38fefd98c929 another 'corec' example
blanchet
parents: 62725
diff changeset
   848
    Paper_Examples
62694
f50d7efc8fe3 added two 'corec' examples
blanchet
parents: 62479
diff changeset
   849
    Stream_Processor
62696
7325d8573fb8 added 'corec' examples and tests
blanchet
parents: 62694
diff changeset
   850
    "Tests/Simple_Nesting"
64379
71f42dcaa1df additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents: 64323
diff changeset
   851
    "Tests/Iterate_GPV"
62696
7325d8573fb8 added 'corec' examples and tests
blanchet
parents: 62694
diff changeset
   852
  theories [quick_and_dirty]
7325d8573fb8 added 'corec' examples and tests
blanchet
parents: 62694
diff changeset
   853
    "Tests/GPV_Bare_Bones"
7325d8573fb8 added 'corec' examples and tests
blanchet
parents: 62694
diff changeset
   854
    "Tests/Merge_D"
7325d8573fb8 added 'corec' examples and tests
blanchet
parents: 62694
diff changeset
   855
    "Tests/Merge_Poly"
7325d8573fb8 added 'corec' examples and tests
blanchet
parents: 62694
diff changeset
   856
    "Tests/Misc_Mono"
7325d8573fb8 added 'corec' examples and tests
blanchet
parents: 62694
diff changeset
   857
    "Tests/Misc_Poly"
7325d8573fb8 added 'corec' examples and tests
blanchet
parents: 62694
diff changeset
   858
    "Tests/Small_Concrete"
62725
5ab1746186c7 new 'corec' example
blanchet
parents: 62706
diff changeset
   859
    "Tests/Stream_Friends"
62696
7325d8573fb8 added 'corec' examples and tests
blanchet
parents: 62694
diff changeset
   860
    "Tests/TLList_Friends"
63190
3e79279c10ca added test
blanchet
parents: 63165
diff changeset
   861
    "Tests/Type_Class"
62694
f50d7efc8fe3 added two 'corec' examples
blanchet
parents: 62479
diff changeset
   862
63888
5a9a1985e9fb sessions that are relevant for routine timing measurements;
wenzelm
parents: 63885
diff changeset
   863
session "HOL-Word" (main timing) in Word = HOL +
65573
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   864
  sessions
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   865
    "HOL-Library"
65382
de848ac5e0d7 more main sessions and global theories;
wenzelm
parents: 65381
diff changeset
   866
  theories
65462
db1827610513 less global theories -- conflict with AFP entries;
wenzelm
parents: 65456
diff changeset
   867
    Word
66445
407de0768126 more complete session (amending e77ea0ea7f2c);
wenzelm
parents: 66444
diff changeset
   868
    WordBitwise
66443
657c517c7dc6 more complete session (amending 783861a66a60);
wenzelm
parents: 66434
diff changeset
   869
    Bit_Comparison
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   870
  document_files "root.bib" "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   871
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   872
session "HOL-Word-Examples" in "Word/Examples" = "HOL-Word" +
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   873
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   874
  theories WordExamples
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   875
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   876
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
   877
  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
   878
    StateSpaceEx
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   879
  document_files "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   880
65550
e957b1f00449 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65549
diff changeset
   881
session "HOL-Nonstandard_Analysis" (timing) in Nonstandard_Analysis = "HOL-Computational_Algebra" +
51421
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   882
  description {*
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   883
    Nonstandard analysis.
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   884
  *}
62479
716336f19aa9 clarified session;
wenzelm
parents: 62380
diff changeset
   885
  theories
716336f19aa9 clarified session;
wenzelm
parents: 62380
diff changeset
   886
    Nonstandard_Analysis
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   887
  document_files "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   888
63888
5a9a1985e9fb sessions that are relevant for routine timing measurements;
wenzelm
parents: 63885
diff changeset
   889
session "HOL-Nonstandard_Analysis-Examples" (timing) in "Nonstandard_Analysis/Examples" = "HOL-Nonstandard_Analysis" +
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   890
  options [document = false]
65543
8369b33fda0a clarified session imports;
wenzelm
parents: 65538
diff changeset
   891
  theories
8369b33fda0a clarified session imports;
wenzelm
parents: 65538
diff changeset
   892
    NSPrimes
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   893
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   894
session "HOL-Mirabelle" in Mirabelle = HOL +
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   895
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   896
  theories Mirabelle_Test
48589
fb446a780d50 separate session HOL-Mirabelle-ex -- cannot run isolated shell scripts within build tool;
wenzelm
parents: 48588
diff changeset
   897
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   898
session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
62354
fdd6989cc8a0 SML/NJ is no longer supported;
wenzelm
parents: 62286
diff changeset
   899
  options [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
   900
  theories Ex
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   901
63888
5a9a1985e9fb sessions that are relevant for routine timing measurements;
wenzelm
parents: 63885
diff changeset
   902
session "HOL-Word-SMT_Examples" (timing) in SMT_Examples = "HOL-Word" +
62354
fdd6989cc8a0 SML/NJ is no longer supported;
wenzelm
parents: 62286
diff changeset
   903
  options [document = false, quick_and_dirty]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   904
  theories
52722
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents: 52499
diff changeset
   905
    Boogie
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   906
    SMT_Examples
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   907
    SMT_Word_Examples
50666
6f48853f08d5 actually run Z3 for "SMT_Tests" when "ISABELLE_FULL_TEST" is enabled
blanchet
parents: 50665
diff changeset
   908
    SMT_Tests
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   909
  files
58367
8af1e68d7e1a renamed SMT certificate files, following 'SMT2' -> 'SMT' renaming
blanchet
parents: 58351
diff changeset
   910
    "Boogie_Dijkstra.certs"
8af1e68d7e1a renamed SMT certificate files, following 'SMT2' -> 'SMT' renaming
blanchet
parents: 58351
diff changeset
   911
    "Boogie_Max.certs"
8af1e68d7e1a renamed SMT certificate files, following 'SMT2' -> 'SMT' renaming
blanchet
parents: 58351
diff changeset
   912
    "SMT_Examples.certs"
8af1e68d7e1a renamed SMT certificate files, following 'SMT2' -> 'SMT' renaming
blanchet
parents: 58351
diff changeset
   913
    "SMT_Word_Examples.certs"
8af1e68d7e1a renamed SMT certificate files, following 'SMT2' -> 'SMT' renaming
blanchet
parents: 58351
diff changeset
   914
    "VCC_Max.certs"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   915
50844
b95ff3744815 populate "main" session group, e.g. relevant for Isabelle/jEdit logic selection;
wenzelm
parents: 50833
diff changeset
   916
session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" +
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   917
  options [document = false]
65382
de848ac5e0d7 more main sessions and global theories;
wenzelm
parents: 65381
diff changeset
   918
  theories
de848ac5e0d7 more main sessions and global theories;
wenzelm
parents: 65381
diff changeset
   919
    SPARK (global)
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   920
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   921
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
   922
  options [document = false, spark_prv = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   923
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   924
    "Gcd/Greatest_Common_Divisor"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   925
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   926
    "Liseq/Longest_Increasing_Subsequence"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   927
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   928
    "RIPEMD-160/F"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   929
    "RIPEMD-160/Hash"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   930
    "RIPEMD-160/K_L"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   931
    "RIPEMD-160/K_R"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   932
    "RIPEMD-160/R_L"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   933
    "RIPEMD-160/Round"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   934
    "RIPEMD-160/R_R"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   935
    "RIPEMD-160/S_L"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   936
    "RIPEMD-160/S_R"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   937
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   938
    "Sqrt/Sqrt"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   939
  files
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   940
    "Gcd/greatest_common_divisor/g_c_d.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   941
    "Gcd/greatest_common_divisor/g_c_d.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   942
    "Gcd/greatest_common_divisor/g_c_d.siv"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   943
    "Liseq/liseq/liseq_length.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   944
    "Liseq/liseq/liseq_length.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   945
    "Liseq/liseq/liseq_length.siv"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   946
    "RIPEMD-160/rmd/f.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   947
    "RIPEMD-160/rmd/f.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   948
    "RIPEMD-160/rmd/f.siv"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   949
    "RIPEMD-160/rmd/hash.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   950
    "RIPEMD-160/rmd/hash.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   951
    "RIPEMD-160/rmd/hash.siv"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   952
    "RIPEMD-160/rmd/k_l.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   953
    "RIPEMD-160/rmd/k_l.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   954
    "RIPEMD-160/rmd/k_l.siv"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   955
    "RIPEMD-160/rmd/k_r.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   956
    "RIPEMD-160/rmd/k_r.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   957
    "RIPEMD-160/rmd/k_r.siv"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   958
    "RIPEMD-160/rmd/r_l.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   959
    "RIPEMD-160/rmd/r_l.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   960
    "RIPEMD-160/rmd/r_l.siv"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   961
    "RIPEMD-160/rmd/round.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   962
    "RIPEMD-160/rmd/round.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   963
    "RIPEMD-160/rmd/round.siv"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   964
    "RIPEMD-160/rmd/r_r.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   965
    "RIPEMD-160/rmd/r_r.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   966
    "RIPEMD-160/rmd/r_r.siv"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   967
    "RIPEMD-160/rmd/s_l.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   968
    "RIPEMD-160/rmd/s_l.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   969
    "RIPEMD-160/rmd/s_l.siv"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   970
    "RIPEMD-160/rmd/s_r.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   971
    "RIPEMD-160/rmd/s_r.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   972
    "RIPEMD-160/rmd/s_r.siv"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   973
65576
8376f83f9094 recovered document from 0f3fdf689bf9;
wenzelm
parents: 65574
diff changeset
   974
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
   975
  options [show_question_marks = false, spark_prv = false]
66031
94cfcae2b228 clarified imports;
wenzelm
parents: 66015
diff changeset
   976
  sessions
94cfcae2b228 clarified imports;
wenzelm
parents: 66015
diff changeset
   977
    "HOL-SPARK-Examples"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   978
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   979
    Example_Verification
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   980
    VC_Principles
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   981
    Reference
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   982
    Complex_Types
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   983
  files
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   984
    "complex_types_app/initialize.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   985
    "complex_types_app/initialize.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   986
    "complex_types_app/initialize.siv"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   987
    "loop_invariant/proc1.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   988
    "loop_invariant/proc1.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   989
    "loop_invariant/proc1.siv"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   990
    "loop_invariant/proc2.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   991
    "loop_invariant/proc2.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   992
    "loop_invariant/proc2.siv"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   993
    "simple_greatest_common_divisor/g_c_d.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   994
    "simple_greatest_common_divisor/g_c_d.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   995
    "simple_greatest_common_divisor/g_c_d.siv"
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   996
  document_files
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   997
    "complex_types.ads"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   998
    "complex_types_app.adb"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   999
    "complex_types_app.ads"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
  1000
    "Gcd.adb"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
  1001
    "Gcd.ads"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
  1002
    "intro.tex"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
  1003
    "loop_invariant.adb"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
  1004
    "loop_invariant.ads"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
  1005
    "root.bib"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
  1006
    "root.tex"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
  1007
    "Simple_Gcd.adb"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
  1008
    "Simple_Gcd.ads"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1009
65573
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
  1010
session "HOL-Mutabelle" in Mutabelle = "HOL-Library" +
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
  1011
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1012
  theories MutabelleExtra
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1013
65569
3cb6f3281ef1 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65563
diff changeset
  1014
session "HOL-Quickcheck_Examples" (timing) in Quickcheck_Examples = "HOL-Library" +
50179
978200ae8473 timeout in proper place (HOL-Quickcheck_Examples approx. 1min, HOL-Quickcheck_Benchmark approx. 1h);
wenzelm
parents: 50161
diff changeset
  1015
  options [document = false]
48588
23456b2a769d added Quickcheck_Benchmark (cf. 1959baa22632);
wenzelm
parents: 48512
diff changeset
  1016
  theories
48690
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
  1017
    Quickcheck_Examples
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
  1018
    Quickcheck_Lattice_Examples
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
  1019
    Completeness
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
  1020
    Quickcheck_Interfaces
63731
9f906a2eb0e7 added theory to provide workaround to support nested datatypes in quickcheck (until quickcheck is generalized to support it with new datatypes)
blanchet
parents: 63643
diff changeset
  1021
    Quickcheck_Nesting_Example
57584
155b7e3b729e proper condition wrt. ISABELLE_GHC (cf. 8840fa17e17c);
wenzelm
parents: 57544
diff changeset
  1022
  theories [condition = ISABELLE_GHC]
57544
8840fa17e17c reactivate session Quickcheck_Examples
Andreas Lochbihler
parents: 57543
diff changeset
  1023
    Hotel_Example
48598
7f4561d43d39 updated ROOT according to 3defa60a7ae3;
wenzelm
parents: 48589
diff changeset
  1024
    Quickcheck_Narrowing_Examples
48588
23456b2a769d added Quickcheck_Benchmark (cf. 1959baa22632);
wenzelm
parents: 48512
diff changeset
  1025
65569
3cb6f3281ef1 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65563
diff changeset
  1026
session "HOL-Quotient_Examples" (timing) in Quotient_Examples = "HOL-Algebra" +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1027
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1028
    Author:     Cezary Kaliszyk and Christian Urban
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1029
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
  1030
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1031
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1032
    DList
63920
003622e08379 resolve the name clash of HOL/Library/FSet and HOL/Quotient_Examples/FSet
kuncar
parents: 63888
diff changeset
  1033
    Quotient_FSet
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1034
    Quotient_Int
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1035
    Quotient_Message
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1036
    Lift_FSet
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1037
    Lift_Set
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1038
    Lift_Fun
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1039
    Quotient_Rat
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1040
    Lift_DList
53682
1b55aeda0e46 include Int_Pow into Quotient_Examples; add end of the theory
kuncar
parents: 53430
diff changeset
  1041
    Int_Pow
60237
d47387d4a3c6 add testing file for code_dt extension of lifting
kuncar
parents: 60119
diff changeset
  1042
    Lifting_Code_Dt_Test
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1043
65569
3cb6f3281ef1 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65563
diff changeset
  1044
session "HOL-Predicate_Compile_Examples" (timing) in Predicate_Compile_Examples = "HOL-Library" +
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
  1045
  options [document = false]
62354
fdd6989cc8a0 SML/NJ is no longer supported;
wenzelm
parents: 62286
diff changeset
  1046
  theories
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1047
    Examples
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1048
    Predicate_Compile_Tests
61140
78ece168f5b5 reactivate examples with predicate compiler and quickcheck
Andreas Lochbihler
parents: 60921
diff changeset
  1049
    Predicate_Compile_Quickcheck_Examples
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1050
    Specialisation_Examples
48690
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
  1051
    IMP_1
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
  1052
    IMP_2
55450
9eddc17749f7 reactivate some examples that still appear to work;
wenzelm
parents: 55447
diff changeset
  1053
    (* FIXME since 21-Jul-2011
61140
78ece168f5b5 reactivate examples with predicate compiler and quickcheck
Andreas Lochbihler
parents: 60921
diff changeset
  1054
    Hotel_Example_Small_Generator *)
48690
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
  1055
    IMP_3
61140
78ece168f5b5 reactivate examples with predicate compiler and quickcheck
Andreas Lochbihler
parents: 60921
diff changeset
  1056
    IMP_4
62242
a4e6ea45f416 guard sessions that no longer work with SML/NJ -- memory problems;
wenzelm
parents: 62168
diff changeset
  1057
  theories [condition = ISABELLE_SWIPL]
48690
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
  1058
    Code_Prolog_Examples
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
  1059
    Context_Free_Grammar_Example
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
  1060
    Hotel_Example_Prolog
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
  1061
    Lambda_Example
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
  1062
    List_Examples
62242
a4e6ea45f416 guard sessions that no longer work with SML/NJ -- memory problems;
wenzelm
parents: 62168
diff changeset
  1063
  theories [condition = ISABELLE_SWIPL, quick_and_dirty]
48690
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
  1064
    Reg_Exp_Example
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1065
64551
79e9587dbcca proper session HOL-Types_To_Sets;
wenzelm
parents: 64431
diff changeset
  1066
session "HOL-Types_To_Sets" in Types_To_Sets = HOL +
79e9587dbcca proper session HOL-Types_To_Sets;
wenzelm
parents: 64431
diff changeset
  1067
  description {*
79e9587dbcca proper session HOL-Types_To_Sets;
wenzelm
parents: 64431
diff changeset
  1068
    Experimental extension of Higher-Order Logic to allow translation of types to sets.
79e9587dbcca proper session HOL-Types_To_Sets;
wenzelm
parents: 64431
diff changeset
  1069
  *}
79e9587dbcca proper session HOL-Types_To_Sets;
wenzelm
parents: 64431
diff changeset
  1070
  options [document = false]
79e9587dbcca proper session HOL-Types_To_Sets;
wenzelm
parents: 64431
diff changeset
  1071
  theories
79e9587dbcca proper session HOL-Types_To_Sets;
wenzelm
parents: 64431
diff changeset
  1072
    Types_To_Sets
79e9587dbcca proper session HOL-Types_To_Sets;
wenzelm
parents: 64431
diff changeset
  1073
    "Examples/Prerequisites"
79e9587dbcca proper session HOL-Types_To_Sets;
wenzelm
parents: 64431
diff changeset
  1074
    "Examples/Finite"
79e9587dbcca proper session HOL-Types_To_Sets;
wenzelm
parents: 64431
diff changeset
  1075
    "Examples/T2_Spaces"
79e9587dbcca proper session HOL-Types_To_Sets;
wenzelm
parents: 64431
diff changeset
  1076
63888
5a9a1985e9fb sessions that are relevant for routine timing measurements;
wenzelm
parents: 63885
diff changeset
  1077
session HOLCF (main timing) in HOLCF = HOL +
48338
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
  1078
  description {*
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
  1079
    Author:     Franz Regensburger
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
  1080
    Author:     Brian Huffman
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
  1081
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
  1082
    HOLCF -- a semantic extension of HOL by the LCF logic.
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
  1083
  *}
65543
8369b33fda0a clarified session imports;
wenzelm
parents: 65538
diff changeset
  1084
  sessions
8369b33fda0a clarified session imports;
wenzelm
parents: 65538
diff changeset
  1085
    "HOL-Library"
48470
7483aa690b4f clarified "document" again, eliminated redundant "no_document";
wenzelm
parents: 48458
diff changeset
  1086
  theories [document = false]
48338
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
  1087
    "~~/src/HOL/Library/Nat_Bijection"
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
  1088
    "~~/src/HOL/Library/Countable"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1089
  theories
65382
de848ac5e0d7 more main sessions and global theories;
wenzelm
parents: 65381
diff changeset
  1090
    HOLCF (global)
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
  1091
  document_files "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1092
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
  1093
session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1094
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1095
    Domain_ex
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1096
    Fixrec_ex
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1097
    New_Domain
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
  1098
  document_files "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1099
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
  1100
session "HOLCF-Library" in "HOLCF/Library" = HOLCF +
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
  1101
  options [document = false]
65570
660df4a6dc59 actually use theory;
wenzelm
parents: 65569
diff changeset
  1102
  theories
660df4a6dc59 actually use theory;
wenzelm
parents: 65569
diff changeset
  1103
    HOLCF_Library
660df4a6dc59 actually use theory;
wenzelm
parents: 65569
diff changeset
  1104
    HOL_Cpo
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1105
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
  1106
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
  1107
  description {*
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1108
    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
  1109
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1110
    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
  1111
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
  1112
  options [document = false]
65573
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
  1113
  sessions
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
  1114
    "HOL-IMP"
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
  1115
  theories
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
  1116
    HoareEx
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
  1117
  document_files "root.tex"
48338
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
  1118
65573
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
  1119
session "HOLCF-ex" in "HOLCF/ex" = "HOLCF-Library" +
51421
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
  1120
  description {*
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
  1121
    Miscellaneous examples for HOLCF.
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
  1122
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
  1123
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1124
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1125
    Dnat
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1126
    Dagstuhl
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1127
    Focus_ex
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1128
    Fix2
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1129
    Hoare
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1130
    Concurrency_Monad
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1131
    Loop
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1132
    Powerdomain_ex
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1133
    Domain_Proofs
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1134
    Letrec
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1135
    Pattern_Match
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1136
65573
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
  1137
session "HOLCF-FOCUS" in "HOLCF/FOCUS" = "HOLCF-Library" +
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1138
  description {*
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1139
    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
  1140
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1141
    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
  1142
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1143
    "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
  1144
    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
  1145
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1146
    "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
  1147
    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
  1148
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1149
    "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
  1150
    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
  1151
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
  1152
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1153
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1154
    Fstreams
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1155
    FOCUS
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1156
    Buffer_adm
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1157
63888
5a9a1985e9fb sessions that are relevant for routine timing measurements;
wenzelm
parents: 63885
diff changeset
  1158
session IOA (timing) in "HOLCF/IOA" = HOLCF +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1159
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1160
    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
  1161
    Copyright   1997 TU München
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1162
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1163
    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
  1164
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1165
    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
  1166
    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
  1167
    finite and infinite sequences.
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1168
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
  1169
  options [document = false]
65538
a39ef48fbee0 tuned imports;
wenzelm
parents: 65535
diff changeset
  1170
  theories Abstraction
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1171
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
  1172
session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1173
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1174
    Author:     Olaf Mueller
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1175
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1176
    The Alternating Bit Protocol performed in I/O-Automata.
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1177
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
  1178
  options [document = false]
59503
9937bc07202b check unused theory;
wenzelm
parents: 59446
diff changeset
  1179
  theories
9937bc07202b check unused theory;
wenzelm
parents: 59446
diff changeset
  1180
    Correctness
9937bc07202b check unused theory;
wenzelm
parents: 59446
diff changeset
  1181
    Spec
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1182
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
  1183
session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1184
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1185
    Author:     Tobias Nipkow & Konrad Slind
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1186
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1187
    A network transmission protocol, performed in the
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1188
    I/O automata formalization by Olaf Mueller.
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1189
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
  1190
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1191
  theories Correctness
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1192
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
  1193
session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1194
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1195
    Author:     Olaf Mueller
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1196
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1197
    Memory storage case study.
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1198
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
  1199
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1200
  theories Correctness
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1201
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
  1202
session "IOA-ex" in "HOLCF/IOA/ex" = IOA +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1203
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1204
    Author:     Olaf Mueller
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1205
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
  1206
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1207
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1208
    TrivEx
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1209
    TrivEx2