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