src/HOL/ROOT
author Manuel Eberl <eberlm@in.tum.de>
Fri, 29 Mar 2024 19:28:59 +0100
changeset 80061 4c1347e172b1
parent 78890 d8045bc0544e
child 80084 173548e4d5d0
permissions -rw-r--r--
moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
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 +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
     4
  description "
51421
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
     5
    Classical Higher-order Logic.
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
     6
  "
70678
36c8c32346cb clarified syntax: 'directories' and 'theories' belong together;
wenzelm
parents: 70675
diff changeset
     7
  options [strict_facts]
70853
c92ae7b0f3f1 clarified sessions/directories;
wenzelm
parents: 70796
diff changeset
     8
  sessions Tools
70796
2739631ac368 discontinued pointless dump_checkpoint and share_common_data -- superseded by base logic image in Isabelle/MMT;
wenzelm
parents: 70781
diff changeset
     9
  theories
65374
a5b38d8d3c1e tuned syntax;
wenzelm
parents: 65099
diff changeset
    10
    Main (global)
a5b38d8d3c1e tuned syntax;
wenzelm
parents: 65099
diff changeset
    11
    Complex_Main (global)
72621
65554bac121b clarified document;
wenzelm
parents: 72601
diff changeset
    12
  document_theories
65554bac121b clarified document;
wenzelm
parents: 72601
diff changeset
    13
    Tools.Code_Generator
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
    14
  document_files
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
    15
    "root.bib"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
    16
    "root.tex"
48338
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
    17
71925
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents: 71924
diff changeset
    18
session "HOL-Examples" in Examples = HOL +
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents: 71924
diff changeset
    19
  description "
74286
641300b56ebe tuned comments;
wenzelm
parents: 74193
diff changeset
    20
    Notable Examples for Isabelle/HOL.
71925
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents: 71924
diff changeset
    21
  "
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents: 71924
diff changeset
    22
  sessions
73811
f143d0a4cb6a clarified examples;
wenzelm
parents: 73691
diff changeset
    23
    "HOL-Computational_Algebra"
71925
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents: 71924
diff changeset
    24
  theories
72029
83456d9f0ed5 clarified examples;
wenzelm
parents: 71989
diff changeset
    25
    Adhoc_Overloading_Examples
71930
35a2ac83a262 New Ackermann development
paulson <lp15@cam.ac.uk>
parents: 71926
diff changeset
    26
    Ackermann
72029
83456d9f0ed5 clarified examples;
wenzelm
parents: 71989
diff changeset
    27
    Cantor
83456d9f0ed5 clarified examples;
wenzelm
parents: 71989
diff changeset
    28
    Coherent
83456d9f0ed5 clarified examples;
wenzelm
parents: 71989
diff changeset
    29
    Commands
71925
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents: 71924
diff changeset
    30
    Drinker
74193
2b00c267196e reflect moved theories
nipkow
parents: 74107
diff changeset
    31
    Functions
75955
5305c65dcbb2 Gauss numbers
haftmann
parents: 75937
diff changeset
    32
    Gauss_Numbers
72029
83456d9f0ed5 clarified examples;
wenzelm
parents: 71989
diff changeset
    33
    Groebner_Examples
83456d9f0ed5 clarified examples;
wenzelm
parents: 71989
diff changeset
    34
    Iff_Oracle
83456d9f0ed5 clarified examples;
wenzelm
parents: 71989
diff changeset
    35
    Induction_Schema
83456d9f0ed5 clarified examples;
wenzelm
parents: 71989
diff changeset
    36
    Knaster_Tarski
83456d9f0ed5 clarified examples;
wenzelm
parents: 71989
diff changeset
    37
    "ML"
83456d9f0ed5 clarified examples;
wenzelm
parents: 71989
diff changeset
    38
    Peirce
83456d9f0ed5 clarified examples;
wenzelm
parents: 71989
diff changeset
    39
    Records
74888
1c50ddcf6a01 Rewrite: added links to docu, made more prominent
nipkow
parents: 74475
diff changeset
    40
    Rewrite_Examples
71925
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents: 71924
diff changeset
    41
    Seq
73811
f143d0a4cb6a clarified examples;
wenzelm
parents: 73691
diff changeset
    42
    Sqrt
71925
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents: 71924
diff changeset
    43
  document_files
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents: 71924
diff changeset
    44
    "root.bib"
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents: 71924
diff changeset
    45
    "root.tex"
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents: 71924
diff changeset
    46
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents: 71924
diff changeset
    47
70669
abdf3732f6f1 avoid overlapping session directories;
wenzelm
parents: 70660
diff changeset
    48
session "HOL-Proofs" (timing) in Proofs = Pure +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
    49
  description "
51421
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
    50
    HOL-Main with explicit proof terms.
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
    51
  "
70398
725438ceae7c proof terms are always constructed sequentially;
wenzelm
parents: 70250
diff changeset
    52
  options [quick_and_dirty = false, record_proofs = 2, parallel_limit = 500]
65543
8369b33fda0a clarified session imports;
wenzelm
parents: 65538
diff changeset
    53
  sessions
8369b33fda0a clarified session imports;
wenzelm
parents: 65538
diff changeset
    54
    "HOL-Library"
65530
09c00a304c00 include imports that morally belong to Main and are used in HOL-Proofs applications;
wenzelm
parents: 65509
diff changeset
    55
  theories
67319
07176d5b81d5 moved 'realizers' into their own theory, now that they are decupled from the old datatype construction
blanchet
parents: 67278
diff changeset
    56
    "HOL-Library.Realizers"
48338
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
    57
63888
5a9a1985e9fb sessions that are relevant for routine timing measurements;
wenzelm
parents: 63885
diff changeset
    58
session "HOL-Library" (main timing) in Library = HOL +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
    59
  description "
51421
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
    60
    Classical Higher-order Logic -- batteries included.
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
    61
  "
75916
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents: 75647
diff changeset
    62
  theories [document = false]
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents: 75647
diff changeset
    63
    README
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    64
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    65
    Library
64588
293ab573d034 clarified library contents
haftmann
parents: 64582
diff changeset
    66
    (*conflicting type class instantiations and dependent applications*)
293ab573d034 clarified library contents
haftmann
parents: 64582
diff changeset
    67
    Finite_Lattice
68312
e9b5f25f6712 canonical names
nipkow
parents: 68261
diff changeset
    68
    List_Lexorder
71766
1249b998e377 New theory Library/List_Lenlexorder.thy, a type class instantiation for well-ordering lists
paulson <lp15@cam.ac.uk>
parents: 71518
diff changeset
    69
    List_Lenlexorder
63763
0f61ea70d384 clarified session: use all theories in directory HOL/Library;
wenzelm
parents: 63731
diff changeset
    70
    Prefix_Order
51115
7dbd6832a689 consolidation of library theories on product orders
haftmann
parents: 51093
diff changeset
    71
    Product_Lexorder
7dbd6832a689 consolidation of library theories on product orders
haftmann
parents: 51093
diff changeset
    72
    Product_Order
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 65678
diff changeset
    73
    Subseq_Order
67611
7929240e44d4 records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents: 67319
diff changeset
    74
    (*conflicting syntax*)
7929240e44d4 records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents: 67319
diff changeset
    75
    Datatype_Records
51161
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51160
diff changeset
    76
    (*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
    77
    AList_Mapping
75937
02b18f59f903 streamlined
haftmann
parents: 75916
diff changeset
    78
    Code_Abstract_Char
51161
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51160
diff changeset
    79
    Code_Binary_Nat
55447
aa41ecbdc205 do not redefine outer syntax commands;
wenzelm
parents: 55417
diff changeset
    80
    Code_Prolog
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    81
    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
    82
    Code_Target_Numeral
73546
7cb3fefef79e confluent preprocessing for floats in presence of target language numerals
haftmann
parents: 73477
diff changeset
    83
    Code_Target_Numeral_Float
74475
409ca22dee4c new notion of infinite sums in HOL-Analysis, ordering on complex numbers
eberlm <eberlm@in.tum.de>
parents: 74365
diff changeset
    84
    Complex_Order
51161
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51160
diff changeset
    85
    DAList
54429
be1bc181bcde explicit inclusion of data refinement theory into HOL-Library session
haftmann
parents: 54193
diff changeset
    86
    DAList_Multiset
51161
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51160
diff changeset
    87
    RBT_Mapping
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51160
diff changeset
    88
    RBT_Set
66015
70643edecb7a specific output setup is not supposed to intrude regular import theory
haftmann
parents: 65956
diff changeset
    89
    (*printing modifications*)
70643edecb7a specific output setup is not supposed to intrude regular import theory
haftmann
parents: 65956
diff changeset
    90
    OptionalSugar
64588
293ab573d034 clarified library contents
haftmann
parents: 64582
diff changeset
    91
    (*prototypic tools*)
293ab573d034 clarified library contents
haftmann
parents: 64582
diff changeset
    92
    Predicate_Compile_Quickcheck
51161
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51160
diff changeset
    93
    (*legacy tools*)
58372
bfd497f2f4c2 moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer)
blanchet
parents: 58371
diff changeset
    94
    Old_Datatype
51161
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 51160
diff changeset
    95
    Old_Recdef
67319
07176d5b81d5 moved 'realizers' into their own theory, now that they are decupled from the old datatype construction
blanchet
parents: 67278
diff changeset
    96
    Realizers
64588
293ab573d034 clarified library contents
haftmann
parents: 64582
diff changeset
    97
    Refute
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
    98
  document_files "root.bib" "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
    99
66932
149025fecca0 reduced heap hierarchy, for potentially improved performance;
wenzelm
parents: 66842
diff changeset
   100
session "HOL-Analysis" (main timing) in Analysis = HOL +
78478
ab9cf0fdb268 no hardwired timeout in Isabelle distribution (unlike on AFP): reverting part of 74c75da4cb01 -- without further tinkering it breaks isabelle_cronjob builds;
wenzelm
parents: 78324
diff changeset
   101
  options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant",
67152
8021ea06aad8 just one session for bulky HOL-Analysis documents;
wenzelm
parents: 67122
diff changeset
   102
    document_variants = "document:manual=-proof,-ML,-unimportant"]
66932
149025fecca0 reduced heap hierarchy, for potentially improved performance;
wenzelm
parents: 66842
diff changeset
   103
  sessions
67152
8021ea06aad8 just one session for bulky HOL-Analysis documents;
wenzelm
parents: 67122
diff changeset
   104
    "HOL-Library"
73477
1d8a79aa2a99 dedicated session for combinatorial material
haftmann
parents: 73408
diff changeset
   105
    "HOL-Combinatorics"
66932
149025fecca0 reduced heap hierarchy, for potentially improved performance;
wenzelm
parents: 66842
diff changeset
   106
    "HOL-Computational_Algebra"
78890
d8045bc0544e Added Kronecker's approximation theorem. Requires adding Real_Asymp to HOL-Analysis. Funny syntax issue in Probability/Projective_Family
paulson <lp15@cam.ac.uk>
parents: 78676
diff changeset
   107
    "HOL-Real_Asymp"
d8045bc0544e Added Kronecker's approximation theorem. Requires adding Real_Asymp to HOL-Analysis. Funny syntax issue in Probability/Projective_Family
paulson <lp15@cam.ac.uk>
parents: 78676
diff changeset
   108
theories
65462
db1827610513 less global theories -- conflict with AFP entries;
wenzelm
parents: 65456
diff changeset
   109
    Analysis
65375
wenzelm
parents: 65374
diff changeset
   110
  document_files
wenzelm
parents: 65374
diff changeset
   111
    "root.tex"
69518
bf88364c9e94 tuned headers etc, added bib-file
nipkow
parents: 69319
diff changeset
   112
    "root.bib"
65375
wenzelm
parents: 65374
diff changeset
   113
71189
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents: 71042
diff changeset
   114
session "HOL-Complex_Analysis" (main timing) in Complex_Analysis = "HOL-Analysis" +
78478
ab9cf0fdb268 no hardwired timeout in Isabelle distribution (unlike on AFP): reverting part of 74c75da4cb01 -- without further tinkering it breaks isabelle_cronjob builds;
wenzelm
parents: 78324
diff changeset
   115
  options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant",
