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