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