71189
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents: 71042
diff changeset
   116
    document_variants = "document:manual=-proof,-ML,-unimportant"]
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents: 71042
diff changeset
   117
  theories
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents: 71042
diff changeset
   118
    Complex_Analysis
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents: 71042
diff changeset
   119
  document_files
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents: 71042
diff changeset
   120
    "root.tex"
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents: 71042
diff changeset
   121
    "root.bib"
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents: 71042
diff changeset
   122
65375
wenzelm
parents: 65374
diff changeset
   123
session "HOL-Analysis-ex" in "Analysis/ex" = "HOL-Analysis" +
wenzelm
parents: 65374
diff changeset
   124
  theories
wenzelm
parents: 65374
diff changeset
   125
    Approximations
70956
860198428664 added examples for "metric" method, by Maximilian Schäffeler
immler
parents: 70853
diff changeset
   126
    Metric_Arith_Examples
65375
wenzelm
parents: 65374
diff changeset
   127
70151
78fffdfc6787 clarified group of "main" library sessions;
wenzelm
parents: 70089
diff changeset
   128
session "HOL-Homology" (timing) in Homology = "HOL-Analysis" +
78478
ab9cf0fdb268 no hardwired timeout in Isabelle distribution (unlike on AFP): reverting part of 74c75da4cb01 -- without further tinkering it breaks isabelle_cronjob builds;
wenzelm
parents: 78324
diff changeset
   129
  options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant",
70089
eca8611201e9 new Homology target, depending on HOL-Algebra and HOL-Analysis
paulson <lp15@cam.ac.uk>
parents: 70086
diff changeset
   130
    document_variants = "document:manual=-proof,-ML,-unimportant"]
eca8611201e9 new Homology target, depending on HOL-Algebra and HOL-Analysis
paulson <lp15@cam.ac.uk>
parents: 70086
diff changeset
   131
  sessions
eca8611201e9 new Homology target, depending on HOL-Algebra and HOL-Analysis
paulson <lp15@cam.ac.uk>
parents: 70086
diff changeset
   132
    "HOL-Algebra"
eca8611201e9 new Homology target, depending on HOL-Algebra and HOL-Analysis
paulson <lp15@cam.ac.uk>
parents: 70086
diff changeset
   133
  theories
eca8611201e9 new Homology target, depending on HOL-Algebra and HOL-Analysis
paulson <lp15@cam.ac.uk>
parents: 70086
diff changeset
   134
    Homology
eca8611201e9 new Homology target, depending on HOL-Algebra and HOL-Analysis
paulson <lp15@cam.ac.uk>
parents: 70086
diff changeset
   135
  document_files
eca8611201e9 new Homology target, depending on HOL-Algebra and HOL-Analysis
paulson <lp15@cam.ac.uk>
parents: 70086
diff changeset
   136
    "root.tex"
eca8611201e9 new Homology target, depending on HOL-Algebra and HOL-Analysis
paulson <lp15@cam.ac.uk>
parents: 70086
diff changeset
   137
73477
1d8a79aa2a99 dedicated session for combinatorial material
haftmann
parents: 73408
diff changeset
   138
session "HOL-Combinatorics" (main timing) in "Combinatorics" = "HOL" +
1d8a79aa2a99 dedicated session for combinatorial material
haftmann
parents: 73408
diff changeset
   139
  sessions
1d8a79aa2a99 dedicated session for combinatorial material
haftmann
parents: 73408
diff changeset
   140
    "HOL-Library"
1d8a79aa2a99 dedicated session for combinatorial material
haftmann
parents: 73408
diff changeset
   141
  theories
1d8a79aa2a99 dedicated session for combinatorial material
haftmann
parents: 73408
diff changeset
   142
    Combinatorics
1d8a79aa2a99 dedicated session for combinatorial material
haftmann
parents: 73408
diff changeset
   143
  document_files
1d8a79aa2a99 dedicated session for combinatorial material
haftmann
parents: 73408
diff changeset
   144
    "root.tex"
1d8a79aa2a99 dedicated session for combinatorial material
haftmann
parents: 73408
diff changeset
   145
67100
c7694d51c278 clarified main sessions;
wenzelm
parents: 67019
diff changeset
   146
session "HOL-Computational_Algebra" (main timing) in "Computational_Algebra" = "HOL-Library" +
65417
fc41a5650fb1 session containing computational algebra
haftmann
parents: 65416
diff changeset
   147
  theories
fc41a5650fb1 session containing computational algebra
haftmann
parents: 65416
diff changeset
   148
    Computational_Algebra
fc41a5650fb1 session containing computational algebra
haftmann
parents: 65416
diff changeset
   149
    (*conflicting type class instantiations and dependent applications*)
fc41a5650fb1 session containing computational algebra
haftmann
parents: 65416
diff changeset
   150
    Field_as_Ring
80061
4c1347e172b1 moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
Manuel Eberl <eberlm@in.tum.de>
parents: 78890
diff changeset
   151
  document_files
4c1347e172b1 moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
Manuel Eberl <eberlm@in.tum.de>
parents: 78890
diff changeset
   152
    "root.tex"
4c1347e172b1 moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
Manuel Eberl <eberlm@in.tum.de>
parents: 78890
diff changeset
   153
    "root.bib"
65417
fc41a5650fb1 session containing computational algebra
haftmann
parents: 65416
diff changeset
   154
68630
c55f6f0b3854 Added Real_Asymp package
Manuel Eberl <eberlm@in.tum.de>
parents: 68617
diff changeset
   155
session "HOL-Real_Asymp" in Real_Asymp = HOL +
c55f6f0b3854 Added Real_Asymp package
Manuel Eberl <eberlm@in.tum.de>
parents: 68617
diff changeset
   156
  sessions
c55f6f0b3854 Added Real_Asymp package
Manuel Eberl <eberlm@in.tum.de>
parents: 68617
diff changeset
   157
    "HOL-Decision_Procs"
c55f6f0b3854 Added Real_Asymp package
Manuel Eberl <eberlm@in.tum.de>
parents: 68617
diff changeset
   158
  theories
c55f6f0b3854 Added Real_Asymp package
Manuel Eberl <eberlm@in.tum.de>
parents: 68617
diff changeset
   159
    Real_Asymp
c55f6f0b3854 Added Real_Asymp package
Manuel Eberl <eberlm@in.tum.de>
parents: 68617
diff changeset
   160
    Real_Asymp_Approx
68677
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents: 68649
diff changeset
   161
    Real_Asymp_Examples
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents: 68649
diff changeset
   162
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents: 68649
diff changeset
   163
session "HOL-Real_Asymp-Manual" in "Real_Asymp/Manual" = "HOL-Real_Asymp" +
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents: 68649
diff changeset
   164
  theories
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents: 68649
diff changeset
   165
    Real_Asymp_Doc
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents: 68649
diff changeset
   166
  document_files (in "~~/src/Doc")
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents: 68649
diff changeset
   167
    "iman.sty"
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents: 68649
diff changeset
   168
    "extra.sty"
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents: 68649
diff changeset
   169
    "isar.sty"
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents: 68649
diff changeset
   170
  document_files
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents: 68649
diff changeset
   171
    "root.tex"
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents: 68649
diff changeset
   172
    "style.sty"
68630
c55f6f0b3854 Added Real_Asymp package
Manuel Eberl <eberlm@in.tum.de>
parents: 68617
diff changeset
   173
71832
f61b19358a8f clarified session imports: avoid bulky HOL-Library image;
wenzelm
parents: 71814
diff changeset
   174
session "HOL-Hahn_Banach" in Hahn_Banach = HOL +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   175
  description "
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   176
    Author:     Gertrud Bauer, TU Munich
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   177
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   178
    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
   179
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   180
    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
   181
    following H. Heuser, Funktionalanalysis, p. 228 -232. The Hahn-Banach
55018
2a526bd279ed moved 'Zorn' into 'Main', since it's a BNF dependency
blanchet
parents: 54961
diff changeset
   182
    theorem is one of the fundamental theorems of functional analysis. It is a
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   183
    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
   184
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   185
    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
   186
    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
   187
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   188
    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
   189
    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
   190
    continous linearform on the whole vectorspace.
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   191
  "
65573
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   192
  sessions
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   193
    "HOL-Analysis"
65543
8369b33fda0a clarified session imports;
wenzelm
parents: 65538
diff changeset
   194
  theories
8369b33fda0a clarified session imports;
wenzelm
parents: 65538
diff changeset
   195
    Hahn_Banach
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   196
  document_files "root.bib" "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   197
71832
f61b19358a8f clarified session imports: avoid bulky HOL-Library image;
wenzelm
parents: 71814
diff changeset
   198
session "HOL-Induct" in Induct = HOL +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   199
  description "
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   200
    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
   201
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   202
    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
   203
    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
   204
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   205
    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
   206
    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
   207
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   208
    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
   209
    (see
58372
bfd497f2f4c2 moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer)
blanchet
parents: 58371
diff changeset
   210
    http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz).
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   211
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   212
    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
   213
    mutually recursive relations.
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   214
  "
71832
f61b19358a8f clarified session imports: avoid bulky HOL-Library image;
wenzelm
parents: 71814
diff changeset
   215
  sessions
f61b19358a8f clarified session imports: avoid bulky HOL-Library image;
wenzelm
parents: 71814
diff changeset
   216
    "HOL-Library"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   217
  theories [quick_and_dirty]
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   218
    Common_Patterns
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   219
  theories
61935
6512e84cc9f5 clarified sessions;
wenzelm
parents: 61793
diff changeset
   220
    Nested_Datatype
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   221
    QuoDataType
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   222
    QuoNestedDataType
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   223
    Term
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   224
    SList
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   225
    ABexp
65562
f9753d949afc renamed theory to avoid conflict with loaded theory "Tree" from HOL-Library;
wenzelm
parents: 65552
diff changeset
   226
    Infinitely_Branching_Tree
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   227
    Ordinals
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   228
    Sigma_Algebra
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   229
    Comb
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   230
    PropLog
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   231
    Com
77036
d0151eb9ecb0 more correct and complete bibliography;
wenzelm
parents: 77003
diff changeset
   232
  document_files
d0151eb9ecb0 more correct and complete bibliography;
wenzelm
parents: 77003
diff changeset
   233
    "root.bib"
d0151eb9ecb0 more correct and complete bibliography;
wenzelm
parents: 77003
diff changeset
   234
    "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   235
65573
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   236
session "HOL-IMP" (timing) in IMP = "HOL-Library" +
59446
4427f04fca57 discontinued obsolete option "document_graph";
wenzelm
parents: 59190
diff changeset
   237
  options [document_variants = document]
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   238
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   239
    BExp
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   240
    ASM
50050
fac2b27893ff new theory IMP/Finite_Reachable
nipkow
parents: 50023
diff changeset
   241
    Finite_Reachable
52394
fe33d456b36c more canonical name (2)
nipkow
parents: 52363
diff changeset
   242
    Denotational
52400
ded7b9c60dc2 tuned theory name
nipkow
parents: 52394
diff changeset
   243
    Compiler2
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   244
    Poly_Types
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   245
    Sec_Typing
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   246
    Sec_TypingT
52726
ee0bd6bababd merged Def_Init_Sound_X into Def_Init_X
nipkow
parents: 52722
diff changeset
   247
    Def_Init_Big
ee0bd6bababd merged Def_Init_Sound_X into Def_Init_X
nipkow
parents: 52722
diff changeset
   248
    Def_Init_Small
ee0bd6bababd merged Def_Init_Sound_X into Def_Init_X
nipkow
parents: 52722
diff changeset
   249
    Fold
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   250
    Live
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   251
    Live_True
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   252
    Hoare_Examples
63538
d7b5e2a222c2 added new vcg based on existentially quantified while-rule
nipkow
parents: 63537
diff changeset
   253
    Hoare_Sound_Complete
52269
d867812da48b more VC -> VCG
nipkow
parents: 52248
diff changeset
   254
    VCG
52282
c79a3e15779e tuned theory name
nipkow
parents: 52277
diff changeset
   255
    Hoare_Total
63538
d7b5e2a222c2 added new vcg based on existentially quantified while-rule
nipkow
parents: 63537
diff changeset
   256
    VCG_Total_EX
