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