src/HOL/ROOT
author Andreas Lochbihler
Sun Jul 15 23:44:38 2018 +0200 (18 months ago)
changeset 68639 357fca99a65a
parent 68617 75129a73aca3
child 68640 f15daa73ee32
permissions -rw-r--r--
more examples for Code_Lazy
     1 chapter HOL
     2 
     3 session HOL (main) = Pure +
     4   description {*
     5     Classical Higher-order Logic.
     6   *}
     7   theories
     8     Main (global)
     9     Complex_Main (global)
    10   document_files
    11     "root.bib"
    12     "root.tex"
    13 
    14 session "HOL-Proofs" (timing) = Pure +
    15   description {*
    16     HOL-Main with explicit proof terms.
    17   *}
    18   options [quick_and_dirty = false, record_proofs = 2, parallel_proofs = 0, parallel_limit = 500]
    19   sessions
    20     "HOL-Library"
    21   theories
    22     "HOL-Library.Realizers"
    23 
    24 session "HOL-Library" (main timing) in Library = HOL +
    25   description {*
    26     Classical Higher-order Logic -- batteries included.
    27   *}
    28   theories
    29     Library
    30     (*conflicting type class instantiations and dependent applications*)
    31     Finite_Lattice
    32     List_Lexorder
    33     Prefix_Order
    34     Product_Lexorder
    35     Product_Order
    36     Subseq_Order
    37     (*conflicting syntax*)
    38     Datatype_Records
    39     (*data refinements and dependent applications*)
    40     AList_Mapping
    41     Code_Binary_Nat
    42     Code_Prolog
    43     Code_Real_Approx_By_Float
    44     Code_Target_Numeral
    45     DAList
    46     DAList_Multiset
    47     RBT_Mapping
    48     RBT_Set
    49     (*printing modifications*)
    50     OptionalSugar
    51     (*prototypic tools*)
    52     Predicate_Compile_Quickcheck
    53     (*legacy tools*)
    54     Old_Datatype
    55     Old_Recdef
    56     Realizers
    57     Refute
    58   document_files "root.bib" "root.tex"
    59 
    60 session "HOL-Analysis" (main timing) in Analysis = HOL +
    61   options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant",
    62     document_variants = "document:manual=-proof,-ML,-unimportant"]
    63   sessions
    64     "HOL-Library"
    65     "HOL-Computational_Algebra"
    66   theories
    67     Analysis
    68   document_files
    69     "root.tex"
    70 
    71 session "HOL-Analysis-ex" in "Analysis/ex" = "HOL-Analysis" +
    72   theories
    73     Approximations
    74 
    75 session "HOL-Computational_Algebra" (main timing) in "Computational_Algebra" = "HOL-Library" +
    76   theories
    77     Computational_Algebra
    78     (*conflicting type class instantiations and dependent applications*)
    79     Field_as_Ring
    80 
    81 session "HOL-Hahn_Banach" in Hahn_Banach = "HOL-Library" +
    82   description {*
    83     Author:     Gertrud Bauer, TU Munich
    84 
    85     The Hahn-Banach theorem for real vector spaces.
    86 
    87     This is the proof of the Hahn-Banach theorem for real vectorspaces,
    88     following H. Heuser, Funktionalanalysis, p. 228 -232. The Hahn-Banach
    89     theorem is one of the fundamental theorems of functional analysis. It is a
    90     conclusion of Zorn's lemma.
    91 
    92     Two different formaulations of the theorem are presented, one for general
    93     real vectorspaces and its application to normed vectorspaces.
    94 
    95     The theorem says, that every continous linearform, defined on arbitrary
    96     subspaces (not only one-dimensional subspaces), can be extended to a
    97     continous linearform on the whole vectorspace.
    98   *}
    99   sessions
   100     "HOL-Analysis"
   101   theories
   102     Hahn_Banach
   103   document_files "root.bib" "root.tex"
   104 
   105 session "HOL-Induct" in Induct = "HOL-Library" +
   106   description {*
   107     Examples of (Co)Inductive Definitions.
   108 
   109     Comb proves the Church-Rosser theorem for combinators (see
   110     http://www.cl.cam.ac.uk/ftp/papers/reports/TR396-lcp-generic-automatic-proof-tools.ps.gz).
   111 
   112     Mutil is the famous Mutilated Chess Board problem (see
   113     http://www.cl.cam.ac.uk/ftp/papers/reports/TR394-lcp-mutilated-chess-board.dvi.gz).
   114 
   115     PropLog proves the completeness of a formalization of propositional logic
   116     (see
   117     http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz).
   118 
   119     Exp demonstrates the use of iterated inductive definitions to reason about
   120     mutually recursive relations.
   121   *}
   122   theories [quick_and_dirty]
   123     Common_Patterns
   124   theories
   125     Nested_Datatype
   126     QuoDataType
   127     QuoNestedDataType
   128     Term
   129     SList
   130     ABexp
   131     Infinitely_Branching_Tree
   132     Ordinals
   133     Sigma_Algebra
   134     Comb
   135     PropLog
   136     Com
   137   document_files "root.tex"
   138 
   139 session "HOL-IMP" (timing) in IMP = "HOL-Library" +
   140   options [document_variants = document]
   141   theories
   142     BExp
   143     ASM
   144     Finite_Reachable
   145     Denotational
   146     Compiler2
   147     Poly_Types
   148     Sec_Typing
   149     Sec_TypingT
   150     Def_Init_Big
   151     Def_Init_Small
   152     Fold
   153     Live
   154     Live_True
   155     Hoare_Examples
   156     Hoare_Sound_Complete
   157     VCG
   158     Hoare_Total
   159     VCG_Total_EX
   160     VCG_Total_EX2
   161     Collecting1
   162     Collecting_Examples
   163     Abs_Int_Tests
   164     Abs_Int1_parity
   165     Abs_Int1_const
   166     Abs_Int3
   167     Procs_Dyn_Vars_Dyn
   168     Procs_Stat_Vars_Dyn
   169     Procs_Stat_Vars_Stat
   170     C_like
   171     OO
   172   document_files "root.bib" "root.tex"
   173 
   174 session "HOL-IMPP" in IMPP = HOL +
   175   description {*
   176     Author:     David von Oheimb
   177     Copyright   1999 TUM
   178 
   179     IMPP -- An imperative language with procedures.
   180 
   181     This is an extension of IMP with local variables and mutually recursive
   182     procedures. For documentation see "Hoare Logic for Mutual Recursion and
   183     Local Variables" (http://isabelle.in.tum.de/Bali/papers/FSTTCS99.html).
   184   *}
   185   theories EvenOdd
   186 
   187 session "HOL-Data_Structures" (timing) in Data_Structures = HOL +
   188   options [document_variants = document]
   189   sessions
   190     "HOL-Number_Theory"
   191   theories [document = false]
   192     Less_False
   193   theories
   194     Sorting
   195     Balance
   196     Tree_Map
   197     AVL_Map
   198     RBT_Map
   199     Tree23_Map
   200     Tree234_Map
   201     Brother12_Map
   202     AA_Map
   203     Set2_Join_RBT
   204     Trie
   205     Leftist_Heap
   206     Binomial_Heap
   207   document_files "root.tex" "root.bib"
   208 
   209 session "HOL-Import" in Import = HOL +
   210   theories HOL_Light_Maps
   211   theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import
   212 
   213 session "HOL-Number_Theory" (main timing) in Number_Theory = "HOL-Computational_Algebra" +
   214   description {*
   215     Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler
   216     Theorem, Wilson's Theorem, some lemmas for Quadratic Reciprocity.
   217   *}
   218   sessions
   219     "HOL-Algebra"
   220   theories
   221     Number_Theory
   222   document_files
   223     "root.tex"
   224 
   225 session "HOL-Hoare" in Hoare = HOL +
   226   description {*
   227     Verification of imperative programs (verification conditions are generated
   228     automatically from pre/post conditions and loop invariants).
   229   *}
   230   theories Hoare
   231   document_files "root.bib" "root.tex"
   232 
   233 session "HOL-Hoare_Parallel" (timing) in Hoare_Parallel = HOL +
   234   description {*
   235     Verification of shared-variable imperative programs a la Owicki-Gries.
   236     (verification conditions are generated automatically).
   237   *}
   238   theories Hoare_Parallel
   239   document_files "root.bib" "root.tex"
   240 
   241 session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Number_Theory" +
   242   sessions
   243     "HOL-Data_Structures"
   244     "HOL-ex"
   245   theories
   246     Generate
   247     Generate_Binary_Nat
   248     Generate_Target_Nat
   249     Generate_Efficient_Datastructures
   250     Code_Lazy_Test
   251     Code_Test_PolyML
   252     Code_Test_Scala
   253   theories [condition = ISABELLE_GHC]
   254     Code_Test_GHC
   255   theories [condition = ISABELLE_MLTON]
   256     Code_Test_MLton
   257   theories [condition = ISABELLE_OCAMLC]
   258     Code_Test_OCaml
   259   theories [condition = ISABELLE_SMLNJ]
   260     Code_Test_SMLNJ
   261 
   262 session "HOL-Metis_Examples" (timing) in Metis_Examples = "HOL-Library" +
   263   description {*
   264     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   265     Author:     Jasmin Blanchette, TU Muenchen
   266 
   267     Testing Metis and Sledgehammer.
   268   *}
   269   sessions
   270     "HOL-Decision_Procs"
   271   theories
   272     Abstraction
   273     Big_O
   274     Binary_Tree
   275     Clausification
   276     Message
   277     Proxies
   278     Tarski
   279     Trans_Closure
   280     Sets
   281 
   282 session "HOL-Nitpick_Examples" in Nitpick_Examples = "HOL-Library" +
   283   description {*
   284     Author:     Jasmin Blanchette, TU Muenchen
   285     Copyright   2009
   286   *}
   287   theories [quick_and_dirty] Nitpick_Examples
   288 
   289 session "HOL-Algebra" (main timing) in Algebra = "HOL-Computational_Algebra" +
   290   description {*
   291     Author: Clemens Ballarin, started 24 September 1999, and many others
   292 
   293     The Isabelle Algebraic Library.
   294   *}
   295   theories
   296     (* Orders and Lattices *)
   297     Galois_Connection    (* Knaster-Tarski theorem and Galois connections *)
   298     (* Groups *)
   299     FiniteProduct        (* Product operator for commutative groups *)
   300     Sylow                (* Sylow's theorem *)
   301     Bij                  (* Automorphism Groups *)
   302     Multiplicative_Group
   303     Zassenhaus            (* The Zassenhaus lemma *)
   304     (* Rings *)
   305     Divisibility         (* Rings *)
   306     IntRing              (* Ideals and residue classes *)
   307     UnivPoly             (* Polynomials *)
   308     (* Main theory *)
   309     Algebra             
   310   document_files "root.bib" "root.tex"
   311 
   312 session "HOL-Auth" (timing) in Auth = "HOL-Library" +
   313   description {*
   314     A new approach to verifying authentication protocols.
   315   *}
   316   theories
   317     Auth_Shared
   318     Auth_Public
   319     "Smartcard/Auth_Smartcard"
   320     "Guard/Auth_Guard_Shared"
   321     "Guard/Auth_Guard_Public"
   322   document_files "root.tex"
   323 
   324 session "HOL-UNITY" (timing) in UNITY = "HOL-Auth" +
   325   description {*
   326     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   327     Copyright   1998  University of Cambridge
   328 
   329     Verifying security protocols using Chandy and Misra's UNITY formalism.
   330   *}
   331   theories
   332     (*Basic meta-theory*)
   333     UNITY_Main
   334 
   335     (*Simple examples: no composition*)
   336     "Simple/Deadlock"
   337     "Simple/Common"
   338     "Simple/Network"
   339     "Simple/Token"
   340     "Simple/Channel"
   341     "Simple/Lift"
   342     "Simple/Mutex"
   343     "Simple/Reach"
   344     "Simple/Reachability"
   345 
   346     (*Verifying security protocols using UNITY*)
   347     "Simple/NSP_Bad"
   348 
   349     (*Example of composition*)
   350     "Comp/Handshake"
   351 
   352     (*Universal properties examples*)
   353     "Comp/Counter"
   354     "Comp/Counterc"
   355     "Comp/Priority"
   356 
   357     "Comp/TimerArray"
   358     "Comp/Progress"
   359 
   360     "Comp/Alloc"
   361     "Comp/AllocImpl"
   362     "Comp/Client"
   363 
   364     (*obsolete*)
   365     ELT
   366   document_files "root.tex"
   367 
   368 session "HOL-Unix" in Unix = "HOL-Library" +
   369   options [print_mode = "no_brackets,no_type_brackets"]
   370   theories Unix
   371   document_files "root.bib" "root.tex"
   372 
   373 session "HOL-ZF" in ZF = "HOL-Library" +
   374   theories
   375     MainZF
   376     Games
   377   document_files "root.tex"
   378 
   379 session "HOL-Imperative_HOL" (timing) in Imperative_HOL = "HOL-Library" +
   380   options [print_mode = "iff,no_brackets"]
   381   theories Imperative_HOL_ex
   382   document_files "root.bib" "root.tex"
   383 
   384 session "HOL-Decision_Procs" (timing) in Decision_Procs = "HOL-Algebra" +
   385   description {*
   386     Various decision procedures, typically involving reflection.
   387   *}
   388   theories
   389     Decision_Procs
   390 
   391 session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
   392   sessions
   393     "HOL-Isar_Examples"
   394   theories
   395     Hilbert_Classical
   396     Proof_Terms
   397     XML_Data
   398 
   399 session "HOL-Proofs-Extraction" (timing) in "Proofs/Extraction" = "HOL-Proofs" +
   400   description {*
   401     Examples for program extraction in Higher-Order Logic.
   402   *}
   403   options [parallel_proofs = 0, quick_and_dirty = false]
   404   sessions
   405     "HOL-Computational_Algebra"
   406   theories
   407     Greatest_Common_Divisor
   408     Warshall
   409     Higman_Extraction
   410     Pigeonhole
   411     Euclid
   412   document_files "root.bib" "root.tex"
   413 
   414 session "HOL-Proofs-Lambda" (timing) in "Proofs/Lambda" = "HOL-Proofs" +
   415   description {*
   416     Lambda Calculus in de Bruijn's Notation.
   417 
   418     This session defines lambda-calculus terms with de Bruijn indixes and
   419     proves confluence of beta, eta and beta+eta.
   420 
   421     The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole
   422     theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html).
   423   *}
   424   options [print_mode = "no_brackets",
   425     parallel_proofs = 0, quick_and_dirty = false]
   426   sessions
   427     "HOL-Library"
   428   theories
   429     Eta
   430     StrongNorm
   431     Standardization
   432     WeakNorm
   433   document_files "root.bib" "root.tex"
   434 
   435 session "HOL-Prolog" in Prolog = HOL +
   436   description {*
   437     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
   438 
   439     A bare-bones implementation of Lambda-Prolog.
   440 
   441     This is a simple exploratory implementation of Lambda-Prolog in HOL,
   442     including some minimal examples (in Test.thy) and a more typical example of
   443     a little functional language and its type system.
   444   *}
   445   theories Test Type
   446 
   447 session "HOL-MicroJava" (timing) in MicroJava = "HOL-Library" +
   448   description {*
   449     Formalization of a fragment of Java, together with a corresponding virtual
   450     machine and a specification of its bytecode verifier and a lightweight
   451     bytecode verifier, including proofs of type-safety.
   452   *}
   453   sessions
   454     "HOL-Eisbach"
   455   theories
   456     MicroJava
   457   document_files
   458     "introduction.tex"
   459     "root.bib"
   460     "root.tex"
   461 
   462 session "HOL-NanoJava" in NanoJava = HOL +
   463   description {*
   464     Hoare Logic for a tiny fragment of Java.
   465   *}
   466   theories Example
   467   document_files "root.bib" "root.tex"
   468 
   469 session "HOL-Bali" (timing) in Bali = "HOL-Library" +
   470   theories
   471     AxExample
   472     AxSound
   473     AxCompl
   474     Trans
   475     TypeSafe
   476   document_files "root.tex"
   477 
   478 session "HOL-IOA" in IOA = HOL +
   479   description {*
   480     Author:     Tobias Nipkow and Konrad Slind and Olaf Müller
   481     Copyright   1994--1996  TU Muenchen
   482 
   483     The meta-theory of I/O-Automata in HOL. This formalization has been
   484     significantly changed and extended, see HOLCF/IOA. There are also the
   485     proofs of two communication protocols which formerly have been here.
   486 
   487     @inproceedings{Nipkow-Slind-IOA,
   488     author={Tobias Nipkow and Konrad Slind},
   489     title={{I/O} Automata in {Isabelle/HOL}},
   490     booktitle={Proc.\ TYPES Workshop 1994},
   491     publisher=Springer,
   492     series=LNCS,
   493     note={To appear}}
   494     ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz
   495 
   496     and
   497 
   498     @inproceedings{Mueller-Nipkow,
   499     author={Olaf M\"uller and Tobias Nipkow},
   500     title={Combining Model Checking and Deduction for {I/O}-Automata},
   501     booktitle={Proc.\ TACAS Workshop},
   502     organization={Aarhus University, BRICS report},
   503     year=1995}
   504     ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz
   505   *}
   506   theories Solve
   507 
   508 session "HOL-Lattice" in Lattice = HOL +
   509   description {*
   510     Author:     Markus Wenzel, TU Muenchen
   511 
   512     Basic theory of lattices and orders.
   513   *}
   514   theories CompleteLattice
   515   document_files "root.tex"
   516 
   517 session "HOL-ex" (timing) in ex = "HOL-Number_Theory" +
   518   description {*
   519     Miscellaneous examples for Higher-Order Logic.
   520   *}
   521   theories
   522     Adhoc_Overloading_Examples
   523     Antiquote
   524     Argo_Examples
   525     Arith_Examples
   526     Ballot
   527     BinEx
   528     Birthday_Paradox
   529     Bit_Lists
   530     Bubblesort
   531     CTL
   532     Cartouche_Examples
   533     Case_Product
   534     Chinese
   535     Classical
   536     Code_Binary_Nat_examples
   537     Code_Lazy_Demo
   538     Code_Timing
   539     Coercion_Examples
   540     Coherent
   541     Commands
   542     Computations
   543     Conditional_Parametricity_Examples
   544     Cubic_Quartic
   545     Datatype_Record_Examples
   546     Dedekind_Real
   547     Erdoes_Szekeres
   548     Eval_Examples
   549     Executable_Relation
   550     Execute_Choice
   551     Functions
   552     Function_Growth
   553     Gauge_Integration
   554     Groebner_Examples
   555     Guess
   556     HarmonicSeries
   557     Hebrew
   558     Hex_Bin_Examples
   559     IArray_Examples
   560     Iff_Oracle
   561     Induction_Schema
   562     Intuitionistic
   563     Lagrange
   564     List_to_Set_Comprehension_Examples
   565     LocaleTest2
   566     "ML"
   567     MergeSort
   568     MonoidGroup
   569     Multiquote
   570     NatSum
   571     Normalization_by_Evaluation
   572     PER
   573     Parallel_Example
   574     Peano_Axioms
   575     Perm_Fragments
   576     PresburgerEx
   577     Primrec
   578     Pythagoras
   579     Quicksort
   580     Radix_Sort
   581     Records
   582     Reflection_Examples
   583     Refute_Examples
   584     Residue_Ring
   585     Rewrite_Examples
   586     SOS
   587     SOS_Cert
   588     Seq
   589     Serbian
   590     Set_Comprehension_Pointfree_Examples
   591     Set_Theory
   592     Simproc_Tests
   593     Simps_Case_Conv_Examples
   594     Sqrt
   595     Sqrt_Script
   596     Sudoku
   597     Sum_of_Powers
   598     Tarski
   599     Termination
   600     ThreeDivides
   601     Transfer_Debug
   602     Transfer_Int_Nat
   603     Transitive_Closure_Table_Ex
   604     Tree23
   605     Unification
   606     While_Combinator_Example
   607     Word_Type
   608     veriT_Preprocessing
   609   theories [skip_proofs = false]
   610     SAT_Examples
   611     Meson_Test
   612 
   613 session "HOL-Isar_Examples" in Isar_Examples = "HOL-Computational_Algebra" +
   614   description {*
   615     Miscellaneous Isabelle/Isar examples.
   616   *}
   617   options [quick_and_dirty]
   618   theories
   619     Knaster_Tarski
   620     Peirce
   621     Drinker
   622     Cantor
   623     Structured_Statements
   624     Basic_Logic
   625     Expr_Compiler
   626     Fibonacci
   627     Group
   628     Group_Context
   629     Group_Notepad
   630     Hoare_Ex
   631     Mutilated_Checkerboard
   632     Puzzle
   633     Summation
   634     First_Order_Logic
   635     Higher_Order_Logic
   636   document_files
   637     "root.bib"
   638     "root.tex"
   639 
   640 session "HOL-Eisbach" in Eisbach = HOL +
   641   description {*
   642     The Eisbach proof method language and "match" method.
   643   *}
   644   sessions
   645     FOL
   646   theories
   647     Eisbach
   648     Tests
   649     Examples
   650     Examples_FOL
   651 
   652 session "HOL-SET_Protocol" (timing) in SET_Protocol = "HOL-Library" +
   653   description {*
   654     Verification of the SET Protocol.
   655   *}
   656   theories
   657     SET_Protocol
   658   document_files "root.tex"
   659 
   660 session "HOL-Matrix_LP" in Matrix_LP = "HOL-Library" +
   661   description {*
   662     Two-dimensional matrices and linear programming.
   663   *}
   664   theories Cplex
   665   document_files "root.tex"
   666 
   667 session "HOL-TLA" in TLA = HOL +
   668   description {*
   669     Lamport's Temporal Logic of Actions.
   670   *}
   671   theories TLA
   672 
   673 session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" +
   674   theories Inc
   675 
   676 session "HOL-TLA-Buffer" in "TLA/Buffer" = "HOL-TLA" +
   677   theories DBuffer
   678 
   679 session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" +
   680   theories MemoryImplementation
   681 
   682 session "HOL-TPTP" in TPTP = "HOL-Library" +
   683   description {*
   684     Author:     Jasmin Blanchette, TU Muenchen
   685     Author:     Nik Sultana, University of Cambridge
   686     Copyright   2011
   687 
   688     TPTP-related extensions.
   689   *}
   690   theories
   691     ATP_Theory_Export
   692     MaSh_Eval
   693     TPTP_Interpret
   694     THF_Arith
   695     TPTP_Proof_Reconstruction
   696   theories
   697     ATP_Problem_Import
   698 
   699 session "HOL-Probability" (main timing) in "Probability" = "HOL-Analysis" +
   700   theories
   701     Probability
   702   document_files "root.tex"
   703 
   704 session "HOL-Probability-ex" (timing) in "Probability/ex" = "HOL-Probability" +
   705   theories
   706     Dining_Cryptographers
   707     Koepf_Duermuth_Countermeasure
   708     Measure_Not_CCC
   709 
   710 session "HOL-Nominal" in Nominal = "HOL-Library" +
   711   theories
   712     Nominal
   713 
   714 session "HOL-Nominal-Examples" (timing) in "Nominal/Examples" = "HOL-Nominal" +
   715   theories
   716     Class3
   717     CK_Machine
   718     Compile
   719     Contexts
   720     Crary
   721     CR_Takahashi
   722     CR
   723     Fsub
   724     Height
   725     Lambda_mu
   726     Lam_Funs
   727     LocalWeakening
   728     Pattern
   729     SN
   730     SOS
   731     Standardization
   732     Support
   733     Type_Preservation
   734     Weakening
   735     W
   736   theories [quick_and_dirty]
   737     VC_Condition
   738 
   739 session "HOL-Cardinals" (timing) in Cardinals = "HOL-Library" +
   740   description {*
   741     Ordinals and Cardinals, Full Theories.
   742   *}
   743   theories
   744     Cardinals
   745     Bounded_Set
   746   document_files
   747     "intro.tex"
   748     "root.tex"
   749     "root.bib"
   750 
   751 session "HOL-Datatype_Examples" (timing) in Datatype_Examples = "HOL-Library" +
   752   description {*
   753     (Co)datatype Examples.
   754   *}
   755   theories
   756     Compat
   757     Lambda_Term
   758     Process
   759     TreeFsetI
   760     "Derivation_Trees/Gram_Lang"
   761     "Derivation_Trees/Parallel_Composition"
   762     Koenig
   763     Lift_BNF
   764     Milner_Tofte
   765     Stream_Processor
   766     Misc_Codatatype
   767     Misc_Datatype
   768     Misc_Primcorec
   769     Misc_Primrec
   770 
   771 session "HOL-Corec_Examples" (timing) in Corec_Examples = "HOL-Library" +
   772   description {*
   773     Corecursion Examples.
   774   *}
   775   theories
   776     LFilter
   777     Paper_Examples
   778     Stream_Processor
   779     "Tests/Simple_Nesting"
   780     "Tests/Iterate_GPV"
   781   theories [quick_and_dirty]
   782     "Tests/GPV_Bare_Bones"
   783     "Tests/Merge_D"
   784     "Tests/Merge_Poly"
   785     "Tests/Misc_Mono"
   786     "Tests/Misc_Poly"
   787     "Tests/Small_Concrete"
   788     "Tests/Stream_Friends"
   789     "Tests/TLList_Friends"
   790     "Tests/Type_Class"
   791 
   792 session "HOL-Word" (main timing) in Word = HOL +
   793   sessions
   794     "HOL-Library"
   795   theories
   796     Word
   797     WordBitwise
   798     Bit_Comparison
   799     WordExamples
   800   document_files "root.bib" "root.tex"
   801 
   802 session "HOL-Statespace" in Statespace = HOL +
   803   theories [skip_proofs = false]
   804     StateSpaceEx
   805   document_files "root.tex"
   806 
   807 session "HOL-Nonstandard_Analysis" (timing) in Nonstandard_Analysis = "HOL-Computational_Algebra" +
   808   description {*
   809     Nonstandard analysis.
   810   *}
   811   theories
   812     Nonstandard_Analysis
   813   document_files "root.tex"
   814 
   815 session "HOL-Nonstandard_Analysis-Examples" (timing) in "Nonstandard_Analysis/Examples" = "HOL-Nonstandard_Analysis" +
   816   theories
   817     NSPrimes
   818 
   819 session "HOL-Mirabelle" in Mirabelle = HOL +
   820   theories Mirabelle_Test
   821 
   822 session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
   823   options [timeout = 60]
   824   theories Ex
   825 
   826 session "HOL-Word-SMT_Examples" (timing) in SMT_Examples = "HOL-Word" +
   827   options [quick_and_dirty]
   828   theories
   829     Boogie
   830     SMT_Examples
   831     SMT_Word_Examples
   832     SMT_Tests
   833 
   834 session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" +
   835   theories
   836     SPARK
   837 
   838 session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
   839   options [spark_prv = false]
   840   theories
   841     "Gcd/Greatest_Common_Divisor"
   842     "Liseq/Longest_Increasing_Subsequence"
   843     "RIPEMD-160/F"
   844     "RIPEMD-160/Hash"
   845     "RIPEMD-160/K_L"
   846     "RIPEMD-160/K_R"
   847     "RIPEMD-160/R_L"
   848     "RIPEMD-160/Round"
   849     "RIPEMD-160/R_R"
   850     "RIPEMD-160/S_L"
   851     "RIPEMD-160/S_R"
   852     "Sqrt/Sqrt"
   853 
   854 session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +
   855   options [show_question_marks = false, spark_prv = false]
   856   sessions
   857     "HOL-SPARK-Examples"
   858   theories
   859     Example_Verification
   860     VC_Principles
   861     Reference
   862     Complex_Types
   863   document_files
   864     "complex_types.ads"
   865     "complex_types_app.adb"
   866     "complex_types_app.ads"
   867     "Gcd.adb"
   868     "Gcd.ads"
   869     "intro.tex"
   870     "loop_invariant.adb"
   871     "loop_invariant.ads"
   872     "root.bib"
   873     "root.tex"
   874     "Simple_Gcd.adb"
   875     "Simple_Gcd.ads"
   876 
   877 session "HOL-Mutabelle" in Mutabelle = "HOL-Library" +
   878   theories MutabelleExtra
   879 
   880 session "HOL-Quickcheck_Examples" (timing) in Quickcheck_Examples = "HOL-Library" +
   881   theories
   882     Quickcheck_Examples
   883     Quickcheck_Lattice_Examples
   884     Completeness
   885     Quickcheck_Interfaces
   886     Quickcheck_Nesting_Example
   887   theories [condition = ISABELLE_GHC]
   888     Hotel_Example
   889     Quickcheck_Narrowing_Examples
   890 
   891 session "HOL-Quotient_Examples" (timing) in Quotient_Examples = "HOL-Algebra" +
   892   description {*
   893     Author:     Cezary Kaliszyk and Christian Urban
   894   *}
   895   theories
   896     DList
   897     Quotient_FSet
   898     Quotient_Int
   899     Quotient_Message
   900     Lift_FSet
   901     Lift_Set
   902     Lift_Fun
   903     Quotient_Rat
   904     Lift_DList
   905     Int_Pow
   906     Lifting_Code_Dt_Test
   907 
   908 session "HOL-Predicate_Compile_Examples" (timing) in Predicate_Compile_Examples = "HOL-Library" +
   909   theories
   910     Examples
   911     Predicate_Compile_Tests
   912     Predicate_Compile_Quickcheck_Examples
   913     Specialisation_Examples
   914     IMP_1
   915     IMP_2
   916     (* FIXME since 21-Jul-2011
   917     Hotel_Example_Small_Generator *)
   918     IMP_3
   919     IMP_4
   920   theories [condition = ISABELLE_SWIPL]
   921     Code_Prolog_Examples
   922     Context_Free_Grammar_Example
   923     Hotel_Example_Prolog
   924     Lambda_Example
   925     List_Examples
   926   theories [condition = ISABELLE_SWIPL, quick_and_dirty]
   927     Reg_Exp_Example
   928 
   929 session "HOL-Types_To_Sets" in Types_To_Sets = HOL +
   930   description {*
   931     Experimental extension of Higher-Order Logic to allow translation of types to sets.
   932   *}
   933   theories
   934     Types_To_Sets
   935     "Examples/Prerequisites"
   936     "Examples/Finite"
   937     "Examples/T2_Spaces"
   938     "Examples/Linear_Algebra_On"
   939 
   940 session HOLCF (main timing) in HOLCF = HOL +
   941   description {*
   942     Author:     Franz Regensburger
   943     Author:     Brian Huffman
   944 
   945     HOLCF -- a semantic extension of HOL by the LCF logic.
   946   *}
   947   sessions
   948     "HOL-Library"
   949   theories
   950     HOLCF (global)
   951   document_files "root.tex"
   952 
   953 session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF +
   954   theories
   955     Domain_ex
   956     Fixrec_ex
   957     New_Domain
   958   document_files "root.tex"
   959 
   960 session "HOLCF-Library" in "HOLCF/Library" = HOLCF +
   961   theories
   962     HOLCF_Library
   963     HOL_Cpo
   964 
   965 session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF +
   966   description {*
   967     IMP -- A WHILE-language and its Semantics.
   968 
   969     This is the HOLCF-based denotational semantics of a simple WHILE-language.
   970   *}
   971   sessions
   972     "HOL-IMP"
   973   theories
   974     HoareEx
   975   document_files
   976     "isaverbatimwrite.sty"
   977     "root.tex"
   978     "root.bib"
   979 
   980 session "HOLCF-ex" in "HOLCF/ex" = "HOLCF-Library" +
   981   description {*
   982     Miscellaneous examples for HOLCF.
   983   *}
   984   theories
   985     Dnat
   986     Dagstuhl
   987     Focus_ex
   988     Fix2
   989     Hoare
   990     Concurrency_Monad
   991     Loop
   992     Powerdomain_ex
   993     Domain_Proofs
   994     Letrec
   995     Pattern_Match
   996 
   997 session "HOLCF-FOCUS" in "HOLCF/FOCUS" = "HOLCF-Library" +
   998   description {*
   999     FOCUS: a theory of stream-processing functions Isabelle/HOLCF.
  1000 
  1001     For introductions to FOCUS, see
  1002 
  1003     "The Design of Distributed Systems - An Introduction to FOCUS"
  1004     http://www4.in.tum.de/publ/html.php?e=2
  1005 
  1006     "Specification and Refinement of a Buffer of Length One"
  1007     http://www4.in.tum.de/publ/html.php?e=15
  1008 
  1009     "Specification and Development of Interactive Systems: Focus on Streams,
  1010     Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321
  1011   *}
  1012   theories
  1013     Fstreams
  1014     FOCUS
  1015     Buffer_adm
  1016 
  1017 session IOA (timing) in "HOLCF/IOA" = HOLCF +
  1018   description {*
  1019     Author:     Olaf Mueller
  1020     Copyright   1997 TU München
  1021 
  1022     A formalization of I/O automata in HOLCF.
  1023 
  1024     The distribution contains simulation relations, temporal logic, and an
  1025     abstraction theory. Everything is based upon a domain-theoretic model of
  1026     finite and infinite sequences.
  1027   *}
  1028   theories Abstraction
  1029 
  1030 session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
  1031   description {*
  1032     Author:     Olaf Mueller
  1033 
  1034     The Alternating Bit Protocol performed in I/O-Automata.
  1035   *}
  1036   theories
  1037     Correctness
  1038     Spec
  1039 
  1040 session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA +
  1041   description {*
  1042     Author:     Tobias Nipkow & Konrad Slind
  1043 
  1044     A network transmission protocol, performed in the
  1045     I/O automata formalization by Olaf Mueller.
  1046   *}
  1047   theories Correctness
  1048 
  1049 session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA +
  1050   description {*
  1051     Author:     Olaf Mueller
  1052 
  1053     Memory storage case study.
  1054   *}
  1055   theories Correctness
  1056 
  1057 session "IOA-ex" in "HOLCF/IOA/ex" = IOA +
  1058   description {*
  1059     Author:     Olaf Mueller
  1060   *}
  1061   theories
  1062     TrivEx
  1063     TrivEx2