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