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