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