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