67019
7a3724078363 Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents: 66992
diff changeset
   257
    VCG_Total_EX2
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   258
    Collecting1
48765
fb1ed5230abc special code with lists no longer necessary, use sets
nipkow
parents: 48738
diff changeset
   259
    Collecting_Examples
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   260
    Abs_Int_Tests
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   261
    Abs_Int1_parity
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   262
    Abs_Int1_const
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   263
    Abs_Int3
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   264
    Procs_Dyn_Vars_Dyn
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   265
    Procs_Stat_Vars_Dyn
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   266
    Procs_Stat_Vars_Stat
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   267
    C_like
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   268
    OO
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   269
  document_files "root.bib" "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   270
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   271
session "HOL-IMPP" in IMPP = HOL +
69272
15e9ed5b28fb isabelle update_cartouches -t;
wenzelm
parents: 69252
diff changeset
   272
  description \<open>
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   273
    Author:     David von Oheimb
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   274
    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
   275
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   276
    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
   277
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   278
    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
   279
    procedures. For documentation see "Hoare Logic for Mutual Recursion and
68649
f849fc1cb65e prefer HTTPS;
wenzelm
parents: 68640
diff changeset
   280
    Local Variables" (https://isabelle.in.tum.de/Bali/papers/FSTTCS99.html).
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   281
  \<close>
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   282
  theories EvenOdd
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   283
63888
5a9a1985e9fb sessions that are relevant for routine timing measurements;
wenzelm
parents: 63885
diff changeset
   284
session "HOL-Data_Structures" (timing) in Data_Structures = HOL +
61203
a8a8eca85801 New subdirectory for functional data structures
nipkow
parents: 61152
diff changeset
   285
  options [document_variants = document]
65573
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   286
  sessions
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   287
    "HOL-Number_Theory"
61203
a8a8eca85801 New subdirectory for functional data structures
nipkow
parents: 61152
diff changeset
   288
  theories [document = false]
65538
a39ef48fbee0 tuned imports;
wenzelm
parents: 65535
diff changeset
   289
    Less_False
61203
a8a8eca85801 New subdirectory for functional data structures
nipkow
parents: 61152
diff changeset
   290
  theories
66543
a90dbf19f573 new file
nipkow
parents: 66453
diff changeset
   291
    Sorting
63829
6a05c8cbf7de More on balancing; renamed theory to Balance
nipkow
parents: 63827
diff changeset
   292
    Balance
61203
a8a8eca85801 New subdirectory for functional data structures
nipkow
parents: 61152
diff changeset
   293
    Tree_Map
77573
237e5504bae7 new theory Tree_Rotations
nipkow
parents: 77036
diff changeset
   294
    Tree_Rotations
71414
c26de1bd7b00 added Interval_Tree.thy
nipkow
parents: 71393
diff changeset
   295
    Interval_Tree
61232
c46faf9762f7 added AVL and lookup function
nipkow
parents: 61224
diff changeset
   296
    AVL_Map
71814
a9df6686ed0e AVL trees with balance tags
nipkow
parents: 71801
diff changeset
   297
    AVL_Bal_Set
71844
57ace76cbffa another AVL tree version
nipkow
parents: 71836
diff changeset
   298
    AVL_Bal2_Set
71801
49d8d8ad7e43 added Height_Balanced_Trees
nipkow
parents: 71766
diff changeset
   299
    Height_Balanced_Tree
71352
41f3ca717da5 alternative deletion in Red-Black trees
nipkow
parents: 71263
diff changeset
   300
    RBT_Set2
61224
759b5299a9f2 added red black trees
nipkow
parents: 61203
diff changeset
   301
    RBT_Map
61469
cd82b1023932 added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents: 61368
diff changeset
   302
    Tree23_Map
72099
f978ecaf119a added theory Tree23_of_List
nipkow
parents: 72056
diff changeset
   303
    Tree23_of_List
61514
213556e498c2 added 234-Trees (slow)
nipkow
parents: 61469
diff changeset
   304
    Tree234_Map
61789
9ce1a397410a added Brother12_Map
nipkow
parents: 61784
diff changeset
   305
    Brother12_Map
62130
90a3016a6c12 added AA_Map; tuned titles
nipkow
parents: 62008
diff changeset
   306
    AA_Map
68261
035c78bb0a66 reorganization, everything based on Tree2 now
nipkow
parents: 68155
diff changeset
   307
    Set2_Join_RBT
69145
806be481aa57 added Array files
nipkow
parents: 69133
diff changeset
   308
    Array_Braun
70250
20d819b0a29d New version of tries
nipkow
parents: 70174
diff changeset
   309
    Trie_Fun
20d819b0a29d New version of tries
nipkow
parents: 70174
diff changeset
   310
    Trie_Map
20d819b0a29d New version of tries
nipkow
parents: 70174
diff changeset
   311
    Tries_Binary
72389
3d255ebe9733 Aded Queues
nipkow
parents: 72331
diff changeset
   312
    Queue_2Lists
72688
8cb82e7f1743 proper defn of a heap
nipkow
parents: 72621
diff changeset
   313
    Heaps
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62696
diff changeset
   314
    Leftist_Heap
78231
3e8d443b9512 New theory Leftist_Heap_List
nipkow
parents: 77573
diff changeset
   315
    Leftist_Heap_List
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents: 66270
diff changeset
   316
    Binomial_Heap
73108
981a383610df HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents: 72993
diff changeset
   317
    Selection
61224
759b5299a9f2 added red black trees
nipkow
parents: 61203
diff changeset
   318
  document_files "root.tex" "root.bib"
61203
a8a8eca85801 New subdirectory for functional data structures
nipkow
parents: 61152
diff changeset
   319
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   320
session "HOL-Import" in Import = HOL +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   321
  theories HOL_Light_Maps
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   322
  theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   323
67100
c7694d51c278 clarified main sessions;
wenzelm
parents: 67019
diff changeset
   324
session "HOL-Number_Theory" (main timing) in Number_Theory = "HOL-Computational_Algebra" +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   325
  description "
55321
eadea363deb6 Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents: 55240
diff changeset
   326
    Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler
55730
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents: 55663
diff changeset
   327
    Theorem, Wilson's Theorem, some lemmas for Quadratic Reciprocity.
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   328
  "
65543
8369b33fda0a clarified session imports;
wenzelm
parents: 65538
diff changeset
   329
  sessions
8369b33fda0a clarified session imports;
wenzelm
parents: 65538
diff changeset
   330
    "HOL-Algebra"
55321
eadea363deb6 Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents: 55240
diff changeset
   331
  theories
eadea363deb6 Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents: 55240
diff changeset
   332
    Number_Theory
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   333
  document_files
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   334
    "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   335
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   336
session "HOL-Hoare" in Hoare = HOL +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   337
  description "
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   338
    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
   339
    automatically from pre/post conditions and loop invariants).
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   340
  "
75916
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents: 75647
diff changeset
   341
  theories [document = false]
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents: 75647
diff changeset
   342
    README
72986
d231d71d27b4 clarified session: avoid merge of different syntax from different Hoare logics;
wenzelm
parents: 72985
diff changeset
   343
  theories
d231d71d27b4 clarified session: avoid merge of different syntax from different Hoare logics;
wenzelm
parents: 72985
diff changeset
   344
    Examples
d231d71d27b4 clarified session: avoid merge of different syntax from different Hoare logics;
wenzelm
parents: 72985
diff changeset
   345
    ExamplesAbort
d231d71d27b4 clarified session: avoid merge of different syntax from different Hoare logics;
wenzelm
parents: 72985
diff changeset
   346
    ExamplesTC
d231d71d27b4 clarified session: avoid merge of different syntax from different Hoare logics;
wenzelm
parents: 72985
diff changeset
   347
    Pointers0
d231d71d27b4 clarified session: avoid merge of different syntax from different Hoare logics;
wenzelm
parents: 72985
diff changeset
   348
    Pointer_Examples
d231d71d27b4 clarified session: avoid merge of different syntax from different Hoare logics;
wenzelm
parents: 72985
diff changeset
   349
    Pointer_ExamplesAbort
d231d71d27b4 clarified session: avoid merge of different syntax from different Hoare logics;
wenzelm
parents: 72985
diff changeset
   350
    SchorrWaite
d231d71d27b4 clarified session: avoid merge of different syntax from different Hoare logics;
wenzelm
parents: 72985
diff changeset
   351
    Separation
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   352
  document_files "root.bib" "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   353
63888
5a9a1985e9fb sessions that are relevant for routine timing measurements;
wenzelm
parents: 63885
diff changeset
   354
session "HOL-Hoare_Parallel" (timing) in Hoare_Parallel = HOL +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   355
  description "
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   356
    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
   357
    (verification conditions are generated automatically).
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   358
  "
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   359
  theories Hoare_Parallel
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   360
  document_files "root.bib" "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   361
72312
0134a7d6ad56 less bulky session stack;
wenzelm
parents: 72262
diff changeset
   362
session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" +
65573
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   363
  sessions
72312
0134a7d6ad56 less bulky session stack;
wenzelm
parents: 72262
diff changeset
   364
    "HOL-Number_Theory"
65573
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   365
    "HOL-Data_Structures"
72056
b9f5f30b623f proper session imports;
wenzelm
parents: 72049
diff changeset
   366
    "HOL-Examples"
51422
821a70e29e0b proper formatting, to facilitate line-based diff;
wenzelm
parents: 51421
diff changeset
   367
  theories
821a70e29e0b proper formatting, to facilitate line-based diff;
wenzelm
parents: 51421
diff changeset
   368
    Generate
821a70e29e0b proper formatting, to facilitate line-based diff;
wenzelm
parents: 51421
diff changeset
   369
    Generate_Binary_Nat
821a70e29e0b proper formatting, to facilitate line-based diff;
wenzelm
parents: 51421
diff changeset
   370
    Generate_Target_Nat
75647
34cd1d210b92 officical abstract characters for code generation
haftmann
parents: 75329
diff changeset
   371
    Generate_Abstract_Char
51422
821a70e29e0b proper formatting, to facilitate line-based diff;
wenzelm
parents: 51421
diff changeset
   372
    Generate_Efficient_Datastructures
68155
8b50f29a1992 new tool Code_Lazy
Andreas Lochbihler
parents: 68133
diff changeset
   373
    Code_Lazy_Test
64582
3d20ded18f14 unconditional Code_Test_PolyML and Code_Test_Scala: compiler is always present;
wenzelm
parents: 64569
diff changeset
   374
    Code_Test_PolyML
3d20ded18f14 unconditional Code_Test_PolyML and Code_Test_Scala: compiler is always present;
wenzelm
parents: 64569
diff changeset
   375
    Code_Test_Scala
66842
wenzelm
parents: 66805
diff changeset
   376
  theories [condition = ISABELLE_GHC]
58039
469a375212c1 add testing framework for generated code
Andreas Lochbihler
parents: 58023
diff changeset
   377
    Code_Test_GHC
66842
wenzelm
parents: 66805
diff changeset
   378
  theories [condition = ISABELLE_MLTON]
58039
469a375212c1 add testing framework for generated code
Andreas Lochbihler
parents: 58023
diff changeset
   379
    Code_Test_MLton
69926
110fff287217 access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents: 69716
diff changeset
   380
  theories [condition = ISABELLE_OCAMLFIND]
58039
469a375212c1 add testing framework for generated code
Andreas Lochbihler
parents: 58023
diff changeset
   381
    Code_Test_OCaml
66842
wenzelm
parents: 66805
diff changeset
   382
  theories [condition = ISABELLE_SMLNJ]
58039
469a375212c1 add testing framework for generated code
Andreas Lochbihler
parents: 58023
diff changeset
   383
    Code_Test_SMLNJ
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   384
65573
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   385
session "HOL-Metis_Examples" (timing) in Metis_Examples = "HOL-Library" +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   386
  description "
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   387
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   388
    Author:     Jasmin Blanchette, TU Muenchen
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   389
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   390
    Testing Metis and Sledgehammer.
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   391
  "
65573
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   392
  sessions
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   393
    "HOL-Decision_Procs"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   394
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   395
    Abstraction
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   396
    Big_O
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   397
    Binary_Tree
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   398
    Clausification
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   399
    Message
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   400
    Proxies
