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