src/HOL/ROOT
author haftmann
Sun Feb 24 20:29:13 2013 +0100 (2013-02-24)
changeset 51263 31e786e0e6a7
parent 51236 f301ad90c48b
child 51397 03b586ee5930
permissions -rw-r--r--
turned example into library for comparing growth of functions
     1 session HOL (main) = Pure +
     2   description {* Classical Higher-order Logic *}
     3   options [document_graph]
     4   theories Complex_Main
     5   files
     6     "Tools/Quickcheck/Narrowing_Engine.hs"
     7     "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
     8     "document/root.bib"
     9     "document/root.tex"
    10 
    11 session "HOL-Proofs" = Pure +
    12   description {* HOL-Main with explicit proof terms *}
    13   options [document = false, proofs = 2]
    14   theories Main
    15   files
    16     "Tools/Quickcheck/Narrowing_Engine.hs"
    17     "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
    18 
    19 session "HOL-Library" (main) in Library = HOL +
    20   description {* Classical Higher-order Logic -- batteries included *}
    21   theories
    22     Library
    23     (*conflicting type class instantiations*)
    24     List_lexord
    25     Sublist_Order
    26     Product_Lexorder
    27     Product_Order
    28     Finite_Lattice
    29     (*data refinements and dependent applications*)
    30     AList_Mapping
    31     Code_Binary_Nat
    32     Code_Char
    33     (* Code_Prolog  FIXME cf. 76965c356d2a *)
    34     Code_Real_Approx_By_Float
    35     Code_Target_Numeral
    36     DAList
    37     RBT_Mapping
    38     RBT_Set
    39     (*legacy tools*)
    40     Refute
    41     Old_Recdef
    42   theories [condition = ISABELLE_FULL_TEST]
    43     Sum_of_Squares_Remote
    44   files "document/root.bib" "document/root.tex"
    45 
    46 session "HOL-Hahn_Banach" in Hahn_Banach = HOL +
    47   description {*
    48     Author:     Gertrud Bauer, TU Munich
    49 
    50     The Hahn-Banach theorem for real vector spaces.
    51   *}
    52   options [document_graph]
    53   theories Hahn_Banach
    54   files "document/root.bib" "document/root.tex"
    55 
    56 session "HOL-Induct" in Induct = HOL +
    57   theories [quick_and_dirty]
    58     Common_Patterns
    59   theories
    60     QuoDataType
    61     QuoNestedDataType
    62     Term
    63     SList
    64     ABexp
    65     Tree
    66     Ordinals
    67     Sigma_Algebra
    68     Comb
    69     PropLog
    70     Com
    71   files "document/root.tex"
    72 
    73 session "HOL-IMP" in IMP = HOL +
    74   options [document_graph, document_variants=document]
    75   theories [document = false]
    76     "~~/src/HOL/ex/Interpretation_with_Defs"
    77     "~~/src/HOL/Library/While_Combinator"
    78     "~~/src/HOL/Library/Char_ord"
    79     "~~/src/HOL/Library/List_lexord"
    80   theories
    81     BExp
    82     ASM
    83     Finite_Reachable
    84     Denotation
    85     Comp_Rev
    86     Poly_Types
    87     Sec_Typing
    88     Sec_TypingT
    89     Def_Init_Sound_Big
    90     Def_Init_Sound_Small
    91     Live
    92     Live_True
    93     Hoare_Examples
    94     VC
    95     HoareT
    96     Collecting1
    97     Collecting_Examples
    98     Abs_Int_Tests
    99     Abs_Int1_parity
   100     Abs_Int1_const
   101     Abs_Int3
   102     "Abs_Int_ITP/Abs_Int1_parity_ITP"
   103     "Abs_Int_ITP/Abs_Int1_const_ITP"
   104     "Abs_Int_ITP/Abs_Int3_ITP"
   105     "Abs_Int_Den/Abs_Int_den2"
   106     Procs_Dyn_Vars_Dyn
   107     Procs_Stat_Vars_Dyn
   108     Procs_Stat_Vars_Stat
   109     C_like
   110     OO
   111     Fold
   112   files "document/root.bib" "document/root.tex"
   113 
   114 session "HOL-IMPP" in IMPP = HOL +
   115   description {*
   116     Author:     David von Oheimb
   117     Copyright   1999 TUM
   118   *}
   119   options [document = false]
   120   theories EvenOdd
   121 
   122 session "HOL-Import" in Import = HOL +
   123   options [document_graph]
   124   theories HOL_Light_Maps
   125   theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import
   126 
   127 session "HOL-Number_Theory" in Number_Theory = HOL +
   128   options [document = false]
   129   theories Number_Theory
   130 
   131 session "HOL-Old_Number_Theory" in Old_Number_Theory = HOL +
   132   options [document_graph]
   133   theories [document = false]
   134     "~~/src/HOL/Library/Infinite_Set"
   135     "~~/src/HOL/Library/Permutation"
   136   theories
   137     Fib
   138     Factorization
   139     Chinese
   140     WilsonRuss
   141     WilsonBij
   142     Quadratic_Reciprocity
   143     Primes
   144     Pocklington
   145   files "document/root.tex"
   146 
   147 session "HOL-Hoare" in Hoare = HOL +
   148   theories Hoare
   149   files "document/root.bib" "document/root.tex"
   150 
   151 session "HOL-Hoare_Parallel" in Hoare_Parallel = HOL +
   152   options [document_graph]
   153   theories Hoare_Parallel
   154   files "document/root.bib" "document/root.tex"
   155 
   156 session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" +
   157   options [document = false, document_graph = false, browser_info = false]
   158   theories Generate Generate_Binary_Nat Generate_Target_Nat Generate_Efficient_Datastructures Generate_Pretty_Char
   159 
   160 session "HOL-Metis_Examples" in Metis_Examples = HOL +
   161   description {*
   162     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   163     Author:     Jasmin Blanchette, TU Muenchen
   164 
   165     Testing Metis and Sledgehammer.
   166   *}
   167   options [timeout = 3600, document = false]
   168   theories
   169     Abstraction
   170     Big_O
   171     Binary_Tree
   172     Clausification
   173     Message
   174     Proxies
   175     Tarski
   176     Trans_Closure
   177     Sets
   178 
   179 session "HOL-Nitpick_Examples" in Nitpick_Examples = HOL +
   180   description {*
   181     Author:     Jasmin Blanchette, TU Muenchen
   182     Copyright   2009
   183   *}
   184   options [document = false]
   185   theories [quick_and_dirty] Nitpick_Examples
   186 
   187 session "HOL-Algebra" (main) in Algebra = HOL +
   188   description {*
   189     Author: Clemens Ballarin, started 24 September 1999
   190 
   191     The Isabelle Algebraic Library.
   192   *}
   193   options [document_graph]
   194   theories [document = false]
   195     (* Preliminaries from set and number theory *)
   196     "~~/src/HOL/Library/FuncSet"
   197     "~~/src/HOL/Old_Number_Theory/Primes"
   198     "~~/src/HOL/Library/Binomial"
   199     "~~/src/HOL/Library/Permutation"
   200   theories
   201     (*** New development, based on explicit structures ***)
   202     (* Groups *)
   203     FiniteProduct        (* Product operator for commutative groups *)
   204     Sylow                (* Sylow's theorem *)
   205     Bij                  (* Automorphism Groups *)
   206 
   207     (* Rings *)
   208     Divisibility         (* Rings *)
   209     IntRing              (* Ideals and residue classes *)
   210     UnivPoly             (* Polynomials *)
   211   theories [document = false]
   212     (*** Old development, based on axiomatic type classes ***)
   213     "abstract/Abstract"  (*The ring theory*)
   214     "poly/Polynomial"    (*The full theory*)
   215   files "document/root.bib" "document/root.tex"
   216 
   217 session "HOL-Auth" in Auth = HOL +
   218   options [document_graph]
   219   theories
   220     Auth_Shared
   221     Auth_Public
   222     "Smartcard/Auth_Smartcard"
   223     "Guard/Auth_Guard_Shared"
   224     "Guard/Auth_Guard_Public"
   225   files "document/root.tex"
   226 
   227 session "HOL-UNITY" in UNITY = "HOL-Auth" +
   228   description {*
   229     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   230     Copyright   1998  University of Cambridge
   231 
   232     Verifying security protocols using UNITY.
   233   *}
   234   options [document_graph]
   235   theories
   236     (*Basic meta-theory*)
   237     "UNITY_Main"
   238 
   239     (*Simple examples: no composition*)
   240     "Simple/Deadlock"
   241     "Simple/Common"
   242     "Simple/Network"
   243     "Simple/Token"
   244     "Simple/Channel"
   245     "Simple/Lift"
   246     "Simple/Mutex"
   247     "Simple/Reach"
   248     "Simple/Reachability"
   249 
   250     (*Verifying security protocols using UNITY*)
   251     "Simple/NSP_Bad"
   252 
   253     (*Example of composition*)
   254     "Comp/Handshake"
   255 
   256     (*Universal properties examples*)
   257     "Comp/Counter"
   258     "Comp/Counterc"
   259     "Comp/Priority"
   260 
   261     "Comp/TimerArray"
   262     "Comp/Progress"
   263 
   264     "Comp/Alloc"
   265     "Comp/AllocImpl"
   266     "Comp/Client"
   267 
   268     (*obsolete*)
   269     "ELT"
   270   files "document/root.tex"
   271 
   272 session "HOL-Unix" in Unix = HOL +
   273   options [print_mode = "no_brackets,no_type_brackets"]
   274   theories Unix
   275   files "document/root.bib" "document/root.tex"
   276 
   277 session "HOL-ZF" in ZF = HOL +
   278   theories MainZF Games
   279   files "document/root.tex"
   280 
   281 session "HOL-Imperative_HOL" in Imperative_HOL = HOL +
   282   options [document_graph, print_mode = "iff,no_brackets"]
   283   theories [document = false]
   284     "~~/src/HOL/Library/Countable"
   285     "~~/src/HOL/Library/Monad_Syntax"
   286     "~~/src/HOL/Library/LaTeXsugar"
   287   theories Imperative_HOL_ex
   288   files "document/root.bib" "document/root.tex"
   289 
   290 session "HOL-Decision_Procs" in Decision_Procs = HOL +
   291   options [condition = ISABELLE_POLYML, document = false]
   292   theories Decision_Procs
   293 
   294 session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
   295   options [document = false, proofs = 2, parallel_proofs = 0]
   296   theories Hilbert_Classical
   297 
   298 session "HOL-Proofs-Extraction" in "Proofs/Extraction" = "HOL-Proofs" +
   299   description {* Examples for program extraction in Higher-Order Logic *}
   300   options [condition = ISABELLE_POLYML, proofs = 2, parallel_proofs = 0]
   301   theories [document = false]
   302     "~~/src/HOL/Library/Code_Target_Numeral"
   303     "~~/src/HOL/Library/Monad_Syntax"
   304     "~~/src/HOL/Number_Theory/Primes"
   305     "~~/src/HOL/Number_Theory/UniqueFactorization"
   306     "~~/src/HOL/Library/State_Monad"
   307   theories
   308     Greatest_Common_Divisor
   309     Warshall
   310     Higman_Extraction
   311     Pigeonhole
   312     Euclid
   313   files "document/root.bib" "document/root.tex"
   314 
   315 session "HOL-Proofs-Lambda" in "Proofs/Lambda" = "HOL-Proofs" +
   316   options [document_graph, print_mode = "no_brackets", proofs = 2, parallel_proofs = 0]
   317   theories [document = false]
   318     "~~/src/HOL/Library/Code_Target_Int"
   319   theories
   320     Eta
   321     StrongNorm
   322     Standardization
   323     WeakNorm
   324   files "document/root.bib" "document/root.tex"
   325 
   326 session "HOL-Prolog" in Prolog = HOL +
   327   description {*
   328     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
   329   *}
   330   options [document = false]
   331   theories Test Type
   332 
   333 session "HOL-MicroJava" in MicroJava = HOL +
   334   options [document_graph]
   335   theories [document = false] "~~/src/HOL/Library/While_Combinator"
   336   theories MicroJava
   337   files
   338     "document/introduction.tex"
   339     "document/root.bib"
   340     "document/root.tex"
   341 
   342 session "HOL-MicroJava-skip_proofs" in MicroJava = HOL +
   343   options [condition = ISABELLE_FULL_TEST, document = false, skip_proofs, quick_and_dirty]
   344   theories MicroJava
   345 
   346 session "HOL-NanoJava" in NanoJava = HOL +
   347   options [document_graph]
   348   theories Example
   349   files "document/root.bib" "document/root.tex"
   350 
   351 session "HOL-Bali" in Bali = HOL +
   352   options [document_graph]
   353   theories
   354     AxExample
   355     AxSound
   356     AxCompl
   357     Trans
   358   files "document/root.tex"
   359 
   360 session "HOL-IOA" in IOA = HOL +
   361   description {*
   362     Author:     Tobias Nipkow & Konrad Slind
   363     Copyright   1994  TU Muenchen
   364 
   365     The meta theory of I/O-Automata.
   366 
   367     @inproceedings{Nipkow-Slind-IOA,
   368     author={Tobias Nipkow and Konrad Slind},
   369     title={{I/O} Automata in {Isabelle/HOL}},
   370     booktitle={Proc.\ TYPES Workshop 1994},
   371     publisher=Springer,
   372     series=LNCS,
   373     note={To appear}}
   374     ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz
   375 
   376     and
   377 
   378     @inproceedings{Mueller-Nipkow,
   379     author={Olaf M\"uller and Tobias Nipkow},
   380     title={Combining Model Checking and Deduction for {I/O}-Automata},
   381     booktitle={Proc.\ TACAS Workshop},
   382     organization={Aarhus University, BRICS report},
   383     year=1995}
   384     ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz
   385   *}
   386   options [document = false]
   387   theories Solve
   388 
   389 session "HOL-Lattice" in Lattice = HOL +
   390   description {*
   391     Author:     Markus Wenzel, TU Muenchen
   392 
   393     Basic theory of lattices and orders.
   394   *}
   395   theories CompleteLattice
   396   files "document/root.tex"
   397 
   398 session "HOL-ex" in ex = HOL +
   399   description {* Miscellaneous examples for Higher-Order Logic. *}
   400   options [timeout = 3600, condition = ISABELLE_POLYML]
   401   theories [document = false]
   402     "~~/src/HOL/Library/State_Monad"
   403     Code_Binary_Nat_examples
   404     "~~/src/HOL/Library/FuncSet"
   405     Eval_Examples
   406     Normalization_by_Evaluation
   407     Hebrew
   408     Chinese
   409     Serbian
   410     "~~/src/HOL/Library/FinFun_Syntax"
   411     "~~/src/HOL/Library/Refute"
   412   theories
   413     Iff_Oracle
   414     Coercion_Examples
   415     Numeral_Representation
   416     Higher_Order_Logic
   417     Abstract_NAT
   418     Guess
   419     Binary
   420     Fundefs
   421     Induction_Schema
   422     LocaleTest2
   423     Records
   424     While_Combinator_Example
   425     MonoidGroup
   426     BinEx
   427     Hex_Bin_Examples
   428     Antiquote
   429     Multiquote
   430     PER
   431     NatSum
   432     ThreeDivides
   433     Intuitionistic
   434     CTL
   435     Arith_Examples
   436     BT
   437     Tree23
   438     MergeSort
   439     Lagrange
   440     Groebner_Examples
   441     MT
   442     Unification
   443     Primrec
   444     Tarski
   445     Classical
   446     Set_Theory
   447     Meson_Test
   448     Termination
   449     Coherent
   450     PresburgerEx
   451     Reflection_Examples
   452     Sqrt
   453     Sqrt_Script
   454     Transfer_Ex
   455     Transfer_Int_Nat
   456     HarmonicSeries
   457     Refute_Examples
   458     Execute_Choice
   459     Summation
   460     Gauge_Integration
   461     Dedekind_Real
   462     Quicksort
   463     Birthday_Paradox
   464     List_to_Set_Comprehension_Examples
   465     Seq
   466     Simproc_Tests
   467     Executable_Relation
   468     FinFunPred
   469     Set_Comprehension_Pointfree_Tests
   470     Parallel_Example
   471     IArray_Examples
   472   theories SVC_Oracle
   473   theories [condition = SVC_HOME]
   474     svc_test
   475   theories [condition = ZCHAFF_HOME]
   476     (*requires zChaff (or some other reasonably fast SAT solver)*)
   477     Sudoku
   478 (* FIXME
   479 (*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
   480 (*global side-effects ahead!*)
   481 try use_thy "SAT_Examples";   (* FIXME try!? (not really a proper test) *)
   482 *)
   483   files "document/root.bib" "document/root.tex"
   484 
   485 session "HOL-Isar_Examples" in Isar_Examples = HOL +
   486   description {* Miscellaneous Isabelle/Isar examples for Higher-Order Logic. *}
   487   theories [document = false]
   488     "~~/src/HOL/Library/Lattice_Syntax"
   489     "../Number_Theory/Primes"
   490   theories
   491     Basic_Logic
   492     Cantor
   493     Drinker
   494     Expr_Compiler
   495     Fibonacci
   496     Group
   497     Group_Context
   498     Group_Notepad
   499     Hoare_Ex
   500     Knaster_Tarski
   501     Mutilated_Checkerboard
   502     Nested_Datatype
   503     Peirce
   504     Puzzle
   505     Summation
   506   files
   507     "document/root.bib"
   508     "document/root.tex"
   509     "document/style.tex"
   510 
   511 session "HOL-SET_Protocol" in SET_Protocol = HOL +
   512   options [document_graph]
   513   theories [document = false] "~~/src/HOL/Library/Nat_Bijection"
   514   theories SET_Protocol
   515   files "document/root.tex"
   516 
   517 session "HOL-Matrix_LP" in Matrix_LP = HOL +
   518   options [document_graph]
   519   theories Cplex
   520   files "document/root.tex"
   521 
   522 session "HOL-TLA" in TLA = HOL +
   523   description {* The Temporal Logic of Actions *}
   524   options [document = false]
   525   theories TLA
   526 
   527 session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" +
   528   options [document = false]
   529   theories Inc
   530 
   531 session "HOL-TLA-Buffer" in "TLA/Buffer" = "HOL-TLA" +
   532   options [document = false]
   533   theories DBuffer
   534 
   535 session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" +
   536   options [document = false]
   537   theories MemoryImplementation
   538 
   539 session "HOL-TPTP" in TPTP = HOL +
   540   description {*
   541     Author:     Jasmin Blanchette, TU Muenchen
   542     Author:     Nik Sultana, University of Cambridge
   543     Copyright   2011
   544 
   545     TPTP-related extensions.
   546   *}
   547   options [document = false]
   548   theories
   549     ATP_Theory_Export
   550     MaSh_Eval
   551     MaSh_Export
   552     TPTP_Interpret
   553     THF_Arith
   554   theories [proofs = 0]  (* FIXME !? *)
   555     ATP_Problem_Import
   556 
   557 session "HOL-Multivariate_Analysis" (main) in Multivariate_Analysis = HOL +
   558   options [document_graph]
   559   theories
   560     Multivariate_Analysis
   561     Determinants
   562   files
   563     "document/root.tex"
   564 
   565 session "HOL-Probability" in "Probability" = "HOL-Multivariate_Analysis" +
   566   options [document_graph]
   567   theories [document = false]
   568     "~~/src/HOL/Library/Countable"
   569     "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits"
   570     "~~/src/HOL/Library/Permutation"
   571   theories
   572     Probability
   573     "ex/Dining_Cryptographers"
   574     "ex/Koepf_Duermuth_Countermeasure"
   575   files "document/root.tex"
   576 
   577 session "HOL-Nominal" (main) in Nominal = HOL +
   578   options [document = false]
   579   theories Nominal
   580 
   581 session "HOL-Nominal-Examples" in "Nominal/Examples" = "HOL-Nominal" +
   582   options [timeout = 3600, condition = ISABELLE_POLYML, document = false]
   583   theories Nominal_Examples
   584   theories [quick_and_dirty] VC_Condition
   585 
   586 session "HOL-Cardinals-Base" in Cardinals = HOL +
   587   description {* Ordinals and Cardinals, Base Theories *}
   588   options [document = false]
   589   theories Cardinal_Arithmetic
   590 
   591 session "HOL-Cardinals" in Cardinals = "HOL-Cardinals-Base" +
   592   description {* Ordinals and Cardinals, Full Theories *}
   593   options [document = false]
   594   theories Cardinals
   595   files
   596     "document/intro.tex"
   597     "document/root.tex"
   598     "document/root.bib"
   599 
   600 session "HOL-BNF-LFP" in BNF = "HOL-Cardinals-Base" +
   601   description {* Bounded Natural Functors for Datatypes *}
   602   options [document = false]
   603   theories BNF_LFP
   604 
   605 session "HOL-BNF" in BNF = "HOL-Cardinals" +
   606   description {* Bounded Natural Functors for (Co)datatypes *}
   607   options [document = false]
   608   theories BNF
   609 
   610 session "HOL-BNF-Examples" in "BNF/Examples" = "HOL-BNF" +
   611   description {* Examples for Bounded Natural Functors *}
   612   options [document = false]
   613   theories
   614     Lambda_Term
   615     Process
   616     TreeFsetI
   617     "Derivation_Trees/Gram_Lang"
   618     "Derivation_Trees/Parallel"
   619     Koenig
   620   theories [condition = ISABELLE_FULL_TEST]
   621     Misc_Codata
   622     Misc_Data
   623 
   624 session "HOL-Word" (main) in Word = HOL +
   625   options [document_graph]
   626   theories Word
   627   files "document/root.bib" "document/root.tex"
   628 
   629 session "HOL-Word-Examples" in "Word/Examples" = "HOL-Word" +
   630   options [document = false]
   631   theories WordExamples
   632 
   633 session "HOL-Statespace" in Statespace = HOL +
   634   theories StateSpaceEx
   635   files "document/root.tex"
   636 
   637 session "HOL-NSA" in NSA = HOL +
   638   options [document_graph]
   639   theories Hypercomplex
   640   files "document/root.tex"
   641 
   642 session "HOL-NSA-Examples" in "NSA/Examples" = "HOL-NSA" +
   643   options [document = false]
   644   theories NSPrimes
   645 
   646 session "HOL-Mirabelle" in Mirabelle = HOL +
   647   options [document = false]
   648   theories Mirabelle_Test
   649 
   650 session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
   651   options [document = false, timeout = 60]
   652   theories Ex
   653 
   654 session "HOL-Word-SMT_Examples" in SMT_Examples = "HOL-Word" +
   655   options [document = false, quick_and_dirty]
   656   theories
   657     SMT_Examples
   658     SMT_Word_Examples
   659   theories [condition = ISABELLE_FULL_TEST]
   660     SMT_Tests
   661   files
   662     "SMT_Examples.certs"
   663     "SMT_Word_Examples.certs"
   664 
   665 session "HOL-Boogie" in "Boogie" = "HOL-Word" +
   666   options [document = false]
   667   theories Boogie
   668 
   669 session "HOL-Boogie-Examples" in "Boogie/Examples" = "HOL-Boogie" +
   670   options [document = false]
   671   theories
   672     Boogie_Max_Stepwise
   673     Boogie_Max
   674     Boogie_Dijkstra
   675     VCC_Max
   676   files
   677     "Boogie_Dijkstra.b2i"
   678     "Boogie_Dijkstra.certs"
   679     "Boogie_Max.b2i"
   680     "Boogie_Max.certs"
   681     "VCC_Max.b2i"
   682     "VCC_Max.certs"
   683 
   684 session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" +
   685   options [document = false]
   686   theories SPARK
   687 
   688 session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
   689   options [document = false]
   690   theories
   691     "Gcd/Greatest_Common_Divisor"
   692 
   693     "Liseq/Longest_Increasing_Subsequence"
   694 
   695     "RIPEMD-160/F"
   696     "RIPEMD-160/Hash"
   697     "RIPEMD-160/K_L"
   698     "RIPEMD-160/K_R"
   699     "RIPEMD-160/R_L"
   700     "RIPEMD-160/Round"
   701     "RIPEMD-160/R_R"
   702     "RIPEMD-160/S_L"
   703     "RIPEMD-160/S_R"
   704 
   705     "Sqrt/Sqrt"
   706   files
   707     "Gcd/greatest_common_divisor/g_c_d.fdl"
   708     "Gcd/greatest_common_divisor/g_c_d.rls"
   709     "Gcd/greatest_common_divisor/g_c_d.siv"
   710     "Liseq/liseq/liseq_length.fdl"
   711     "Liseq/liseq/liseq_length.rls"
   712     "Liseq/liseq/liseq_length.siv"
   713     "RIPEMD-160/rmd/f.fdl"
   714     "RIPEMD-160/rmd/f.rls"
   715     "RIPEMD-160/rmd/f.siv"
   716     "RIPEMD-160/rmd/hash.fdl"
   717     "RIPEMD-160/rmd/hash.rls"
   718     "RIPEMD-160/rmd/hash.siv"
   719     "RIPEMD-160/rmd/k_l.fdl"
   720     "RIPEMD-160/rmd/k_l.rls"
   721     "RIPEMD-160/rmd/k_l.siv"
   722     "RIPEMD-160/rmd/k_r.fdl"
   723     "RIPEMD-160/rmd/k_r.rls"
   724     "RIPEMD-160/rmd/k_r.siv"
   725     "RIPEMD-160/rmd/r_l.fdl"
   726     "RIPEMD-160/rmd/r_l.rls"
   727     "RIPEMD-160/rmd/r_l.siv"
   728     "RIPEMD-160/rmd/round.fdl"
   729     "RIPEMD-160/rmd/round.rls"
   730     "RIPEMD-160/rmd/round.siv"
   731     "RIPEMD-160/rmd/r_r.fdl"
   732     "RIPEMD-160/rmd/r_r.rls"
   733     "RIPEMD-160/rmd/r_r.siv"
   734     "RIPEMD-160/rmd/s_l.fdl"
   735     "RIPEMD-160/rmd/s_l.rls"
   736     "RIPEMD-160/rmd/s_l.siv"
   737     "RIPEMD-160/rmd/s_r.fdl"
   738     "RIPEMD-160/rmd/s_r.rls"
   739     "RIPEMD-160/rmd/s_r.siv"
   740 
   741 session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +
   742   options [show_question_marks = false]
   743   theories
   744     Example_Verification
   745     VC_Principles
   746     Reference
   747     Complex_Types
   748   files
   749     "complex_types_app/initialize.fdl"
   750     "complex_types_app/initialize.rls"
   751     "complex_types_app/initialize.siv"
   752     "document/complex_types.ads"
   753     "document/complex_types_app.adb"
   754     "document/complex_types_app.ads"
   755     "document/Gcd.adb"
   756     "document/Gcd.ads"
   757     "document/intro.tex"
   758     "document/loop_invariant.adb"
   759     "document/loop_invariant.ads"
   760     "document/root.bib"
   761     "document/root.tex"
   762     "document/Simple_Gcd.adb"
   763     "document/Simple_Gcd.ads"
   764     "loop_invariant/proc1.fdl"
   765     "loop_invariant/proc1.rls"
   766     "loop_invariant/proc1.siv"
   767     "loop_invariant/proc2.fdl"
   768     "loop_invariant/proc2.rls"
   769     "loop_invariant/proc2.siv"
   770     "simple_greatest_common_divisor/g_c_d.fdl"
   771     "simple_greatest_common_divisor/g_c_d.rls"
   772     "simple_greatest_common_divisor/g_c_d.siv"
   773 
   774 session "HOL-Mutabelle" in Mutabelle = HOL +
   775   options [document = false]
   776   theories MutabelleExtra
   777 
   778 session "HOL-Quickcheck_Examples" in Quickcheck_Examples = HOL +
   779   options [document = false]
   780   theories
   781     Quickcheck_Examples
   782   (* FIXME
   783     Quickcheck_Lattice_Examples
   784     Completeness
   785     Quickcheck_Interfaces
   786     Hotel_Example *)
   787   theories [condition = ISABELLE_GHC]
   788     Quickcheck_Narrowing_Examples
   789 
   790 session "HOL-Quickcheck_Benchmark" in Quickcheck_Benchmark = HOL +
   791   theories [condition = ISABELLE_FULL_TEST, quick_and_dirty]
   792     Find_Unused_Assms_Examples
   793     Needham_Schroeder_No_Attacker_Example
   794     Needham_Schroeder_Guided_Attacker_Example
   795     Needham_Schroeder_Unguided_Attacker_Example
   796 
   797 session "HOL-Quotient_Examples" in Quotient_Examples = HOL +
   798   description {*
   799     Author:     Cezary Kaliszyk and Christian Urban
   800   *}
   801   options [document = false]
   802   theories
   803     DList
   804     FSet
   805     Quotient_Int
   806     Quotient_Message
   807     Lift_FSet
   808     Lift_Set
   809     Lift_Fun
   810     Quotient_Rat
   811     Lift_DList
   812 
   813 session "HOL-Predicate_Compile_Examples" in Predicate_Compile_Examples = HOL +
   814   options [document = false]
   815   theories
   816     Examples
   817     Predicate_Compile_Tests
   818     (* FIXME
   819     Predicate_Compile_Quickcheck_Examples  -- should be added again soon (since 21-Oct-2010) *)
   820     Specialisation_Examples
   821     (* FIXME since 21-Jul-2011
   822     Hotel_Example_Small_Generator
   823     IMP_1
   824     IMP_2
   825     IMP_3
   826     IMP_4 *)
   827   theories [condition = "ISABELLE_SWIPL"]  (* FIXME: *or* ISABELLE_YAP (??) *)
   828     Code_Prolog_Examples
   829     Context_Free_Grammar_Example
   830     Hotel_Example_Prolog
   831     Lambda_Example
   832     List_Examples
   833   theories [condition = "ISABELLE_SWIPL", quick_and_dirty]  (* FIXME: *or* ISABELLE_YAP (??) *)
   834     Reg_Exp_Example
   835 
   836 session HOLCF (main) in HOLCF = HOL +
   837   description {*
   838     Author:     Franz Regensburger
   839     Author:     Brian Huffman
   840 
   841     HOLCF -- a semantic extension of HOL by the LCF logic.
   842   *}
   843   options [document_graph]
   844   theories [document = false]
   845     "~~/src/HOL/Library/Nat_Bijection"
   846     "~~/src/HOL/Library/Countable"
   847   theories
   848     Plain_HOLCF
   849     Fixrec
   850     HOLCF
   851   files "document/root.tex"
   852 
   853 session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF +
   854   theories
   855     Domain_ex
   856     Fixrec_ex
   857     New_Domain
   858   files "document/root.tex"
   859 
   860 session "HOLCF-Library" in "HOLCF/Library" = HOLCF +
   861   options [document = false]
   862   theories HOLCF_Library
   863 
   864 session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF +
   865   options [document = false]
   866   theories HoareEx
   867   files "document/root.tex"
   868 
   869 session "HOLCF-ex" in "HOLCF/ex" = HOLCF +
   870   description {* Misc HOLCF examples *}
   871   options [document = false]
   872   theories
   873     Dnat
   874     Dagstuhl
   875     Focus_ex
   876     Fix2
   877     Hoare
   878     Concurrency_Monad
   879     Loop
   880     Powerdomain_ex
   881     Domain_Proofs
   882     Letrec
   883     Pattern_Match
   884 
   885 session "HOLCF-FOCUS" in "HOLCF/FOCUS" = HOLCF +
   886   options [document = false]
   887   theories
   888     Fstreams
   889     FOCUS
   890     Buffer_adm
   891 
   892 session IOA in "HOLCF/IOA" = HOLCF +
   893   description {*
   894     Author:     Olaf Mueller
   895 
   896     Formalization of a semantic model of I/O-Automata.
   897   *}
   898   options [document = false]
   899   theories "meta_theory/Abstraction"
   900 
   901 session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
   902   description {*
   903     Author:     Olaf Mueller
   904 
   905     The Alternating Bit Protocol performed in I/O-Automata.
   906   *}
   907   options [document = false]
   908   theories Correctness
   909 
   910 session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA +
   911   description {*
   912     Author:     Tobias Nipkow & Konrad Slind
   913 
   914     A network transmission protocol, performed in the
   915     I/O automata formalization by Olaf Mueller.
   916   *}
   917   options [document = false]
   918   theories Correctness
   919 
   920 session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA +
   921   description {*
   922     Author:     Olaf Mueller
   923 
   924     Memory storage case study.
   925   *}
   926   options [document = false]
   927   theories Correctness
   928 
   929 session "IOA-ex" in "HOLCF/IOA/ex" = IOA +
   930   description {*
   931     Author:     Olaf Mueller
   932   *}
   933   options [document = false]
   934   theories
   935     TrivEx
   936     TrivEx2
   937 
   938 session "HOL-Datatype_Benchmark" in Datatype_Benchmark = HOL +
   939   description {* Some rather large datatype examples (from John Harrison). *}
   940   options [document = false]
   941   theories [condition = ISABELLE_FULL_TEST, timing]
   942     Brackin
   943     Instructions
   944     SML
   945     Verilog
   946 
   947 session "HOL-Record_Benchmark" in Record_Benchmark = HOL +
   948   description {* Some benchmark on large record. *}
   949   options [document = false]
   950   theories [condition = ISABELLE_FULL_TEST, timing]
   951     Record_Benchmark
   952