78676
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents: 78478
diff changeset
   401
    Sets
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents: 78478
diff changeset
   402
    Sledgehammer_Isar_Proofs
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   403
    Tarski
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   404
    Trans_Closure
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   405
72189
7a213affdc10 clarified session: no parent image for minor theory imports;
wenzelm
parents: 72102
diff changeset
   406
session "HOL-Nitpick_Examples" in Nitpick_Examples = HOL +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   407
  description "
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   408
    Author:     Jasmin Blanchette, TU Muenchen
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   409
    Copyright   2009
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   410
  "
72993
6ead333e450d more robust defaults: spurious problems with parallel invocations and interrupts;
wenzelm
parents: 72986
diff changeset
   411
  options [kodkod_scala]
72189
7a213affdc10 clarified session: no parent image for minor theory imports;
wenzelm
parents: 72102
diff changeset
   412
  sessions "HOL-Library"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   413
  theories [quick_and_dirty] Nitpick_Examples
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   414
65550
e957b1f00449 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65549
diff changeset
   415
session "HOL-Algebra" (main timing) in Algebra = "HOL-Computational_Algebra" +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   416
  description "
68569
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents: 68522
diff changeset
   417
    Author: Clemens Ballarin, started 24 September 1999, and many others
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   418
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   419
    The Isabelle Algebraic Library.
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   420
  "
70660
373d95cf1b98 proper session-qualifier imports (amending "fixes" from adaa0a6ea4fe);
wenzelm
parents: 70646
diff changeset
   421
  sessions
373d95cf1b98 proper session-qualifier imports (amending "fixes" from adaa0a6ea4fe);
wenzelm
parents: 70646
diff changeset
   422
    "HOL-Cardinals"
73477
1d8a79aa2a99 dedicated session for combinatorial material
haftmann
parents: 73408
diff changeset
   423
    "HOL-Combinatorics"
75916
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents: 75647
diff changeset
   424
  theories [document = false]
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents: 75647
diff changeset
   425
    README
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   426
  theories
65099
30d0b2f1df76 Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents: 65050
diff changeset
   427
    (* Orders and Lattices *)
30d0b2f1df76 Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents: 65050
diff changeset
   428
    Galois_Connection    (* Knaster-Tarski theorem and Galois connections *)
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   429
    (* Groups *)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   430
    FiniteProduct        (* Product operator for commutative groups *)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   431
    Sylow                (* Sylow's theorem *)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   432
    Bij                  (* Automorphism Groups *)
65416
f707dbcf11e3 more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents: 65382
diff changeset
   433
    Multiplicative_Group
68443
43055b016688 New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents: 68312
diff changeset
   434
    Zassenhaus            (* The Zassenhaus lemma *)
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   435
    (* Rings *)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   436
    Divisibility         (* Rings *)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   437
    IntRing              (* Ideals and residue classes *)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   438
    UnivPoly             (* Polynomials *)
68569
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents: 68522
diff changeset
   439
    (* Main theory *)
70078
3a1b2d8c89aa bundle for cardinal syntax
traytel
parents: 70026
diff changeset
   440
    Algebra
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   441
  document_files "root.bib" "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   442
71832
f61b19358a8f clarified session imports: avoid bulky HOL-Library image;
wenzelm
parents: 71814
diff changeset
   443
session "HOL-Auth" (timing) in Auth = HOL +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   444
  description "
51421
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   445
    A new approach to verifying authentication protocols.
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   446
  "
71832
f61b19358a8f clarified session imports: avoid bulky HOL-Library image;
wenzelm
parents: 71814
diff changeset
   447
  sessions "HOL-Library"
70675
efd995488228 declare session directories;
wenzelm
parents: 70669
diff changeset
   448
  directories "Smartcard" "Guard"
75916
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents: 75647
diff changeset
   449
  theories [document = false]
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents: 75647
diff changeset
   450
    README
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   451
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   452
    Auth_Shared
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   453
    Auth_Public
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   454
    "Smartcard/Auth_Smartcard"
75916
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents: 75647
diff changeset
   455
  theories [document = false]
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents: 75647
diff changeset
   456
    "Guard/README_Guard"
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents: 75647
diff changeset
   457
  theories
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   458
    "Guard/Auth_Guard_Shared"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   459
    "Guard/Auth_Guard_Public"
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   460
  document_files "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   461
63888
5a9a1985e9fb sessions that are relevant for routine timing measurements;
wenzelm
parents: 63885
diff changeset
   462
session "HOL-UNITY" (timing) in UNITY = "HOL-Auth" +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   463
  description "
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   464
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   465
    Copyright   1998  University of Cambridge
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   466
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   467
    Verifying security protocols using Chandy and Misra's UNITY formalism.
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   468
  "
70675
efd995488228 declare session directories;
wenzelm
parents: 70669
diff changeset
   469
  directories "Simple" "Comp"
75916
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents: 75647
diff changeset
   470
  theories [document = false]
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents: 75647
diff changeset
   471
    README
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   472
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   473
    (*Basic meta-theory*)
65538
a39ef48fbee0 tuned imports;
wenzelm
parents: 65535
diff changeset
   474
    UNITY_Main
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   475
75916
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents: 75647
diff changeset
   476
  theories [document = false]
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents: 75647
diff changeset
   477
    "Simple/README_Simple"
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents: 75647
diff changeset
   478
  theories
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   479
    (*Simple examples: no composition*)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   480
    "Simple/Deadlock"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   481
    "Simple/Common"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   482
    "Simple/Network"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   483
    "Simple/Token"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   484
    "Simple/Channel"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   485
    "Simple/Lift"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   486
    "Simple/Mutex"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   487
    "Simple/Reach"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   488
    "Simple/Reachability"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   489
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   490
    (*Verifying security protocols using UNITY*)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   491
    "Simple/NSP_Bad"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   492
75916
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents: 75647
diff changeset
   493
  theories [document = false]
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents: 75647
diff changeset
   494
    "Comp/README_Comp"
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents: 75647
diff changeset
   495
  theories
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   496
    (*Example of composition*)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   497
    "Comp/Handshake"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   498
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   499
    (*Universal properties examples*)
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   500
    "Comp/Counter"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   501
    "Comp/Counterc"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   502
    "Comp/Priority"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   503
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   504
    "Comp/TimerArray"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   505
    "Comp/Progress"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   506
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   507
    "Comp/Alloc"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   508
    "Comp/AllocImpl"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   509
    "Comp/Client"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   510
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   511
    (*obsolete*)
65538
a39ef48fbee0 tuned imports;
wenzelm
parents: 65535
diff changeset
   512
    ELT
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   513
  document_files "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   514
71832
f61b19358a8f clarified session imports: avoid bulky HOL-Library image;
wenzelm
parents: 71814
diff changeset
   515
session "HOL-Unix" in Unix = HOL +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   516
  options [print_mode = "no_brackets,no_type_brackets"]
71832
f61b19358a8f clarified session imports: avoid bulky HOL-Library image;
wenzelm
parents: 71814
diff changeset
   517
  sessions "HOL-Library"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   518
  theories Unix
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   519
  document_files "root.bib" "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   520
71832
f61b19358a8f clarified session imports: avoid bulky HOL-Library image;
wenzelm
parents: 71814
diff changeset
   521
session "HOL-ZF" in ZF = HOL +
f61b19358a8f clarified session imports: avoid bulky HOL-Library image;
wenzelm
parents: 71814
diff changeset
   522
  sessions "HOL-Library"
65573
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   523
  theories
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   524
    MainZF
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   525
    Games
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   526
  document_files "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   527
71832
f61b19358a8f clarified session imports: avoid bulky HOL-Library image;
wenzelm
parents: 71814
diff changeset
   528
session "HOL-Imperative_HOL" (timing) in Imperative_HOL = HOL +
70678
36c8c32346cb clarified syntax: 'directories' and 'theories' belong together;
wenzelm
parents: 70675
diff changeset
   529
  options [print_mode = "iff,no_brackets"]
71832
f61b19358a8f clarified session imports: avoid bulky HOL-Library image;
wenzelm
parents: 71814
diff changeset
   530
  sessions "HOL-Library"
70675
efd995488228 declare session directories;
wenzelm
parents: 70669
diff changeset
   531
  directories "ex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   532
  theories Imperative_HOL_ex
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   533
  document_files "root.bib" "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   534
65550
e957b1f00449 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65549
diff changeset
   535
session "HOL-Decision_Procs" (timing) in Decision_Procs = "HOL-Algebra" +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   536
  description "
51544
8c58fbbc1d5a tuned session specification;
wenzelm
parents: 51517
diff changeset
   537
    Various decision procedures, typically involving reflection.
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   538
  "
70675
efd995488228 declare session directories;
wenzelm
parents: 70669
diff changeset
   539
  directories "ex"
65543
8369b33fda0a clarified session imports;
wenzelm
parents: 65538
diff changeset
   540
  theories
8369b33fda0a clarified session imports;
wenzelm
parents: 65538
diff changeset
   541
    Decision_Procs
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   542
63000
d0dfdd413a7f remove "slow" session tags
Lars Hupel <lars.hupel@mytum.de>
parents: 62999
diff changeset
   543
session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
65573
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   544
  sessions
72049
18d35be9493f proper import sessions;
wenzelm
parents: 72029
diff changeset
   545
    "HOL-Examples"
52424
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents: 52400
diff changeset
   546
  theories
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents: 52400
diff changeset
   547
    Hilbert_Classical
62363
7b5468422352 moved examples to avoid dependency on bulky HOL-Proofs session, e.g. relevant for "isabelle makedist";
wenzelm
parents: 62357
diff changeset
   548
    Proof_Terms
52424
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents: 52400
diff changeset
   549
    XML_Data
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   550
63888
5a9a1985e9fb sessions that are relevant for routine timing measurements;
wenzelm
parents: 63885
diff changeset
   551
session "HOL-Proofs-Extraction" (timing) in "Proofs/Extraction" = "HOL-Proofs" +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   552
  description "
51421
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   553
    Examples for program extraction in Higher-Order Logic.
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   554
  "
70398
725438ceae7c proof terms are always constructed sequentially;
wenzelm
parents: 70250
diff changeset
   555
  options [quick_and_dirty = false]
65543
8369b33fda0a clarified session imports;
wenzelm
parents: 65538
diff changeset
   556
  sessions
8369b33fda0a clarified session imports;
wenzelm
parents: 65538
diff changeset
   557
    "HOL-Computational_Algebra"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   558
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   559
    Greatest_Common_Divisor
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   560
    Warshall
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   561
    Higman_Extraction
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   562
    Pigeonhole
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   563
    Euclid
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   564
  document_files "root.bib" "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   565
63888
5a9a1985e9fb sessions that are relevant for routine timing measurements;
wenzelm
parents: 63885
diff changeset
   566
session "HOL-Proofs-Lambda" (timing) in "Proofs/Lambda" = "HOL-Proofs" +
69272
15e9ed5b28fb isabelle update_cartouches -t;
wenzelm
parents: 69252
diff changeset
   567
  description \<open>
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   568
    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
   569
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   570
    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
   571
    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
   572
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   573
    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
   574
    theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html).
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   575
  \<close>
70398
725438ceae7c proof terms are always constructed sequentially;
wenzelm
parents: 70250
diff changeset
   576
  options [print_mode = "no_brackets", quick_and_dirty = false]
65543
8369b33fda0a clarified session imports;
wenzelm
parents: 65538
diff changeset
   577
  sessions
8369b33fda0a clarified session imports;
wenzelm
parents: 65538
diff changeset
   578
    "HOL-Library"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   579
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   580
    Eta
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   581
    StrongNorm
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   582
    Standardization
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   583
    WeakNorm
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   584
  document_files "root.bib" "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   585
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   586
session "HOL-Prolog" in Prolog = HOL +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   587
  description "
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   588
    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
   589
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   590
    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
   591
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   592
    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
   593
    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
   594
    a little functional language and its type system.
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   595
  "
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   596
  theories Test Type
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   597
71832
f61b19358a8f clarified session imports: avoid bulky HOL-Library image;
wenzelm
parents: 71814
diff changeset
   598
session "HOL-MicroJava" (timing) in MicroJava = HOL +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   599
  description "
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   600
    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
   601
    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
   602
    bytecode verifier, including proofs of type-safety.
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   603
  "
