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