src/HOL/ROOT
author bulwahn
Thu, 30 May 2013 20:09:49 +0200
changeset 52248 2c893e0c1def
parent 52226 0d3165844048
child 52269 d867812da48b
permissions -rw-r--r--
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
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
  *}
48338
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
     7
  options [document_graph]
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
     8
  theories Complex_Main
48901
5e0455e29339 more basic file dependencies -- no load command here;
wenzelm
parents: 48765
diff changeset
     9
  files
5e0455e29339 more basic file dependencies -- no load command here;
wenzelm
parents: 48765
diff changeset
    10
    "Tools/Quickcheck/Narrowing_Engine.hs"
5e0455e29339 more basic file dependencies -- no load command here;
wenzelm
parents: 48765
diff changeset
    11
    "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
5e0455e29339 more basic file dependencies -- no load command here;
wenzelm
parents: 48765
diff changeset
    12
    "document/root.bib"
5e0455e29339 more basic file dependencies -- no load command here;
wenzelm
parents: 48765
diff changeset
    13
    "document/root.tex"
48338
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
    14
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
    15
session "HOL-Proofs" = Pure +
51421
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
    16
  description {*
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
    17
    HOL-Main with explicit proof terms.
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
    18
  *}
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
    19
  options [document = false, proofs = 2, skip_proofs = false]
48338
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
    20
  theories Main
48901
5e0455e29339 more basic file dependencies -- no load command here;
wenzelm
parents: 48765
diff changeset
    21
  files
5e0455e29339 more basic file dependencies -- no load command here;
wenzelm
parents: 48765
diff changeset
    22
    "Tools/Quickcheck/Narrowing_Engine.hs"
5e0455e29339 more basic file dependencies -- no load command here;
wenzelm
parents: 48765
diff changeset
    23
    "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
48338
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
    24
50844
b95ff3744815 populate "main" session group, e.g. relevant for Isabelle/jEdit logic selection;
wenzelm
parents: 50833
diff changeset
    25
session "HOL-Library" (main) in Library = HOL +
51421
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
    26
  description {*
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
    27
    Classical Higher-order Logic -- batteries included.
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
    28
  *}
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    29
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    30
    Library
51161
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51160
diff changeset
    31
    (*conflicting type class instantiations*)
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    32
    List_lexord
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    33
    Sublist_Order
51115
7dbd6832a689 consolidation of library theories on product orders
haftmann
parents: 51093
diff changeset
    34
    Product_Lexorder
7dbd6832a689 consolidation of library theories on product orders
haftmann
parents: 51093
diff changeset
    35
    Product_Order
51161
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51160
diff changeset
    36
    Finite_Lattice
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51160
diff changeset
    37
    (*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
    38
    AList_Mapping
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51160
diff changeset
    39
    Code_Binary_Nat
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51160
diff changeset
    40
    Code_Char
48721
wenzelm
parents: 48690
diff changeset
    41
    (* Code_Prolog  FIXME cf. 76965c356d2a *)
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    42
    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
    43
    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
    44
    DAList
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51160
diff changeset
    45
    RBT_Mapping
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51160
diff changeset
    46
    RBT_Set
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51160
diff changeset
    47
    (*legacy tools*)
49985
5b4b0e4e5205 moved Refute to "HOL/Library" to speed up building "Main" even more
blanchet
parents: 49932
diff changeset
    48
    Refute
51161
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51160
diff changeset
    49
    Old_Recdef
48932
c6e679443adc actual use of (sos remote_csdp) via ISABELLE_FULL_TEST;
wenzelm
parents: 48901
diff changeset
    50
  theories [condition = ISABELLE_FULL_TEST]
c6e679443adc actual use of (sos remote_csdp) via ISABELLE_FULL_TEST;
wenzelm
parents: 48901
diff changeset
    51
    Sum_of_Squares_Remote
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    52
  files "document/root.bib" "document/root.tex"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    53
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
    54
session "HOL-Hahn_Banach" in Hahn_Banach = HOL +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    55
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    56
    Author:     Gertrud Bauer, TU Munich
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    57
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    58
    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
    59
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    60
    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
    61
    following H. Heuser, Funktionalanalysis, p. 228 -232. The Hahn-Banach
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    62
    theorem is one of the fundamental theorems of functioal analysis. It is a
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    63
    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
    64
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    65
    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
    66
    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
    67
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    68
    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
    69
    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
    70
    continous linearform on the whole vectorspace.
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    71
  *}
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    72
  options [document_graph]
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    73
  theories Hahn_Banach
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    74
  files "document/root.bib" "document/root.tex"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    75
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
    76