65573
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   604
  sessions
71832
f61b19358a8f clarified session imports: avoid bulky HOL-Library image;
wenzelm
parents: 71814
diff changeset
   605
    "HOL-Library"
65573
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   606
    "HOL-Eisbach"
70678
36c8c32346cb clarified syntax: 'directories' and 'theories' belong together;
wenzelm
parents: 70675
diff changeset
   607
  directories "BV" "Comp" "DFA" "J" "JVM"
59446
4427f04fca57 discontinued obsolete option "document_graph";
wenzelm
parents: 59190
diff changeset
   608
  theories
4427f04fca57 discontinued obsolete option "document_graph";
wenzelm
parents: 59190
diff changeset
   609
    MicroJava
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   610
  document_files
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   611
    "introduction.tex"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   612
    "root.bib"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   613
    "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   614
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   615
session "HOL-NanoJava" in NanoJava = HOL +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   616
  description "
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   617
    Hoare Logic for a tiny fragment of Java.
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   618
  "
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   619
  theories Example
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   620
  document_files "root.bib" "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   621
71832
f61b19358a8f clarified session imports: avoid bulky HOL-Library image;
wenzelm
parents: 71814
diff changeset
   622
session "HOL-Bali" (timing) in Bali = HOL +
f61b19358a8f clarified session imports: avoid bulky HOL-Library image;
wenzelm
parents: 71814
diff changeset
   623
  sessions
f61b19358a8f clarified session imports: avoid bulky HOL-Library image;
wenzelm
parents: 71814
diff changeset
   624
    "HOL-Library"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   625
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   626
    AxExample
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   627
    AxSound
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   628
    AxCompl
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   629
    Trans
