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