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