60751
83f04804696c reactivated dead code;
wenzelm
parents: 60603
diff changeset
   630
    TypeSafe
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   631
  document_files "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   632
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   633
session "HOL-IOA" in IOA = HOL +
69272
15e9ed5b28fb isabelle update_cartouches -t;
wenzelm
parents: 69252
diff changeset
   634
  description \<open>
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   635
    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
   636
    Copyright   1994--1996  TU Muenchen
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   637
55417
01fbfb60c33e adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents: 55370
diff changeset
   638
    The meta-theory of I/O-Automata in HOL. This formalization has been
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   639
    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
   640
    proofs of two communication protocols which formerly have been here.
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   641
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   642
    @inproceedings{Nipkow-Slind-IOA,
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   643
    author={Tobias Nipkow and Konrad Slind},
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   644
    title={{I/O} Automata in {Isabelle/HOL}},
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   645
    booktitle={Proc.\ TYPES Workshop 1994},
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   646
    publisher=Springer,
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   647
    series=LNCS,
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   648
    note={To appear}}
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   649
    ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   650
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   651
    and
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   652
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   653
    @inproceedings{Mueller-Nipkow,
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   654
    author={Olaf M\"uller and Tobias Nipkow},
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   655
    title={Combining Model Checking and Deduction for {I/O}-Automata},
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   656
    booktitle={Proc.\ TACAS Workshop},
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   657
    organization={Aarhus University, BRICS report},
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   658
    year=1995}
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   659
    ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   660
  \<close>
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   661
  theories Solve
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   662
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   663
session "HOL-Lattice" in Lattice = HOL +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   664
  description "
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   665
    Author:     Markus Wenzel, TU Muenchen
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   666
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   667
    Basic theory of lattices and orders.
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   668
  "
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   669
  theories CompleteLattice
77036
d0151eb9ecb0 more correct and complete bibliography;
wenzelm
parents: 77003
diff changeset
   670
  document_files
d0151eb9ecb0 more correct and complete bibliography;
wenzelm
parents: 77003
diff changeset
   671
    "root.bib"
d0151eb9ecb0 more correct and complete bibliography;
wenzelm
parents: 77003
diff changeset
   672
    "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   673
66752
1dd5633f5862 clarified imports: prefer parent session images;
wenzelm
parents: 66751
diff changeset
   674
session "HOL-ex" (timing) in ex = "HOL-Number_Theory" +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   675
  description "
74286
641300b56ebe tuned comments;
wenzelm
parents: 74193
diff changeset
   676
    Miscellaneous examples and experiments for Isabelle/HOL.
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   677
  "
77036
d0151eb9ecb0 more correct and complete bibliography;
wenzelm
parents: 77003
diff changeset
   678
  options [document = false]
65548
b7caa2b8bdbf removed pointless document;
wenzelm
parents: 65544
diff changeset
   679
  theories
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   680
    Antiquote
65549
wenzelm
parents: 65548
diff changeset
   681
    Argo_Examples
wenzelm
parents: 65548
diff changeset
   682
    Arith_Examples
wenzelm
parents: 65548
diff changeset
   683
    Ballot
77003
ab905b5bb206 HOL/Library/BigO is obsolete
paulson <lp15@cam.ac.uk>
parents: 75974
diff changeset
   684
    BigO
65549
wenzelm
parents: 65548
diff changeset
   685
    BinEx
wenzelm
parents: 65548
diff changeset
   686
    Birthday_Paradox
wenzelm
parents: 65548
diff changeset
   687
    Bubblesort
wenzelm
parents: 65548
diff changeset
   688
    CTL
wenzelm
parents: 65548
diff changeset
   689
    Cartouche_Examples
65563
e83c9e94e891 actually use theory;
wenzelm
parents: 65562
diff changeset
   690
    Case_Product
65549
wenzelm
parents: 65548
diff changeset
   691
    Chinese
wenzelm
parents: 65548
diff changeset
   692
    Classical
wenzelm
parents: 65548
diff changeset
   693
    Code_Binary_Nat_examples
68639
357fca99a65a more examples for Code_Lazy
Andreas Lochbihler
parents: 68617
diff changeset
   694
    Code_Lazy_Demo
65549
wenzelm
parents: 65548
diff changeset
   695
    Code_Timing
wenzelm
parents: 65548
diff changeset
   696
    Coercion_Examples
wenzelm
parents: 65548
diff changeset
   697
    Computations
67224
341fbce5b26d a conditional paramitrecity prover
traytel
parents: 67215
diff changeset
   698
    Conditional_Parametricity_Examples
59190
3a594fd13ca4 3 old example lemmas by Amine listed in the top 100 theorems
kleing
parents: 59162
diff changeset
   699
    Cubic_Quartic
67611
7929240e44d4 records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents: 67319
diff changeset
   700
    Datatype_Record_Examples
65549
wenzelm
parents: 65548
diff changeset
   701
    Erdoes_Szekeres
wenzelm
parents: 65548
diff changeset
   702
    Eval_Examples
wenzelm
parents: 65548
diff changeset
   703
    Executable_Relation
wenzelm
parents: 65548
diff changeset
   704
    Execute_Choice
66797
9c9baae29217 removed mere toy example from library
haftmann
parents: 66779
diff changeset
   705
    Function_Growth
65549
wenzelm
parents: 65548
diff changeset
   706
    Gauge_Integration
wenzelm
parents: 65548
diff changeset
   707
    HarmonicSeries
wenzelm
parents: 65548
diff changeset
   708
    Hebrew
wenzelm
parents: 65548
diff changeset
   709
    Hex_Bin_Examples
wenzelm
parents: 65548
diff changeset
   710
    IArray_Examples
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   711
    Intuitionistic
70525
1615b6808192 NEWS and example for Theory.join_theory;
wenzelm
parents: 70398
diff changeset
   712
    Join_Theory
65549
wenzelm
parents: 65548
diff changeset
   713
    Lagrange
wenzelm
parents: 65548
diff changeset
   714
    List_to_Set_Comprehension_Examples
wenzelm
parents: 65548
diff changeset
   715
    LocaleTest2
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   716
    MergeSort
65549
wenzelm
parents: 65548
diff changeset
   717
    MonoidGroup
wenzelm
parents: 65548
diff changeset
   718
    Multiquote
wenzelm
parents: 65548
diff changeset
   719
    NatSum
wenzelm
parents: 65548
diff changeset
   720
    Normalization_by_Evaluation
wenzelm
parents: 65548
diff changeset
   721
    PER
wenzelm
parents: 65548
diff changeset
   722
    Parallel_Example
wenzelm
parents: 65548
diff changeset
   723
    Peano_Axioms
wenzelm
parents: 65548
diff changeset
   724
    Perm_Fragments
wenzelm
parents: 65548
diff changeset
   725
    PresburgerEx
wenzelm
parents: 65548
diff changeset
   726
    Pythagoras
wenzelm
parents: 65548
diff changeset
   727
    Quicksort
67612
e4e57da0583a New theory ex/Radix_Sort.thy
nipkow
parents: 67611
diff changeset
   728
    Radix_Sort
65549
wenzelm
parents: 65548
diff changeset
   729
    Reflection_Examples
wenzelm
parents: 65548
diff changeset
   730
    Refute_Examples
68035
6d7cc6723978 proof of concept for residue rings over int using type numerals
haftmann
parents: 68028
diff changeset
   731
    Residue_Ring
65549
wenzelm
parents: 65548
diff changeset
   732
    SOS
wenzelm
parents: 65548
diff changeset
   733
    SOS_Cert
wenzelm
parents: 65548
diff changeset
   734
    Serbian
wenzelm
parents: 65548
diff changeset
   735
    Set_Comprehension_Pointfree_Examples
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   736
    Set_Theory
65549
wenzelm
parents: 65548
diff changeset
   737
    Simproc_Tests
wenzelm
parents: 65548
diff changeset
   738
    Simps_Case_Conv_Examples
70018
571909ef3103 experimental commands for proof sketching and exploration
haftmann
parents: 69926
diff changeset
   739
    Sketch_and_Explore
69252
fc359b60121c dedicated examples for sorting
haftmann
parents: 69145
diff changeset
   740
    Sorting_Algorithms_Examples
72536
589645894305 bundle mixins for locale and class specifications
haftmann
parents: 72515
diff changeset
   741
    Specifications_with_bundle_mixins
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   742
    Sqrt_Script
65549
wenzelm
parents: 65548
diff changeset
   743
    Sudoku
wenzelm
parents: 65548
diff changeset
   744
    Tarski
wenzelm
parents: 65548
diff changeset
   745
    Termination
wenzelm
parents: 65548
diff changeset
   746
    ThreeDivides
61368
33a62b54f381 add a file with examples of debugging transfer
kuncar
parents: 61232
diff changeset
   747
    Transfer_Debug
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   748
    Transfer_Int_Nat
56922
d411a81b8356 removed junk from library theory
haftmann
parents: 56818
diff changeset
   749
    Transitive_Closure_Table_Ex
65549
wenzelm
parents: 65548
diff changeset
   750
    Tree23
69716
749aaeb40788 Added triangular numbers
Manuel Eberl <eberlm@in.tum.de>
parents: 69689
diff changeset
   751
    Triangular_Numbers
65549
wenzelm
parents: 65548
diff changeset
   752
    Unification
wenzelm
parents: 65548
diff changeset
   753
    While_Combinator_Example
64978
5b9ba120d222 added veriT preprocessing proof reconstruction example
blanchet
parents: 64959
diff changeset
   754
    veriT_Preprocessing
51558
91f8bed6d0a4 allow build with skip_proofs enabled -- disable it for sessions that would fail due to embedded diagnostic commands, for example;
wenzelm
parents: 51553
diff changeset
   755
  theories [skip_proofs = false]
67159
deccbba7cfe3 more robust;
wenzelm
parents: 67152
diff changeset
   756
    SAT_Examples
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
   757
    Meson_Test
77036
d0151eb9ecb0 more correct and complete bibliography;
wenzelm
parents: 77003
diff changeset
   758
  document_files
d0151eb9ecb0 more correct and complete bibliography;
wenzelm
parents: 77003
diff changeset
   759
    "root.bib"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   760
65550
e957b1f00449 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65549
diff changeset
   761
session "HOL-Isar_Examples" in Isar_Examples = "HOL-Computational_Algebra" +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   762
  description "
61935
6512e84cc9f5 clarified sessions;
wenzelm
parents: 61793
diff changeset
   763
    Miscellaneous Isabelle/Isar examples.
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   764
  "
61939
3c8c390a8f0a tuned document;
wenzelm
parents: 61938
diff changeset
   765
  options [quick_and_dirty]
72985
9cc431444435 clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents: 72850
diff changeset
   766
  sessions
9cc431444435 clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents: 72850
diff changeset
   767
    "HOL-Hoare"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   768
  theories
61939
3c8c390a8f0a tuned document;
wenzelm
parents: 61938
diff changeset
   769
    Structured_Statements
3c8c390a8f0a tuned document;
wenzelm
parents: 61938
diff changeset
   770
    Basic_Logic
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   771
    Expr_Compiler
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   772
    Fibonacci
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   773
    Group
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   774
    Group_Context
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   775
    Group_Notepad
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   776
    Hoare_Ex
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   777
    Mutilated_Checkerboard
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   778
    Puzzle
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   779
    Summation
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   780
  document_files
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   781
    "root.bib"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   782
    "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   783
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents: 60008
diff changeset
   784
session "HOL-Eisbach" in Eisbach = HOL +
69272
15e9ed5b28fb isabelle update_cartouches -t;
wenzelm
parents: 69252
diff changeset
   785
  description \<open>
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents: 60008
diff changeset
   786
    The Eisbach proof method language and "match" method.
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   787
  \<close>
66444
6d2d993fa76e clarified imports;
wenzelm
parents: 66443
diff changeset
   788
  sessions
6d2d993fa76e clarified imports;
wenzelm
parents: 66443
diff changeset
   789
    FOL
70958
e8fc52f3f175 a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents: 70956
diff changeset
   790
    "HOL-Analysis"
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents: 60008
diff changeset
   791
  theories
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents: 60008
diff changeset
   792
    Eisbach
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents: 60008
diff changeset
   793
    Tests
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents: 60008
diff changeset
   794
    Examples
62168
e97452d79102 Eisbach works for other object-logics, e.g. Eisbach_FOL.thy;
wenzelm
parents: 62155
diff changeset
   795
    Examples_FOL
70958
e8fc52f3f175 a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents: 70956
diff changeset
   796
    Example_Metric
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents: 60008
diff changeset
   797
71832
f61b19358a8f clarified session imports: avoid bulky HOL-Library image;
wenzelm
parents: 71814
diff changeset
   798
session "HOL-SET_Protocol" (timing) in SET_Protocol = HOL +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   799
  description "
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   800
    Verification of the SET Protocol.
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   801
  "
71832
f61b19358a8f clarified session imports: avoid bulky HOL-Library image;
wenzelm
parents: 71814
diff changeset
   802
  sessions
f61b19358a8f clarified session imports: avoid bulky HOL-Library image;
wenzelm
parents: 71814
diff changeset
   803
    "HOL-Library"
65543
8369b33fda0a clarified session imports;
wenzelm
parents: 65538
diff changeset
   804
  theories
8369b33fda0a clarified session imports;
wenzelm
parents: 65538
diff changeset
   805
    SET_Protocol
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   806
  document_files "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   807
71832
f61b19358a8f clarified session imports: avoid bulky HOL-Library image;
wenzelm
parents: 71814
diff changeset
   808
session "HOL-Matrix_LP" in Matrix_LP = HOL +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   809
  description "
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   810
    Two-dimensional matrices and linear programming.
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   811
  "
71832
f61b19358a8f clarified session imports: avoid bulky HOL-Library image;
wenzelm
parents: 71814
diff changeset
   812
  sessions "HOL-Library"
70675
efd995488228 declare session directories;
wenzelm
parents: 70669
diff changeset
   813
  directories "Compute_Oracle"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   814
  theories Cplex
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   815
  document_files "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   816
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   817
session "HOL-TLA" in TLA = HOL +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   818
  description "
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
   819
    Lamport's Temporal Logic of Actions.
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   820
  "
75916
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents: 75647
diff changeset
   821
  theories
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents: 75647
diff changeset
   822
    README
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents: 75647
diff changeset
   823
    TLA
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   824
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   825
session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   826
  theories Inc
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   827
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   828
session "HOL-TLA-Buffer" in "TLA/Buffer" = "HOL-TLA" +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   829
  theories DBuffer
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   830
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   831
session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   832
  theories MemoryImplementation
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   833
71832
f61b19358a8f clarified session imports: avoid bulky HOL-Library image;
wenzelm
parents: 71814
diff changeset
   834
session "HOL-TPTP" in TPTP = HOL +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   835
  description "
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   836
    Author:     Jasmin Blanchette, TU Muenchen
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   837
    Author:     Nik Sultana, University of Cambridge
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   838
    Copyright   2011
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   839
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   840
    TPTP-related extensions.
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   841
  "
71832
f61b19358a8f clarified session imports: avoid bulky HOL-Library image;
wenzelm
parents: 71814
diff changeset
   842
  sessions
f61b19358a8f clarified session imports: avoid bulky HOL-Library image;
wenzelm
parents: 71814
diff changeset
   843
    "HOL-Library"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   844
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   845
    ATP_Theory_Export
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   846
    MaSh_Eval
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   847
    TPTP_Interpret
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   848
    THF_Arith
55596
928b9f677165 reconstruction framework for LEO-II's TPTP proofs;
sultana
parents: 55450
diff changeset
   849
    TPTP_Proof_Reconstruction
52488
cd65ee49a8ba discontinued system option "proofs" -- global state of Proofterm.proofs is persistently compiled into HOL-Proofs image;
wenzelm
parents: 52424
diff changeset
   850
  theories
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   851
    ATP_Problem_Import
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   852
65382
de848ac5e0d7 more main sessions and global theories;
wenzelm
parents: 65381
diff changeset
   853
session "HOL-Probability" (main timing) in "Probability" = "HOL-Analysis" +
73477
1d8a79aa2a99 dedicated session for combinatorial material
haftmann
parents: 73408
diff changeset
   854
  sessions
1d8a79aa2a99 dedicated session for combinatorial material
haftmann
parents: 73408
diff changeset
   855
    "HOL-Combinatorics"
70781
a37e2ea96c6d just one dump_checkpoint Main -- potentially more robust;
wenzelm
parents: 70678
diff changeset
   856
  theories
66992
69673025292e less global theories -- avoid confusion about special cases;
wenzelm
parents: 66986
diff changeset
   857
    Probability
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   858
  document_files "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   859
63888
5a9a1985e9fb sessions that are relevant for routine timing measurements;
wenzelm
parents: 63885
diff changeset
   860
session "HOL-Probability-ex" (timing) in "Probability/ex" = "HOL-Probability" +
61946
844881193616 put example into separate session, to restrict precious session image to library theories
haftmann
parents: 61939
diff changeset
   861
  theories
65538
a39ef48fbee0 tuned imports;
wenzelm
parents: 65535
diff changeset
   862
    Dining_Cryptographers
a39ef48fbee0 tuned imports;
wenzelm
parents: 65535
diff changeset
   863
    Koepf_Duermuth_Countermeasure
a39ef48fbee0 tuned imports;
wenzelm
parents: 65535
diff changeset
   864
    Measure_Not_CCC
61946
844881193616 put example into separate session, to restrict precious session image to library theories
haftmann
parents: 61939
diff changeset
   865
71832
f61b19358a8f clarified session imports: avoid bulky HOL-Library image;
wenzelm
parents: 71814
diff changeset
   866
session "HOL-Nominal" in Nominal = HOL +
f61b19358a8f clarified session imports: avoid bulky HOL-Library image;
wenzelm
parents: 71814
diff changeset
   867
  sessions "HOL-Library"
70781
a37e2ea96c6d just one dump_checkpoint Main -- potentially more robust;
wenzelm
parents: 70678
diff changeset
   868
  theories
65573
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   869
    Nominal
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   870
63888
5a9a1985e9fb sessions that are relevant for routine timing measurements;
wenzelm
parents: 63885
diff changeset
   871
session "HOL-Nominal-Examples" (timing) in "Nominal/Examples" = "HOL-Nominal" +
58329
a31404ec7414 run larger nominal examples only 'ISABELLE_FULL_TEST'
blanchet
parents: 58313
diff changeset
   872
  theories
59162
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   873
    Class3
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   874
    CK_Machine
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   875
    Compile
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   876
    Contexts
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   877
    Crary
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   878
    CR_Takahashi
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   879
    CR
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   880
    Fsub
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   881
    Height
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   882
    Lambda_mu
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   883
    Lam_Funs
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   884
    LocalWeakening
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   885
    Pattern
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   886
    SN
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   887
    SOS
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   888
    Standardization
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   889
    Support
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   890
    Type_Preservation
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   891
    Weakening
dca5594761f2 afford full test, with slightly improved scheduling order;
wenzelm
parents: 59144
diff changeset
   892
    W
58329
a31404ec7414 run larger nominal examples only 'ISABELLE_FULL_TEST'
blanchet
parents: 58313
diff changeset
   893
  theories [quick_and_dirty]
a31404ec7414 run larger nominal examples only 'ISABELLE_FULL_TEST'
blanchet
parents: 58313
diff changeset
   894
    VC_Condition
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   895
70078
3a1b2d8c89aa bundle for cardinal syntax
traytel
parents: 70026
diff changeset
   896
session "HOL-Cardinals" (timing) in Cardinals = HOL +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   897
  description "
51421
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   898
    Ordinals and Cardinals, Full Theories.
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   899
  "
59747
7325ffa35038 bounded powerset
traytel
parents: 59743
diff changeset
   900
  theories
7325ffa35038 bounded powerset
traytel
parents: 59743
diff changeset
   901
    Cardinals
7325ffa35038 bounded powerset
traytel
parents: 59743
diff changeset
   902
    Bounded_Set
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   903
  document_files
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   904
    "intro.tex"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   905
    "root.tex"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   906
    "root.bib"
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents: 48932
diff changeset
   907
65574
10f4a17e5928 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65573
diff changeset
   908
session "HOL-Datatype_Examples" (timing) in Datatype_Examples = "HOL-Library" +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   909
  description "
62286
705d4c4003ea clarified ISABELLE_FULL_TEST vs. benchmarks: src/Benchmarks is not in ROOTS and thus not covered by "isabelle build -a" by default;
wenzelm
parents: 62285
diff changeset
   910
    (Co)datatype Examples.
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   911
  "
70675
efd995488228 declare session directories;
wenzelm
parents: 70669
diff changeset
   912
  directories "Derivation_Trees"
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents: 48932
diff changeset
   913
  theories
56454
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents: 56215
diff changeset
   914
    Compat
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents: 48932
diff changeset
   915
    Lambda_Term
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents: 48932
diff changeset
   916
    Process
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents: 48932
diff changeset
   917
    TreeFsetI
49872
c6a686c9be2a update ROOT with teh directory change in BNF
popescua
parents: 49693
diff changeset
   918
    "Derivation_Trees/Gram_Lang"
65574
10f4a17e5928 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65573
diff changeset
   919
    "Derivation_Trees/Parallel_Composition"
50517
8f6c11103820 renamed theory
traytel
parents: 50480
diff changeset
   920
    Koenig
60921
487050067be9 actually process lift_bnf regression suite
traytel
parents: 60809
diff changeset
   921
    Lift_BNF
61745
e23e0ff98657 Ported old example to use (co)datatypes
traytel
parents: 61670
diff changeset
   922
    Milner_Tofte
54961
e60428f432bc new codatatype example: stream processors
traytel
parents: 54481
diff changeset
   923
    Stream_Processor
71393
fce780f9c9c6 new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents: 71352
diff changeset
   924
    Cyclic_List
fce780f9c9c6 new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents: 71352
diff changeset
   925
    Free_Idempotent_Monoid
73398
180981b87929 generalized confluence-based subdistributivity theorem for quotients;
traytel
parents: 73108
diff changeset
   926
    Regex_ACI
180981b87929 generalized confluence-based subdistributivity theorem for quotients;
traytel
parents: 73108
diff changeset
   927
    Regex_ACIDZ
71263
35a92ce0b94e an extensive example for lift_bnf across quotients
traytel
parents: 71189
diff changeset
   928
    TLList
73408
be11fe268b33 another example for lift_bnf for quotients
traytel
parents: 73398
diff changeset
   929
    FAE_Sequence
53122
bc87b7af4767 renamed theory files to be closer to (new) command names
blanchet
parents: 52726
diff changeset
   930
    Misc_Codatatype
bc87b7af4767 renamed theory files to be closer to (new) command names
blanchet
parents: 52726
diff changeset
   931
    Misc_Datatype
54193
bc07627c5dcd added 'primcorec' examples
blanchet
parents: 53935
diff changeset
   932
    Misc_Primcorec
53306
45f13517693a added example
blanchet
parents: 53164
diff changeset
   933
    Misc_Primrec
71836
c095d3143047 New HOL simproc 'datatype_no_proper_subterm'
Manuel Eberl <eberlm@in.tum.de>
parents: 71832
diff changeset
   934
    Datatype_Simproc_Tests
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents: 48932
diff changeset
   935
65573
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
   936
session "HOL-Corec_Examples" (timing) in Corec_Examples = "HOL-Library" +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   937
  description "
62694
f50d7efc8fe3 added two 'corec' examples
blanchet
parents: 62479
diff changeset
   938
    Corecursion Examples.
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   939
  "
70675
efd995488228 declare session directories;
wenzelm
parents: 70669
diff changeset
   940
  directories "Tests"
62694
f50d7efc8fe3 added two 'corec' examples
blanchet
parents: 62479
diff changeset
   941
  theories
f50d7efc8fe3 added two 'corec' examples
blanchet
parents: 62479
diff changeset
   942
    LFilter
62734
38fefd98c929 another 'corec' example
blanchet
parents: 62725
diff changeset
   943
    Paper_Examples
62694
f50d7efc8fe3 added two 'corec' examples
blanchet
parents: 62479
diff changeset
   944
    Stream_Processor
62696
7325d8573fb8 added 'corec' examples and tests
blanchet
parents: 62694
diff changeset
   945
    "Tests/Simple_Nesting"
64379
71f42dcaa1df additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents: 64323
diff changeset
   946
    "Tests/Iterate_GPV"
62696
7325d8573fb8 added 'corec' examples and tests
blanchet
parents: 62694
diff changeset
   947
  theories [quick_and_dirty]
7325d8573fb8 added 'corec' examples and tests
blanchet
parents: 62694
diff changeset
   948
    "Tests/GPV_Bare_Bones"
7325d8573fb8 added 'corec' examples and tests
blanchet
parents: 62694
diff changeset
   949
    "Tests/Merge_D"
7325d8573fb8 added 'corec' examples and tests
blanchet
parents: 62694
diff changeset
   950
    "Tests/Merge_Poly"
7325d8573fb8 added 'corec' examples and tests
blanchet
parents: 62694
diff changeset
   951
    "Tests/Misc_Mono"
7325d8573fb8 added 'corec' examples and tests
blanchet
parents: 62694
diff changeset
   952
    "Tests/Misc_Poly"
7325d8573fb8 added 'corec' examples and tests
blanchet
parents: 62694
diff changeset
   953
    "Tests/Small_Concrete"
62725
5ab1746186c7 new 'corec' example
blanchet
parents: 62706
diff changeset
   954
    "Tests/Stream_Friends"
62696
7325d8573fb8 added 'corec' examples and tests
blanchet
parents: 62694
diff changeset
   955
    "Tests/TLList_Friends"
63190
3e79279c10ca added test
blanchet
parents: 63165
diff changeset
   956
    "Tests/Type_Class"
62694
f50d7efc8fe3 added two 'corec' examples
blanchet
parents: 62479
diff changeset
   957
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
   958
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
   959
  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
   960
    StateSpaceEx
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   961
  document_files "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   962
65550
e957b1f00449 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65549
diff changeset
   963
session "HOL-Nonstandard_Analysis" (timing) in Nonstandard_Analysis = "HOL-Computational_Algebra" +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   964
  description "
51421
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
   965
    Nonstandard analysis.
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
   966
  "
62479
716336f19aa9 clarified session;
wenzelm
parents: 62380
diff changeset
   967
  theories
716336f19aa9 clarified session;
wenzelm
parents: 62380
diff changeset
   968
    Nonstandard_Analysis
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
   969
  document_files "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   970
63888
5a9a1985e9fb sessions that are relevant for routine timing measurements;
wenzelm
parents: 63885
diff changeset
   971
session "HOL-Nonstandard_Analysis-Examples" (timing) in "Nonstandard_Analysis/Examples" = "HOL-Nonstandard_Analysis" +
65543
8369b33fda0a clarified session imports;
wenzelm
parents: 65538
diff changeset
   972
  theories
8369b33fda0a clarified session imports;
wenzelm
parents: 65538
diff changeset
   973
    NSPrimes
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   974
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents: 73662
diff changeset
   975
session "HOL-Mirabelle-ex" in "Tools/Mirabelle" = HOL +
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents: 73662
diff changeset
   976
  description "Some arbitrary small test case for Mirabelle."
73822
1192c68ebe1c suppress theories from other sessions, unless explicitly specified via mirabelle_theories;
wenzelm
parents: 73811
diff changeset
   977
  options [timeout = 60,
1192c68ebe1c suppress theories from other sessions, unless explicitly specified via mirabelle_theories;
wenzelm
parents: 73811
diff changeset
   978
    mirabelle_theories = "HOL-Analysis.Inner_Product", mirabelle_actions = "arith"]
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents: 73662
diff changeset
   979
  sessions
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents: 73662
diff changeset
   980
    "HOL-Analysis"
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents: 73662
diff changeset
   981
  theories
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents: 73662
diff changeset
   982
    "HOL-Analysis.Inner_Product"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   983
72515
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72486
diff changeset
   984
session "HOL-SMT_Examples" (timing) in SMT_Examples = HOL +
66946
3d8fd98c7c86 ROOT cleanup: empty 'document_files' means there is no document;
wenzelm
parents: 66932
diff changeset
   985
  options [quick_and_dirty]
72515
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72486
diff changeset
   986
  sessions
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72486
diff changeset
   987
    "HOL-Library"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   988
  theories
52722
2c81f7baf8c4 removed obsolete HOL-Boogie session;
boehmes
parents: 52499
diff changeset
   989
    Boogie
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   990
    SMT_Examples
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   991
    SMT_Word_Examples
73654
6e85281177df proper condition: z3 could be absent, e.g. on arm64-linux;
wenzelm
parents: 73546
diff changeset
   992
    SMT_Examples_Verit
72458
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 72389
diff changeset
   993
    SMT_Tests_Verit
73657
dceb5dde442f proper settings variable, amending 6e85281177df;
wenzelm
parents: 73654
diff changeset
   994
  theories [condition = Z3_INSTALLED]
73654
6e85281177df proper condition: z3 could be absent, e.g. on arm64-linux;
wenzelm
parents: 73546
diff changeset
   995
    SMT_Tests
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
   996
72515
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72486
diff changeset
   997
session "HOL-SPARK" in "SPARK" = HOL +
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72486
diff changeset
   998
  sessions
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72486
diff changeset
   999
    "HOL-Library"
65382
de848ac5e0d7 more main sessions and global theories;
wenzelm
parents: 65381
diff changeset
  1000
  theories
66992
69673025292e less global theories -- avoid confusion about special cases;
wenzelm
parents: 66986
diff changeset
  1001
    SPARK
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1002
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
  1003
session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
70675
efd995488228 declare session directories;
wenzelm
parents: 70669
diff changeset
  1004
  directories "Gcd" "Liseq" "RIPEMD-160" "Sqrt"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1005
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1006
    "Gcd/Greatest_Common_Divisor"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1007
    "Liseq/Longest_Increasing_Subsequence"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1008
    "RIPEMD-160/F"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1009
    "RIPEMD-160/Hash"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1010
    "RIPEMD-160/K_L"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1011
    "RIPEMD-160/K_R"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1012
    "RIPEMD-160/R_L"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1013
    "RIPEMD-160/Round"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1014
    "RIPEMD-160/R_R"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1015
    "RIPEMD-160/S_L"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1016
    "RIPEMD-160/S_R"
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1017
    "Sqrt/Sqrt"
70026
6ae9505d693a more convenient export;
wenzelm
parents: 70018
diff changeset
  1018
  export_files (in ".") "*:**.prv"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1019
65576
8376f83f9094 recovered document from 0f3fdf689bf9;
wenzelm
parents: 65574
diff changeset
  1020
session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +
69099
d44cb8a3e5e0 HOL-SPARK .prv files are no longer written to the file-system;
wenzelm
parents: 69093
diff changeset
  1021
  options [show_question_marks = false]
66031
94cfcae2b228 clarified imports;
wenzelm
parents: 66015
diff changeset
  1022
  sessions
72515
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72486
diff changeset
  1023
    "HOL-Library"
66031
94cfcae2b228 clarified imports;
wenzelm
parents: 66015
diff changeset
  1024
    "HOL-SPARK-Examples"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1025
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1026
    Example_Verification
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1027
    VC_Principles
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1028
    Reference
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1029
    Complex_Types
72601
110bfed4815d proper document_theories;
wenzelm
parents: 72536
diff changeset
  1030
  document_theories
110bfed4815d proper document_theories;
wenzelm
parents: 72536
diff changeset
  1031
    "HOL-SPARK-Examples.Greatest_Common_Divisor"
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
  1032
  document_files
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
  1033
    "complex_types.ads"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
  1034
    "complex_types_app.adb"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
  1035
    "complex_types_app.ads"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
  1036
    "Gcd.adb"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
  1037
    "Gcd.ads"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
  1038
    "intro.tex"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
  1039
    "loop_invariant.adb"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
  1040
    "loop_invariant.ads"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
  1041
    "root.bib"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
  1042
    "root.tex"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
  1043
    "Simple_Gcd.adb"
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
  1044
    "Simple_Gcd.ads"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1045
71832
f61b19358a8f clarified session imports: avoid bulky HOL-Library image;
wenzelm
parents: 71814
diff changeset
  1046
session "HOL-Mutabelle" in Mutabelle = HOL +
f61b19358a8f clarified session imports: avoid bulky HOL-Library image;
wenzelm
parents: 71814
diff changeset
  1047
  sessions "HOL-Library"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1048
  theories MutabelleExtra
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1049
71832
f61b19358a8f clarified session imports: avoid bulky HOL-Library image;
wenzelm
parents: 71814
diff changeset
  1050
session "HOL-Quickcheck_Examples" (timing) in Quickcheck_Examples = HOL +
f61b19358a8f clarified session imports: avoid bulky HOL-Library image;
wenzelm
parents: 71814
diff changeset
  1051
  sessions "HOL-Library"
48588
23456b2a769d added Quickcheck_Benchmark (cf. 1959baa22632);
wenzelm
parents: 48512
diff changeset
  1052
  theories
48690
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
  1053
    Quickcheck_Examples
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
  1054
    Quickcheck_Lattice_Examples
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
  1055
    Completeness
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
  1056
    Quickcheck_Interfaces
63731
9f906a2eb0e7 added theory to provide workaround to support nested datatypes in quickcheck (until quickcheck is generalized to support it with new datatypes)
blanchet
parents: 63643
diff changeset
  1057
    Quickcheck_Nesting_Example
57584
155b7e3b729e proper condition wrt. ISABELLE_GHC (cf. 8840fa17e17c);
wenzelm
parents: 57544
diff changeset
  1058
  theories [condition = ISABELLE_GHC]
57544
8840fa17e17c reactivate session Quickcheck_Examples
Andreas Lochbihler
parents: 57543
diff changeset
  1059
    Hotel_Example
48598
7f4561d43d39 updated ROOT according to 3defa60a7ae3;
wenzelm
parents: 48589
diff changeset
  1060
    Quickcheck_Narrowing_Examples
48588
23456b2a769d added Quickcheck_Benchmark (cf. 1959baa22632);
wenzelm
parents: 48512
diff changeset
  1061
65569
3cb6f3281ef1 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65563
diff changeset
  1062
session "HOL-Quotient_Examples" (timing) in Quotient_Examples = "HOL-Algebra" +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
  1063
  description "
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1064
    Author:     Cezary Kaliszyk and Christian Urban
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
  1065
  "
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1066
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1067
    DList
63920
003622e08379 resolve the name clash of HOL/Library/FSet and HOL/Quotient_Examples/FSet
kuncar
parents: 63888
diff changeset
  1068
    Quotient_FSet
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1069
    Quotient_Int
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1070
    Quotient_Message
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1071
    Lift_FSet
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1072
    Lift_Set
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1073
    Lift_Fun
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1074
    Quotient_Rat
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1075
    Lift_DList
53682
1b55aeda0e46 include Int_Pow into Quotient_Examples; add end of the theory
kuncar
parents: 53430
diff changeset
  1076
    Int_Pow
60237
d47387d4a3c6 add testing file for code_dt extension of lifting
kuncar
parents: 60119
diff changeset
  1077
    Lifting_Code_Dt_Test
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1078
71832
f61b19358a8f clarified session imports: avoid bulky HOL-Library image;
wenzelm
parents: 71814
diff changeset
  1079
session "HOL-Predicate_Compile_Examples" (timing) in Predicate_Compile_Examples = HOL +
f61b19358a8f clarified session imports: avoid bulky HOL-Library image;
wenzelm
parents: 71814
diff changeset
  1080
  sessions "HOL-Library"
62354
fdd6989cc8a0 SML/NJ is no longer supported;
wenzelm
parents: 62286
diff changeset
  1081
  theories
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1082
    Examples
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1083
    Predicate_Compile_Tests
61140
78ece168f5b5 reactivate examples with predicate compiler and quickcheck
Andreas Lochbihler
parents: 60921
diff changeset
  1084
    Predicate_Compile_Quickcheck_Examples
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1085
    Specialisation_Examples
48690
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
  1086
    IMP_1
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
  1087
    IMP_2
55450
9eddc17749f7 reactivate some examples that still appear to work;
wenzelm
parents: 55447
diff changeset
  1088
    (* FIXME since 21-Jul-2011
61140
78ece168f5b5 reactivate examples with predicate compiler and quickcheck
Andreas Lochbihler
parents: 60921
diff changeset
  1089
    Hotel_Example_Small_Generator *)
48690
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
  1090
    IMP_3
61140
78ece168f5b5 reactivate examples with predicate compiler and quickcheck
Andreas Lochbihler
parents: 60921
diff changeset
  1091
    IMP_4
62242
a4e6ea45f416 guard sessions that no longer work with SML/NJ -- memory problems;
wenzelm
parents: 62168
diff changeset
  1092
  theories [condition = ISABELLE_SWIPL]
48690
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
  1093
    Code_Prolog_Examples
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
  1094
    Context_Free_Grammar_Example
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
  1095
    Hotel_Example_Prolog
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
  1096
    Lambda_Example
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
  1097
    List_Examples
62242
a4e6ea45f416 guard sessions that no longer work with SML/NJ -- memory problems;
wenzelm
parents: 62168
diff changeset
  1098
  theories [condition = ISABELLE_SWIPL, quick_and_dirty]
48690
c1499b14b48c more precise imitation of old ROOT.ML files;
wenzelm
parents: 48679
diff changeset
  1099
    Reg_Exp_Example
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1100
64551
79e9587dbcca proper session HOL-Types_To_Sets;
wenzelm
parents: 64431
diff changeset
  1101
session "HOL-Types_To_Sets" in Types_To_Sets = HOL +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
  1102
  description "
64551
79e9587dbcca proper session HOL-Types_To_Sets;
wenzelm
parents: 64431
diff changeset
  1103
    Experimental extension of Higher-Order Logic to allow translation of types to sets.
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
  1104
  "
70675
efd995488228 declare session directories;
wenzelm
parents: 70669
diff changeset
  1105
  directories "Examples"
64551
79e9587dbcca proper session HOL-Types_To_Sets;
wenzelm
parents: 64431
diff changeset
  1106
  theories
79e9587dbcca proper session HOL-Types_To_Sets;
wenzelm
parents: 64431
diff changeset
  1107
    Types_To_Sets
79e9587dbcca proper session HOL-Types_To_Sets;
wenzelm
parents: 64431
diff changeset
  1108
    "Examples/Prerequisites"
79e9587dbcca proper session HOL-Types_To_Sets;
wenzelm
parents: 64431
diff changeset
  1109
    "Examples/Finite"
79e9587dbcca proper session HOL-Types_To_Sets;
wenzelm
parents: 64431
diff changeset
  1110
    "Examples/T2_Spaces"
69689
ab5a8a2519b0 automation for unverloading definitions
immler
parents: 69545
diff changeset
  1111
    "Examples/Unoverload_Def"
68522
d9cbc1e8644d example for Types_To_Sets: transfer from type-based linear algebra to subspaces
immler
parents: 68516
diff changeset
  1112
    "Examples/Linear_Algebra_On"
64551
79e9587dbcca proper session HOL-Types_To_Sets;
wenzelm
parents: 64431
diff changeset
  1113
66982
67595389aa8a build faster without heap images for minor imports;
wenzelm
parents: 66956
diff changeset
  1114
session HOLCF (main timing) in HOLCF = HOL +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
  1115
  description "
48338
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
  1116
    Author:     Franz Regensburger
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
  1117
    Author:     Brian Huffman
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
  1118
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
  1119
    HOLCF -- a semantic extension of HOL by the LCF logic.
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
  1120
  "
66982
67595389aa8a build faster without heap images for minor imports;
wenzelm
parents: 66956
diff changeset
  1121
  sessions
67595389aa8a build faster without heap images for minor imports;
wenzelm
parents: 66956
diff changeset
  1122
    "HOL-Library"
75916
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents: 75647
diff changeset
  1123
  theories [document = false]
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents: 75647
diff changeset
  1124
    README
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1125
  theories
65382
de848ac5e0d7 more main sessions and global theories;
wenzelm
parents: 65381
diff changeset
  1126
    HOLCF (global)
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
  1127
  document_files "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1128
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
  1129
session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF +
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1130
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1131
    Domain_ex
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1132
    Fixrec_ex
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1133
    New_Domain
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 56680
diff changeset
  1134
  document_files "root.tex"
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1135
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
  1136
session "HOLCF-Library" in "HOLCF/Library" = HOLCF +
65570
660df4a6dc59 actually use theory;
wenzelm
parents: 65569
diff changeset
  1137
  theories
660df4a6dc59 actually use theory;
wenzelm
parents: 65569
diff changeset
  1138
    HOLCF_Library
660df4a6dc59 actually use theory;
wenzelm
parents: 65569
diff changeset
  1139
    HOL_Cpo
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1140
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
  1141
session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
  1142
  description "
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1143
    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
  1144
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1145
    This is the HOLCF-based denotational semantics of a simple WHILE-language.
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
  1146
  "
65573
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
  1147
  sessions
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
  1148
    "HOL-IMP"
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
  1149
  theories
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
  1150
    HoareEx
66950
1a5e90026391 recovered document from 9bfb6978eb80;
wenzelm
parents: 66946
diff changeset
  1151
  document_files
1a5e90026391 recovered document from 9bfb6978eb80;
wenzelm
parents: 66946
diff changeset
  1152
    "isaverbatimwrite.sty"
1a5e90026391 recovered document from 9bfb6978eb80;
wenzelm
parents: 66946
diff changeset
  1153
    "root.tex"
1a5e90026391 recovered document from 9bfb6978eb80;
wenzelm
parents: 66946
diff changeset
  1154
    "root.bib"
48338
3592a2091c80 some HOL sessions;
wenzelm
parents:
diff changeset
  1155
65573
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
  1156
session "HOLCF-ex" in "HOLCF/ex" = "HOLCF-Library" +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
  1157
  description "
51421
b5d559b101d9 more uniform session descriptions, which show up in chapter index;
wenzelm
parents: 51403
diff changeset
  1158
    Miscellaneous examples for HOLCF.
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
  1159
  "
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1160
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1161
    Dnat
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1162
    Dagstuhl
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1163
    Focus_ex
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1164
    Fix2
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1165
    Hoare
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1166
    Concurrency_Monad
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1167
    Loop
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1168
    Powerdomain_ex
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1169
    Domain_Proofs
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1170
    Letrec
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1171
    Pattern_Match
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1172
65573
0f3fdf689bf9 clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents: 65570
diff changeset
  1173
session "HOLCF-FOCUS" in "HOLCF/FOCUS" = "HOLCF-Library" +
69272
15e9ed5b28fb isabelle update_cartouches -t;
wenzelm
parents: 69252
diff changeset
  1174
  description \<open>
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1175
    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
  1176
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1177
    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
  1178
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1179
    "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
  1180
    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
  1181
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1182
    "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
  1183
    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
  1184
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1185
    "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
  1186
    Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
  1187
  \<close>
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1188
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1189
    Fstreams
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1190
    FOCUS
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1191
    Buffer_adm
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1192
63888
5a9a1985e9fb sessions that are relevant for routine timing measurements;
wenzelm
parents: 63885
diff changeset
  1193
session IOA (timing) in "HOLCF/IOA" = HOLCF +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
  1194
  description "
72835
66ca5016b008 more Unicode;
wenzelm
parents: 72834
diff changeset
  1195
    Author:     Olaf Müller
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1196
    Copyright   1997 TU München
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1197
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1198
    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
  1199
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
  1200
    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
  1201
    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
  1202
    finite and infinite sequences.
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
  1203
  "
65538
a39ef48fbee0 tuned imports;
wenzelm
parents: 65535
diff changeset
  1204
  theories Abstraction
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1205
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
  1206
session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
  1207
  description "
72835
66ca5016b008 more Unicode;
wenzelm
parents: 72834
diff changeset
  1208
    Author:     Olaf Müller
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1209
72833
fe7df3f7412e eliminated odd "Read_me";
wenzelm
parents: 72688
diff changeset
  1210
    The Alternating Bit Protocol performed in I/O-Automata:
fe7df3f7412e eliminated odd "Read_me";
wenzelm
parents: 72688
diff changeset
  1211
    combining IOA with Model Checking.
fe7df3f7412e eliminated odd "Read_me";
wenzelm
parents: 72688
diff changeset
  1212
fe7df3f7412e eliminated odd "Read_me";
wenzelm
parents: 72688
diff changeset
  1213
    Theory Correctness contains the proof of the abstraction from unbounded
fe7df3f7412e eliminated odd "Read_me";
wenzelm
parents: 72688
diff changeset
  1214
    channels to finite ones.
fe7df3f7412e eliminated odd "Read_me";
wenzelm
parents: 72688
diff changeset
  1215
72850
4cb480334f48 spelling;
wenzelm
parents: 72835
diff changeset
  1216
    File Check.ML contains a simple ModelChecker prototype checking Spec
72833
fe7df3f7412e eliminated odd "Read_me";
wenzelm
parents: 72688
diff changeset
  1217
    against the finite version of the ABP-protocol.
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
  1218
  "
59503
9937bc07202b check unused theory;
wenzelm
parents: 59446
diff changeset
  1219
  theories
9937bc07202b check unused theory;
wenzelm
parents: 59446
diff changeset
  1220
    Correctness
9937bc07202b check unused theory;
wenzelm
parents: 59446
diff changeset
  1221
    Spec
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1222
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
  1223
session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
  1224
  description "
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1225
    Author:     Tobias Nipkow & Konrad Slind
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1226
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1227
    A network transmission protocol, performed in the
72835
66ca5016b008 more Unicode;
wenzelm
parents: 72834
diff changeset
  1228
    I/O automata formalization by Olaf Müller.
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
  1229
  "
72834
a025f845fd41 eliminated odd "Read_me";
wenzelm
parents: 72833
diff changeset
  1230
  theories
a025f845fd41 eliminated odd "Read_me";
wenzelm
parents: 72833
diff changeset
  1231
    Overview
a025f845fd41 eliminated odd "Read_me";
wenzelm
parents: 72833
diff changeset
  1232
    Correctness
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1233
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
  1234
session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
  1235
  description "
72835
66ca5016b008 more Unicode;
wenzelm
parents: 72834
diff changeset
  1236
    Author:     Olaf Müller
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1237
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1238
    Memory storage case study.
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
  1239
  "
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1240
  theories Correctness
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1241
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48721
diff changeset
  1242
session "IOA-ex" in "HOLCF/IOA/ex" = IOA +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
  1243
  description "
72835
66ca5016b008 more Unicode;
wenzelm
parents: 72834
diff changeset
  1244
    Author:     Olaf Müller
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
  1245
  "
48481
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1246
  theories
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1247
    TrivEx
2c828c830ad7 more session entries;
wenzelm
parents: 48470
diff changeset
  1248
    TrivEx2