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