session "HOL-Induct" in Induct = HOL +
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    77
  description {*
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    78
    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
    79
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    80
    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
    81
    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
    82
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    83
    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
    84
    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
    85
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    86
    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
    87
    (see
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    88
    HREF="http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz).
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    89
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    90
    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
    91
    mutually recursive relations.
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    92
  *}
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    93
  theories [quick_and_dirty]
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    94
    Common_Patterns
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    95
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    96
    QuoDataType
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    97
    QuoNestedDataType
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    98
    Term
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    99
    SList
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   100
    ABexp
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   101
    Tree
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   102
    Ordinals
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   103
    Sigma_Algebra
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   104
    Comb
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   105
    PropLog
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   106
    Com
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   107
  files "document/root.tex"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   108
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   109
session "HOL-IMP" in IMP = HOL +
50870
b8606dd29783 hardwired document_variants, to prevent HOL-IMP's \snip choking on macros from isabellestags.sty;
wenzelm
parents: 50844
diff changeset
   110
  options [document_graph, document_variants=document]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   111
  theories [document = false]
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   112
    "~~/src/HOL/ex/Interpretation_with_Defs"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   113
    "~~/src/HOL/Library/While_Combinator"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   114
    "~~/src/HOL/Library/Char_ord"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   115
    "~~/src/HOL/Library/List_lexord"
51625
bd3358aac5d2 tuned document
nipkow
parents: 51562
diff changeset
   116
    "~~/src/HOL/Library/Quotient_List"
bd3358aac5d2 tuned document
nipkow
parents: 51562
diff changeset
   117
    "~~/src/HOL/Library/Extended"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   118
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   119
    BExp
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   120
    ASM
50050
fac2b27893ff new theory IMP/Finite_Reachable
nipkow
parents: 50023
diff changeset
   121
    Finite_Reachable
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   122
    Denotation
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   123
    Comp_Rev
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   124
    Poly_Types
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   125
    Sec_Typing
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   126
    Sec_TypingT
50161
4fc4237488ab tuned names
nipkow
parents: 50149
diff changeset
   127
    Def_Init_Sound_Big
4fc4237488ab tuned names
nipkow
parents: 50149
diff changeset
   128
    Def_Init_Sound_Small
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   129
    Live
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   130
    Live_True
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   131
    Hoare_Examples
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   132
    VC
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   133
    HoareT
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   134
    Collecting1
48765
fb1ed5230abc special code with lists no longer necessary, use sets
nipkow
parents: 48738
diff changeset
   135
    Collecting_Examples
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   136
    Abs_Int_Tests
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   137
    Abs_Int1_parity
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   138
    Abs_Int1_const
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   139
    Abs_Int3
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   140
    "Abs_Int_ITP/Abs_Int1_parity_ITP"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   141
    "Abs_Int_ITP/Abs_Int1_const_ITP"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   142
    "Abs_Int_ITP/Abs_Int3_ITP"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   143
    "Abs_Int_Den/Abs_Int_den2"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   144
    Procs_Dyn_Vars_Dyn
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   145
    Procs_Stat_Vars_Dyn
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   146
    Procs_Stat_Vars_Stat
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   147
    C_like
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   148
    OO
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   149
    Fold
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   150
  files "document/root.bib" "document/root.tex"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   151
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   152
session "HOL-IMPP" in IMPP = HOL +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   153
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   154
    Author:     David von Oheimb
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   155
    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
   156
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   157
    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
   158
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   159
    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
   160
    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
   161
    Local Variables" (http://isabelle.in.tum.de/Bali/papers/FSTTCS99.html).
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   162
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   163
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   164
  theories EvenOdd
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   165
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   166
session "HOL-Import" in Import = HOL +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   167
  options [document_graph]
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   168
  theories HOL_Light_Maps
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   169
  theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   170
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   171
session "HOL-Number_Theory" in Number_Theory = HOL +
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   172
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   173
  theories Number_Theory
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   174
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   175
session "HOL-Old_Number_Theory" in Old_Number_Theory = HOL +
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   176
  description {*
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   177
    Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   178
    Theorem, Wilson's Theorem, Quadratic Reciprocity.
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   179
  *}
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   180
  options [document_graph]
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   181
  theories [document = false]
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   182
    "~~/src/HOL/Library/Infinite_Set"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   183
    "~~/src/HOL/Library/Permutation"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   184
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   185
    Fib
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   186
    Factorization
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   187
    Chinese
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   188
    WilsonRuss
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   189
    WilsonBij
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   190
    Quadratic_Reciprocity
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   191
    Primes
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   192
    Pocklington
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   193
  files "document/root.tex"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   194
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   195
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
   196
  description {*
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   197
    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
   198
    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
   199
  *}
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   200
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   201
  theories Hoare
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   202
  files "document/root.bib" "document/root.tex"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   203
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   204
session "HOL-Hoare_Parallel" in Hoare_Parallel = HOL +
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   205
  description {*
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   206
    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
   207
    (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
   208
  *}
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   209
  options [document_graph]
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   210
  theories Hoare_Parallel
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   211
  files "document/root.bib" "document/root.tex"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   212
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   213
session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   214
  options [document = false, document_graph = false, browser_info = false]
51422
821a70e29e0b proper formatting, to facilitate line-based diff;
wenzelm
parents: 51421
diff changeset
   215
  theories
821a70e29e0b proper formatting, to facilitate line-based diff;
wenzelm
parents: 51421
diff changeset
   216
    Generate
821a70e29e0b proper formatting, to facilitate line-based diff;
wenzelm
parents: 51421
diff changeset
   217
    Generate_Binary_Nat
821a70e29e0b proper formatting, to facilitate line-based diff;
wenzelm
parents: 51421
diff changeset
   218
    Generate_Target_Nat
821a70e29e0b proper formatting, to facilitate line-based diff;
wenzelm
parents: 51421
diff changeset
   219
    Generate_Efficient_Datastructures
821a70e29e0b proper formatting, to facilitate line-based diff;
wenzelm
parents: 51421
diff changeset
   220
    Generate_Pretty_Char
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   221
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   222
session "HOL-Metis_Examples" in Metis_Examples = HOL +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   223
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   224
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   225
    Author:     Jasmin Blanchette, TU Muenchen
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   226
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   227
    Testing Metis and Sledgehammer.
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   228
  *}
48679
5741f2152f5e some timeouts, which modify the build order;
wenzelm
parents: 48636
diff changeset
   229
  options [timeout = 3600, document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   230
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   231
    Abstraction
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   232
    Big_O
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   233
    Binary_Tree
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   234
    Clausification
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   235
    Message
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   236
    Proxies
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   237
    Tarski
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   238
    Trans_Closure
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   239
    Sets
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   240
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   241
session "HOL-Nitpick_Examples" in Nitpick_Examples = HOL +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   242
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   243
    Author:     Jasmin Blanchette, TU Muenchen
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   244
    Copyright   2009
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   245
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   246
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   247
  theories [quick_and_dirty] Nitpick_Examples
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   248
50844
b95ff3744815 populate "main" session group, e.g. relevant for Isabelle/jEdit logic selection;
wenzelm
parents: 50833
diff changeset
   249
session "HOL-Algebra" (main) in Algebra = HOL +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   250
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   251
    Author: Clemens Ballarin, started 24 September 1999
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   252
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   253
    The Isabelle Algebraic Library.
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   254
  *}
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   255
  options [document_graph]
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   256
  theories [document = false]
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   257
    (* Preliminaries from set and number theory *)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   258
    "~~/src/HOL/Library/FuncSet"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   259
    "~~/src/HOL/Old_Number_Theory/Primes"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   260
    "~~/src/HOL/Library/Binomial"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   261
    "~~/src/HOL/Library/Permutation"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   262
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   263
    (*** New development, based on explicit structures ***)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   264
    (* Groups *)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   265
    FiniteProduct        (* Product operator for commutative groups *)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   266
    Sylow                (* Sylow's theorem *)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   267
    Bij                  (* Automorphism Groups *)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   268
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   269
    (* Rings *)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   270
    Divisibility         (* Rings *)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   271
    IntRing              (* Ideals and residue classes *)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   272
    UnivPoly             (* Polynomials *)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   273
  files "document/root.bib" "document/root.tex"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   274
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   275
session "HOL-Auth" in Auth = HOL +
51421
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   276
  description {*
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   277
    A new approach to verifying authentication protocols.
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   278
  *}
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   279
  options [document_graph]
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   280
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   281
    Auth_Shared
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   282
    Auth_Public
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   283
    "Smartcard/Auth_Smartcard"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   284
    "Guard/Auth_Guard_Shared"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   285
    "Guard/Auth_Guard_Public"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   286
  files "document/root.tex"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   287
51236
f301ad90c48b more explicit session dependency, for improved parallel performance of HOL-UNITY test session -- NB: separate 'theories' sections are sequential;
wenzelm
parents: 51161
diff changeset
   288
session "HOL-UNITY" in UNITY = "HOL-Auth" +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   289
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   290
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   291
    Copyright   1998  University of Cambridge
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   292
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   293
    Verifying security protocols using Chandy and Misra's UNITY formalism.
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   294
  *}
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   295
  options [document_graph]
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   296
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   297
    (*Basic meta-theory*)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   298
    "UNITY_Main"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   299
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   300
    (*Simple examples: no composition*)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   301
    "Simple/Deadlock"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   302
    "Simple/Common"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   303
    "Simple/Network"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   304
    "Simple/Token"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   305
    "Simple/Channel"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   306
    "Simple/Lift"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   307
    "Simple/Mutex"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   308
    "Simple/Reach"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   309
    "Simple/Reachability"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   310
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   311
    (*Verifying security protocols using UNITY*)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   312
    "Simple/NSP_Bad"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   313
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   314
    (*Example of composition*)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   315
    "Comp/Handshake"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   316
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   317
    (*Universal properties examples*)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   318
    "Comp/Counter"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   319
    "Comp/Counterc"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   320
    "Comp/Priority"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   321
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   322
    "Comp/TimerArray"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   323
    "Comp/Progress"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   324
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   325
    "Comp/Alloc"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   326
    "Comp/AllocImpl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   327
    "Comp/Client"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   328
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   329
    (*obsolete*)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   330
    "ELT"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   331
  files "document/root.tex"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   332
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   333
session "HOL-Unix" in Unix = HOL +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   334
  options [print_mode = "no_brackets,no_type_brackets"]
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   335
  theories Unix
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   336
  files "document/root.bib" "document/root.tex"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   337
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   338
session "HOL-ZF" in ZF = HOL +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   339
  theories MainZF Games
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   340
  files "document/root.tex"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   341
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   342
session "HOL-Imperative_HOL" in Imperative_HOL = HOL +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   343
  options [document_graph, print_mode = "iff,no_brackets"]
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   344
  theories [document = false]
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   345
    "~~/src/HOL/Library/Countable"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   346
    "~~/src/HOL/Library/Monad_Syntax"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   347
    "~~/src/HOL/Library/LaTeXsugar"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   348
  theories Imperative_HOL_ex
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   349
  files "document/root.bib" "document/root.tex"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   350
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   351
session "HOL-Decision_Procs" in Decision_Procs = HOL +
51544
8c58fbbc1d5a tuned session specification;
wenzelm
parents: 51517
diff changeset
   352
  description {*
8c58fbbc1d5a tuned session specification;
wenzelm
parents: 51517
diff changeset
   353
    Various decision procedures, typically involving reflection.
8c58fbbc1d5a tuned session specification;
wenzelm
parents: 51517
diff changeset
   354
  *}
48496
a7eed34cf219 added condition = ISABELLE_POLYML according to no-smlnj targets in IsaMakefile;
wenzelm
parents: 48493
diff changeset
   355
  options [condition = ISABELLE_POLYML, document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   356
  theories Decision_Procs
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   357
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   358
session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
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
   359
  options [document = false, proofs = 2, skip_proofs = false, parallel_proofs = 0]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   360
  theories Hilbert_Classical
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   361
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   362
session "HOL-Proofs-Extraction" in "Proofs/Extraction" = "HOL-Proofs" +
51421
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   363
  description {*
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   364
    Examples for program extraction in Higher-Order Logic.
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   365
  *}
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
   366
  options [condition = ISABELLE_POLYML, proofs = 2, skip_proofs = false, parallel_proofs = 0]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   367
  theories [document = false]
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51115
diff changeset
   368
    "~~/src/HOL/Library/Code_Target_Numeral"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   369
    "~~/src/HOL/Library/Monad_Syntax"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   370
    "~~/src/HOL/Number_Theory/Primes"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   371
    "~~/src/HOL/Number_Theory/UniqueFactorization"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   372
    "~~/src/HOL/Library/State_Monad"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   373
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   374
    Greatest_Common_Divisor
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   375
    Warshall
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   376
    Higman_Extraction
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   377
    Pigeonhole
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   378
    Euclid
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   379
  files "document/root.bib" "document/root.tex"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   380
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   381
session "HOL-Proofs-Lambda" in "Proofs/Lambda" = "HOL-Proofs" +
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   382
  description {*
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   383
    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
   384
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   385
    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
   386
    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
   387
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   388
    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
   389
    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
   390
  *}
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
   391
  options [document_graph, print_mode = "no_brackets", proofs = 2, 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
   392
    parallel_proofs = 0]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   393
  theories [document = false]
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51115
diff changeset
   394
    "~~/src/HOL/Library/Code_Target_Int"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   395
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   396
    Eta
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   397
    StrongNorm
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   398
    Standardization
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   399
    WeakNorm
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   400
  files "document/root.bib" "document/root.tex"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   401
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   402
session "HOL-Prolog" in Prolog = HOL +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   403
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   404
    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
   405
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   406
    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
   407
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   408
    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
   409
    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
   410
    a little functional language and its type system.
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   411
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   412
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   413
  theories Test Type
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   414
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   415
session "HOL-MicroJava" in MicroJava = HOL +
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   416
  description {*
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   417
    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
   418
    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
   419
    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
   420
  *}
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   421
  options [document_graph]
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   422
  theories [document = false] "~~/src/HOL/Library/While_Combinator"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   423
  theories MicroJava
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   424
  files
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   425
    "document/introduction.tex"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   426
    "document/root.bib"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   427
    "document/root.tex"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   428
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   429
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
   430
  description {*
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   431
    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
   432
  *}
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   433
  options [document_graph]
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   434
  theories Example
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   435
  files "document/root.bib" "document/root.tex"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   436
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   437
session "HOL-Bali" in Bali = HOL +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   438
  options [document_graph]
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   439
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   440
    AxExample
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   441
    AxSound
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   442
    AxCompl
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   443
    Trans
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   444
  files "document/root.tex"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   445
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   446
session "HOL-IOA" in IOA = HOL +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   447
  description {*
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   448
    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
   449
    Copyright   1994--1996  TU Muenchen
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   450
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   451
    The meta theory of I/O-Automata in HOL. This formalization has been
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   452
    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
   453
    proofs of two communication protocols which formerly have been here.
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   454
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   455
    @inproceedings{Nipkow-Slind-IOA,
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   456
    author={Tobias Nipkow and Konrad Slind},
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   457
    title={{I/O} Automata in {Isabelle/HOL}},
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   458
    booktitle={Proc.\ TYPES Workshop 1994},
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   459
    publisher=Springer,
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   460
    series=LNCS,
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   461
    note={To appear}}
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   462
    ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   463
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   464
    and
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   465
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   466
    @inproceedings{Mueller-Nipkow,
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   467
    author={Olaf M\"uller and Tobias Nipkow},
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   468
    title={Combining Model Checking and Deduction for {I/O}-Automata},
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   469
    booktitle={Proc.\ TACAS Workshop},
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   470
    organization={Aarhus University, BRICS report},
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   471
    year=1995}
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   472
    ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   473
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   474
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   475
  theories Solve
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   476
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   477
session "HOL-Lattice" in Lattice = HOL +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   478
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   479
    Author:     Markus Wenzel, TU Muenchen
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   480
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   481
    Basic theory of lattices and orders.
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   482
  *}
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   483
  theories CompleteLattice
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   484
  files "document/root.tex"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   485
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   486
session "HOL-ex" in ex = HOL +
51421
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   487
  description {*
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   488
    Miscellaneous examples for Higher-Order Logic.
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   489
  *}
48679
5741f2152f5e some timeouts, which modify the build order;
wenzelm
parents: 48636
diff changeset
   490
  options [timeout = 3600, condition = ISABELLE_POLYML]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   491
  theories [document = false]
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   492
    "~~/src/HOL/Library/State_Monad"
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents: 49985
diff changeset
   493
    Code_Binary_Nat_examples
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   494
    "~~/src/HOL/Library/FuncSet"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   495
    Eval_Examples
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   496
    Normalization_by_Evaluation
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   497
    Hebrew
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   498
    Chinese
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   499
    Serbian
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   500
    "~~/src/HOL/Library/FinFun_Syntax"
49985
5b4b0e4e5205 moved Refute to "HOL/Library" to speed up building "Main" even more
blanchet
parents: 49932
diff changeset
   501
    "~~/src/HOL/Library/Refute"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   502
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   503
    Iff_Oracle
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   504
    Coercion_Examples
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   505
    Numeral_Representation
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   506
    Higher_Order_Logic
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   507
    Abstract_NAT
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   508
    Guess
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   509
    Fundefs
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   510
    Induction_Schema
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   511
    LocaleTest2
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   512
    Records
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   513
    While_Combinator_Example
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   514
    MonoidGroup
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   515
    BinEx
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   516
    Hex_Bin_Examples
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   517
    Antiquote
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   518
    Multiquote
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   519
    PER
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   520
    NatSum
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   521
    ThreeDivides
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   522
    Intuitionistic
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   523
    CTL
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   524
    Arith_Examples
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   525
    BT
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   526
    Tree23
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   527
    MergeSort
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   528
    Lagrange
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   529
    Groebner_Examples
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   530
    MT
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   531
    Unification
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   532
    Primrec
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   533
    Tarski
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   534
    Classical
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   535
    Set_Theory
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   536
    Termination
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   537
    Coherent
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   538
    PresburgerEx
51093
9d7aa2bb097b tuned, particulary name
haftmann
parents: 50988
diff changeset
   539
    Reflection_Examples
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   540
    Sqrt
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   541
    Sqrt_Script
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   542
    Transfer_Ex
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   543
    Transfer_Int_Nat
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   544
    HarmonicSeries
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   545
    Refute_Examples
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   546
    Execute_Choice
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   547
    Summation
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   548
    Gauge_Integration
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   549
    Dedekind_Real
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   550
    Quicksort
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   551
    Birthday_Paradox
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   552
    List_to_Set_Comprehension_Examples
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   553
    Seq
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   554
    Simproc_Tests
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   555
    Executable_Relation
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   556
    FinFunPred
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   557
    Set_Comprehension_Pointfree_Tests
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   558
    Parallel_Example
50138
ca989d793b34 new theory of immutable arrays
nipkow
parents: 50050
diff changeset
   559
    IArray_Examples
51559
wenzelm
parents: 51558
diff changeset
   560
    SVC_Oracle
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
   561
  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
   562
    Meson_Test
48690
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
   563
  theories [condition = SVC_HOME]
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
   564
    svc_test
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   565
  theories [condition = ZCHAFF_HOME]
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   566
    (*requires zChaff (or some other reasonably fast SAT solver)*)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   567
    Sudoku
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   568
(* FIXME
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   569
(*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   570
(*global side-effects ahead!*)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   571
try use_thy "SAT_Examples";   (* FIXME try!? (not really a proper test) *)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   572
*)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   573
  files "document/root.bib" "document/root.tex"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   574
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   575
session "HOL-Isar_Examples" in Isar_Examples = HOL +
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   576
  description {*
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   577
    Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   578
  *}
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   579
  theories [document = false]
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   580
    "~~/src/HOL/Library/Lattice_Syntax"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   581
    "../Number_Theory/Primes"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   582
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   583
    Basic_Logic
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   584
    Cantor
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   585
    Drinker
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   586
    Expr_Compiler
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   587
    Fibonacci
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   588
    Group
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   589
    Group_Context
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   590
    Group_Notepad
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   591
    Hoare_Ex
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   592
    Knaster_Tarski
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   593
    Mutilated_Checkerboard
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   594
    Nested_Datatype
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   595
    Peirce
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   596
    Puzzle
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   597
    Summation
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   598
  files
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   599
    "document/root.bib"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   600
    "document/root.tex"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   601
    "document/style.tex"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   602
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   603
session "HOL-SET_Protocol" in SET_Protocol = HOL +
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   604
  description {*
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   605
    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
   606
  *}
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   607
  options [document_graph]
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   608
  theories [document = false] "~~/src/HOL/Library/Nat_Bijection"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   609
  theories SET_Protocol
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   610
  files "document/root.tex"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   611
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   612
session "HOL-Matrix_LP" in Matrix_LP = HOL +
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   613
  description {*
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   614
    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
   615
  *}
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   616
  options [document_graph]
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   617
  theories Cplex
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   618
  files "document/root.tex"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   619
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   620
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
   621
  description {*
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   622
    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
   623
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   624
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   625
  theories TLA
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   626
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   627
session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" +
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   628
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   629
  theories Inc
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   630
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   631
session "HOL-TLA-Buffer" in "TLA/Buffer" = "HOL-TLA" +
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   632
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   633
  theories DBuffer
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   634
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   635
session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" +
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   636
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   637
  theories MemoryImplementation
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   638
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   639
session "HOL-TPTP" in TPTP = HOL +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   640
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   641
    Author:     Jasmin Blanchette, TU Muenchen
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   642
    Author:     Nik Sultana, University of Cambridge
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   643
    Copyright   2011
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   644
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   645
    TPTP-related extensions.
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   646
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   647
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   648
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   649
    ATP_Theory_Export
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   650
    MaSh_Eval
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   651
    MaSh_Export
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   652
    TPTP_Interpret
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   653
    THF_Arith
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   654
  theories [proofs = 0]  (* FIXME !? *)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   655
    ATP_Problem_Import
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   656
50844
b95ff3744815 populate "main" session group, e.g. relevant for Isabelle/jEdit logic selection;
wenzelm
parents: 50833
diff changeset
   657
session "HOL-Multivariate_Analysis" (main) in Multivariate_Analysis = HOL +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   658
  options [document_graph]
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   659
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   660
    Multivariate_Analysis
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   661
    Determinants
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   662
  files
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   663
    "document/root.tex"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   664
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   665
session "HOL-Probability" in "Probability" = "HOL-Multivariate_Analysis" +
48617
f4e9288fdbfc HOL-Probability appears to work with smlnj;
wenzelm
parents: 48614
diff changeset
   666
  options [document_graph]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   667
  theories [document = false]
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   668
    "~~/src/HOL/Library/Countable"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   669
    "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   670
    "~~/src/HOL/Library/Permutation"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   671
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   672
    Probability
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   673
    "ex/Dining_Cryptographers"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   674
    "ex/Koepf_Duermuth_Countermeasure"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   675
  files "document/root.tex"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   676
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   677
session "HOL-Nominal" (main) in Nominal = HOL +
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   678
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   679
  theories Nominal
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   680
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   681
session "HOL-Nominal-Examples" in "Nominal/Examples" = "HOL-Nominal" +
48679
5741f2152f5e some timeouts, which modify the build order;
wenzelm
parents: 48636
diff changeset
   682
  options [timeout = 3600, condition = ISABELLE_POLYML, document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   683
  theories Nominal_Examples
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   684
  theories [quick_and_dirty] VC_Condition
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   685
49310
6e30078de4f0 renamed "Ordinals_and_Cardinals" to "Cardinals"
blanchet
parents: 49110
diff changeset
   686
session "HOL-Cardinals-Base" in Cardinals = HOL +
51421
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   687
  description {*
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   688
    Ordinals and Cardinals, Base Theories.
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   689
  *}
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents: 48932
diff changeset
   690
  options [document = false]
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents: 48932
diff changeset
   691
  theories Cardinal_Arithmetic
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents: 48932
diff changeset
   692
49310
6e30078de4f0 renamed "Ordinals_and_Cardinals" to "Cardinals"
blanchet
parents: 49110
diff changeset
   693
session "HOL-Cardinals" in Cardinals = "HOL-Cardinals-Base" +
51421
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   694
  description {*
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   695
    Ordinals and Cardinals, Full Theories.
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   696
  *}
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
   697
  options [document = false]
49439
80b1963215c8 added top-level theory for Cardinals
popescua
parents: 49404
diff changeset
   698
  theories Cardinals
48984
f51d4a302962 do not hardwire document output options -- to be provided by the user;
wenzelm
parents: 48978
diff changeset
   699
  files
f51d4a302962 do not hardwire document output options -- to be provided by the user;
wenzelm
parents: 48978
diff changeset
   700
    "document/intro.tex"
f51d4a302962 do not hardwire document output options -- to be provided by the user;
wenzelm
parents: 48978
diff changeset
   701
    "document/root.tex"
f51d4a302962 do not hardwire document output options -- to be provided by the user;
wenzelm
parents: 48978
diff changeset
   702
    "document/root.bib"
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents: 48932
diff changeset
   703
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
   704
session "HOL-BNF-LFP" in BNF = "HOL-Cardinals-Base" +
51421
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   705
  description {*
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   706
    Bounded Natural Functors for Datatypes.
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   707
  *}
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
   708
  options [document = false]
9f5bfef8bd82 created separate session "HOL-BNF-LFP" as a step towards eventual integration in "HOL" in the middle term
blanchet
parents: 49510
diff changeset
   709
  theories BNF_LFP
9f5bfef8bd82 created separate session "HOL-BNF-LFP" as a step towards eventual integration in "HOL" in the middle term
blanchet
parents: 49510
diff changeset
   710
49517
c473c8749cd1 changed base session for "HOL-BNF" for faster building in the typical case
blanchet
parents: 49511
diff changeset
   711
session "HOL-BNF" in BNF = "HOL-Cardinals" +
51421
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   712
  description {*
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   713
    Bounded Natural Functors for (Co)datatypes.
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   714
  *}
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents: 48932
diff changeset
   715
  options [document = false]
49510
ba50d204095e renamed "Codatatype" directory "BNF" (and corresponding session) -- this opens the door to no-nonsense session names like "HOL-BNF-LFP"
blanchet
parents: 49483
diff changeset
   716
  theories BNF
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents: 48932
diff changeset
   717
49510
ba50d204095e renamed "Codatatype" directory "BNF" (and corresponding session) -- this opens the door to no-nonsense session names like "HOL-BNF-LFP"
blanchet
parents: 49483
diff changeset
   718
session "HOL-BNF-Examples" in "BNF/Examples" = "HOL-BNF" +
51421
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   719
  description {*
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   720
    Examples for Bounded Natural Functors.
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   721
  *}
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
   722
  options [document = false]
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents: 48932
diff changeset
   723
  theories
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents: 48932
diff changeset
   724
    Lambda_Term
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents: 48932
diff changeset
   725
    Process
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents: 48932
diff changeset
   726
    TreeFsetI
49872
c6a686c9be2a update ROOT with teh directory change in BNF
popescua
parents: 49693
diff changeset
   727
    "Derivation_Trees/Gram_Lang"
c6a686c9be2a update ROOT with teh directory change in BNF
popescua
parents: 49693
diff changeset
   728
    "Derivation_Trees/Parallel"
50517
8f6c11103820 renamed theory
traytel
parents: 50480
diff changeset
   729
    Koenig
49693
393d7242adaf thread the right local theory through + reenable parallel proofs for previously problematic theories
blanchet
parents: 49601
diff changeset
   730
  theories [condition = ISABELLE_FULL_TEST]
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents: 48932
diff changeset
   731
    Misc_Codata
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents: 48932
diff changeset
   732
    Misc_Data
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents: 48932
diff changeset
   733
50844
b95ff3744815 populate "main" session group, e.g. relevant for Isabelle/jEdit logic selection;
wenzelm
parents: 50833
diff changeset
   734
session "HOL-Word" (main) in Word = HOL +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   735
  options [document_graph]
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   736
  theories Word
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   737
  files "document/root.bib" "document/root.tex"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   738
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   739
session "HOL-Word-Examples" in "Word/Examples" = "HOL-Word" +
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   740
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   741
  theories WordExamples
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   742
52248
2c893e0c1def added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents: 52226
diff changeset
   743
session "HOL-Spec_Check" in Spec_Check = HOL +
2c893e0c1def added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents: 52226
diff changeset
   744
  theories
2c893e0c1def added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents: 52226
diff changeset
   745
    Examples
2c893e0c1def added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents: 52226
diff changeset
   746
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   747
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
   748
  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
   749
    StateSpaceEx
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   750
  files "document/root.tex"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   751
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   752
session "HOL-NSA" in NSA = HOL +
51421
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   753
  description {*
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   754
    Nonstandard analysis.
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   755
  *}
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   756
  options [document_graph]
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   757
  theories Hypercomplex
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   758
  files "document/root.tex"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   759
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   760
session "HOL-NSA-Examples" in "NSA/Examples" = "HOL-NSA" +
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   761
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   762
  theories NSPrimes
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   763
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   764
session "HOL-Mirabelle" in Mirabelle = HOL +
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   765
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   766
  theories Mirabelle_Test
48589
fb446a780d50 separate session HOL-Mirabelle-ex -- cannot run isolated shell scripts within build tool;
wenzelm
parents: 48588
diff changeset
   767
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   768
session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
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
   769
  options [document = false, timeout = 60]
8a232a4e3fd8 reactivate HOL-Mirabelle-ex with increased chances that it works most of the time (cf. bec1add86e79, a93d920707bb, be27a453aacc);
wenzelm
parents: 49439
diff changeset
   770
  theories Ex
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   771
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   772
session "HOL-Word-SMT_Examples" in SMT_Examples = "HOL-Word" +
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   773
  options [document = false, quick_and_dirty]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   774
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   775
    SMT_Examples
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   776
    SMT_Word_Examples
50666
6f48853f08d5 actually run Z3 for "SMT_Tests" when "ISABELLE_FULL_TEST" is enabled
blanchet
parents: 50665
diff changeset
   777
  theories [condition = ISABELLE_FULL_TEST]
6f48853f08d5 actually run Z3 for "SMT_Tests" when "ISABELLE_FULL_TEST" is enabled
blanchet
parents: 50665
diff changeset
   778
    SMT_Tests
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   779
  files
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   780
    "SMT_Examples.certs"
50665
c9daeff9516e added missing certificate file to "ROOT"
blanchet
parents: 50634
diff changeset
   781
    "SMT_Word_Examples.certs"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   782
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   783
session "HOL-Boogie" in "Boogie" = "HOL-Word" +
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   784
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   785
  theories Boogie
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   786
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   787
session "HOL-Boogie-Examples" in "Boogie/Examples" = "HOL-Boogie" +
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   788
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   789
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   790
    Boogie_Max_Stepwise
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   791
    Boogie_Max
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   792
    Boogie_Dijkstra
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   793
    VCC_Max
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   794
  files
48493
142ab4ff8fa8 more files;
wenzelm
parents: 48492
diff changeset
   795
    "Boogie_Dijkstra.b2i"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   796
    "Boogie_Dijkstra.certs"
48493
142ab4ff8fa8 more files;
wenzelm
parents: 48492
diff changeset
   797
    "Boogie_Max.b2i"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   798
    "Boogie_Max.certs"
48493
142ab4ff8fa8 more files;
wenzelm
parents: 48492
diff changeset
   799
    "VCC_Max.b2i"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   800
    "VCC_Max.certs"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   801
50844
b95ff3744815 populate "main" session group, e.g. relevant for Isabelle/jEdit logic selection;
wenzelm
parents: 50833
diff changeset
   802
session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" +
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   803
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   804
  theories SPARK
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   805
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   806
session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   807
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   808
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   809
    "Gcd/Greatest_Common_Divisor"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   810
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   811
    "Liseq/Longest_Increasing_Subsequence"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   812
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   813
    "RIPEMD-160/F"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   814
    "RIPEMD-160/Hash"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   815
    "RIPEMD-160/K_L"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   816
    "RIPEMD-160/K_R"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   817
    "RIPEMD-160/R_L"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   818
    "RIPEMD-160/Round"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   819
    "RIPEMD-160/R_R"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   820
    "RIPEMD-160/S_L"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   821
    "RIPEMD-160/S_R"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   822
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   823
    "Sqrt/Sqrt"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   824
  files
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   825
    "Gcd/greatest_common_divisor/g_c_d.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   826
    "Gcd/greatest_common_divisor/g_c_d.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   827
    "Gcd/greatest_common_divisor/g_c_d.siv"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   828
    "Liseq/liseq/liseq_length.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   829
    "Liseq/liseq/liseq_length.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   830
    "Liseq/liseq/liseq_length.siv"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   831
    "RIPEMD-160/rmd/f.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   832
    "RIPEMD-160/rmd/f.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   833
    "RIPEMD-160/rmd/f.siv"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   834
    "RIPEMD-160/rmd/hash.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   835
    "RIPEMD-160/rmd/hash.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   836
    "RIPEMD-160/rmd/hash.siv"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   837
    "RIPEMD-160/rmd/k_l.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   838
    "RIPEMD-160/rmd/k_l.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   839
    "RIPEMD-160/rmd/k_l.siv"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   840
    "RIPEMD-160/rmd/k_r.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   841
    "RIPEMD-160/rmd/k_r.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   842
    "RIPEMD-160/rmd/k_r.siv"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   843
    "RIPEMD-160/rmd/r_l.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   844
    "RIPEMD-160/rmd/r_l.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   845
    "RIPEMD-160/rmd/r_l.siv"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   846
    "RIPEMD-160/rmd/round.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   847
    "RIPEMD-160/rmd/round.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   848
    "RIPEMD-160/rmd/round.siv"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   849
    "RIPEMD-160/rmd/r_r.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   850
    "RIPEMD-160/rmd/r_r.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   851
    "RIPEMD-160/rmd/r_r.siv"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   852
    "RIPEMD-160/rmd/s_l.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   853
    "RIPEMD-160/rmd/s_l.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   854
    "RIPEMD-160/rmd/s_l.siv"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   855
    "RIPEMD-160/rmd/s_r.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   856
    "RIPEMD-160/rmd/s_r.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   857
    "RIPEMD-160/rmd/s_r.siv"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   858
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   859
session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +
48486
691d0b44a793 more build options;
wenzelm
parents: 48483
diff changeset
   860
  options [show_question_marks = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   861
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   862
    Example_Verification
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   863
    VC_Principles
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   864
    Reference
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   865
    Complex_Types
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   866
  files
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   867
    "complex_types_app/initialize.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   868
    "complex_types_app/initialize.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   869
    "complex_types_app/initialize.siv"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   870
    "document/complex_types.ads"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   871
    "document/complex_types_app.adb"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   872
    "document/complex_types_app.ads"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   873
    "document/Gcd.adb"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   874
    "document/Gcd.ads"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   875
    "document/intro.tex"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   876
    "document/loop_invariant.adb"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   877
    "document/loop_invariant.ads"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   878
    "document/root.bib"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   879
    "document/root.tex"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   880
    "document/Simple_Gcd.adb"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   881
    "document/Simple_Gcd.ads"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   882
    "loop_invariant/proc1.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   883
    "loop_invariant/proc1.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   884
    "loop_invariant/proc1.siv"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   885
    "loop_invariant/proc2.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   886
    "loop_invariant/proc2.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   887
    "loop_invariant/proc2.siv"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   888
    "simple_greatest_common_divisor/g_c_d.fdl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   889
    "simple_greatest_common_divisor/g_c_d.rls"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   890
    "simple_greatest_common_divisor/g_c_d.siv"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   891
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   892
session "HOL-Mutabelle" in Mutabelle = HOL +
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   893
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   894
  theories MutabelleExtra
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   895
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   896
session "HOL-Quickcheck_Examples" in Quickcheck_Examples = HOL +
50179
978200ae8473 timeout in proper place (HOL-Quickcheck_Examples approx. 1min, HOL-Quickcheck_Benchmark approx. 1h);
wenzelm
parents: 50161
diff changeset
   897
  options [document = false]
48588
23456b2a769d added Quickcheck_Benchmark (cf. 1959baa22632);
wenzelm
parents: 48512
diff changeset
   898
  theories
48690
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
   899
    Quickcheck_Examples
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
   900
  (* FIXME
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
   901
    Quickcheck_Lattice_Examples
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
   902
    Completeness
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
   903
    Quickcheck_Interfaces
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
   904
    Hotel_Example *)
48598
7f4561d43d39 updated ROOT according to 3defa60a7ae3;
wenzelm
parents: 48589
diff changeset
   905
  theories [condition = ISABELLE_GHC]
7f4561d43d39 updated ROOT according to 3defa60a7ae3;
wenzelm
parents: 48589
diff changeset
   906
    Quickcheck_Narrowing_Examples
48588
23456b2a769d added Quickcheck_Benchmark (cf. 1959baa22632);
wenzelm
parents: 48512
diff changeset
   907
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   908
session "HOL-Quickcheck_Benchmark" in Quickcheck_Benchmark = HOL +
50571
b649e33e4821 HOL-Quickcheck_Benchmark works without timeout (NB: isatest imposes global timeout already);
wenzelm
parents: 50568
diff changeset
   909
  theories [condition = ISABELLE_FULL_TEST, quick_and_dirty]
50568
ee090b5712f3 reverting d466ebc27810 as the previous changeset should allow to run Find_Unused_Assms_Examples again
bulwahn
parents: 50517
diff changeset
   910
    Find_Unused_Assms_Examples
48618
1f7e068b4613 moved another larger quickcheck example to Quickcheck_Benchmark
bulwahn
parents: 48614
diff changeset
   911
    Needham_Schroeder_No_Attacker_Example
1f7e068b4613 moved another larger quickcheck example to Quickcheck_Benchmark
bulwahn
parents: 48614
diff changeset
   912
    Needham_Schroeder_Guided_Attacker_Example
48690
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
   913
    Needham_Schroeder_Unguided_Attacker_Example
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   914
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   915
session "HOL-Quotient_Examples" in Quotient_Examples = HOL +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   916
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   917
    Author:     Cezary Kaliszyk and Christian Urban
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   918
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   919
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   920
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   921
    DList
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   922
    FSet
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   923
    Quotient_Int
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   924
    Quotient_Message
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   925
    Lift_FSet
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   926
    Lift_Set
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   927
    Lift_Fun
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   928
    Quotient_Rat
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   929
    Lift_DList
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   930
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   931
session "HOL-Predicate_Compile_Examples" in Predicate_Compile_Examples = HOL +
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   932
  options [document = false]
48690
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
   933
  theories
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   934
    Examples
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   935
    Predicate_Compile_Tests
48690
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
   936
    (* FIXME
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
   937
    Predicate_Compile_Quickcheck_Examples  -- should be added again soon (since 21-Oct-2010) *)
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   938
    Specialisation_Examples
48690
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
   939
    (* FIXME since 21-Jul-2011
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
   940
    Hotel_Example_Small_Generator
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
   941
    IMP_1
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
   942
    IMP_2
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
   943
    IMP_3
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
   944
    IMP_4 *)
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
   945
  theories [condition = "ISABELLE_SWIPL"]  (* FIXME: *or* ISABELLE_YAP (??) *)
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
   946
    Code_Prolog_Examples
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
   947
    Context_Free_Grammar_Example
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
   948
    Hotel_Example_Prolog
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
   949
    Lambda_Example
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
   950
    List_Examples
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
   951
  theories [condition = "ISABELLE_SWIPL", quick_and_dirty]  (* FIXME: *or* ISABELLE_YAP (??) *)
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
   952
    Reg_Exp_Example
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   953
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   954
session HOLCF (main) in HOLCF = HOL +
48338
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
   955
  description {*
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
   956
    Author:     Franz Regensburger
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
   957
    Author:     Brian Huffman
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
   958
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
   959
    HOLCF -- a semantic extension of HOL by the LCF logic.
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
   960
  *}
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
   961
  options [document_graph]
48470
7483aa690b4f clarified "document" again, eliminated redundant "no_document";
wenzelm
parents: 48458
diff changeset
   962
  theories [document = false]
48338
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
   963
    "~~/src/HOL/Library/Nat_Bijection"
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
   964
    "~~/src/HOL/Library/Countable"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   965
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   966
    Plain_HOLCF
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   967
    Fixrec
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   968
    HOLCF
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   969
  files "document/root.tex"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   970
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   971
session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   972
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   973
    Domain_ex
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   974
    Fixrec_ex
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   975
    New_Domain
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   976
  files "document/root.tex"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   977
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   978
session "HOLCF-Library" in "HOLCF/Library" = HOLCF +
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   979
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   980
  theories HOLCF_Library
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   981
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   982
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
   983
  description {*
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   984
    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
   985
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   986
    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
   987
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   988
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   989
  theories HoareEx
48338
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
   990
  files "document/root.tex"
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
   991
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   992
session "HOLCF-ex" in "HOLCF/ex" = HOLCF +
51421
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   993
  description {*
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   994
    Miscellaneous examples for HOLCF.
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   995
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
   996
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   997
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   998
    Dnat
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   999
    Dagstuhl
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1000
    Focus_ex
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1001
    Fix2
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1002
    Hoare
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1003
    Concurrency_Monad
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1004
    Loop
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1005
    Powerdomain_ex
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1006
    Domain_Proofs
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1007
    Letrec
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1008
    Pattern_Match
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1009
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
  1010
session "HOLCF-FOCUS" in "HOLCF/FOCUS" = HOLCF +
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1011
  description {*
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1012
    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
  1013
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1014
    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
  1015
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1016
    "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
  1017
    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
  1018
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1019
    "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
  1020
    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
  1021
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1022
    "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
  1023
    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
  1024
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
  1025
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1026
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1027
    Fstreams
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1028
    FOCUS
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1029
    Buffer_adm
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1030
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
  1031
session IOA in "HOLCF/IOA" = HOLCF +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1032
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1033
    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
  1034
    Copyright   1997 TU München
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1035
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1036
    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
  1037
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1038
    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
  1039
    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
  1040
    finite and infinite sequences.
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1041
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
  1042
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1043
  theories "meta_theory/Abstraction"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1044
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
  1045
session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1046
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1047
    Author:     Olaf Mueller
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1048
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1049
    The Alternating Bit Protocol performed in I/O-Automata.
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1050
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
  1051
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1052
  theories Correctness
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1053
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
  1054
session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1055
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1056
    Author:     Tobias Nipkow & Konrad Slind
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1057
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1058
    A network transmission protocol, performed in the
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1059
    I/O automata formalization by Olaf Mueller.
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1060
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
  1061
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1062
  theories Correctness
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1063
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
  1064
session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1065
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1066
    Author:     Olaf Mueller
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1067
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1068
    Memory storage case study.
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1069
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
  1070
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1071
  theories Correctness
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1072
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
  1073
session "IOA-ex" in "HOLCF/IOA/ex" = IOA +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1074
  description {*
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1075
    Author:     Olaf Mueller
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1076
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
  1077
  options [document = false]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1078
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1079
    TrivEx
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1080
    TrivEx2
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1081
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
  1082
session "HOL-Datatype_Benchmark" in Datatype_Benchmark = HOL +
51421
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
  1083
  description {*
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
  1084
    Some rather large datatype examples (from John Harrison).
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
  1085
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
  1086
  options [document = false]
48635
bfce940c6f38 clarified ISABELLE_FULL_TEST;
wenzelm
parents: 48627
diff changeset
  1087
  theories [condition = ISABELLE_FULL_TEST, timing]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1088
    Brackin
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1089
    Instructions
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1090
    SML
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1091
    Verilog
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 "HOL-Record_Benchmark" in Record_Benchmark = HOL +
51421
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
  1094
  description {*
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
  1095
    Some benchmark on large record.
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
  1096
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48481
diff changeset
  1097
  options [document = false]
48635
bfce940c6f38 clarified ISABELLE_FULL_TEST;
wenzelm
parents: 48627
diff changeset
  1098
  theories [condition = ISABELLE_FULL_TEST, timing]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1099
    Record_Benchmark
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1100