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