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