src/HOL/ROOT
author wenzelm
Thu Feb 21 18:21:40 2013 +0100 (2013-02-21)
changeset 51236 f301ad90c48b
parent 51161 6ed12ae3b3e1
child 51263 31e786e0e6a7
permissions -rw-r--r--
more explicit session dependency, for improved parallel performance of HOL-UNITY test session -- NB: separate 'theories' sections are sequential;
     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     Landau
   459     Execute_Choice
   460     Summation
   461     Gauge_Integration
   462     Dedekind_Real
   463     Quicksort
   464     Birthday_Paradox
   465     List_to_Set_Comprehension_Examples
   466     Seq
   467     Simproc_Tests
   468     Executable_Relation
   469     FinFunPred
   470     Set_Comprehension_Pointfree_Tests
   471     Parallel_Example
   472     IArray_Examples
   473   theories SVC_Oracle
   474   theories [condition = SVC_HOME]
   475     svc_test
   476   theories [condition = ZCHAFF_HOME]
   477     (*requires zChaff (or some other reasonably fast SAT solver)*)
   478     Sudoku
   479 (* FIXME
   480 (*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
   481 (*global side-effects ahead!*)
   482 try use_thy "SAT_Examples";   (* FIXME try!? (not really a proper test) *)
   483 *)
   484   files "document/root.bib" "document/root.tex"
   485 
   486 session "HOL-Isar_Examples" in Isar_Examples = HOL +
   487   description {* Miscellaneous Isabelle/Isar examples for Higher-Order Logic. *}
   488   theories [document = false]
   489     "~~/src/HOL/Library/Lattice_Syntax"
   490     "../Number_Theory/Primes"
   491   theories
   492     Basic_Logic
   493     Cantor
   494     Drinker
   495     Expr_Compiler
   496     Fibonacci
   497     Group
   498     Group_Context
   499     Group_Notepad
   500     Hoare_Ex
   501     Knaster_Tarski
   502     Mutilated_Checkerboard
   503     Nested_Datatype
   504     Peirce
   505     Puzzle
   506     Summation
   507   files
   508     "document/root.bib"
   509     "document/root.tex"
   510     "document/style.tex"
   511 
   512 session "HOL-SET_Protocol" in SET_Protocol = HOL +
   513   options [document_graph]
   514   theories [document = false] "~~/src/HOL/Library/Nat_Bijection"
   515   theories SET_Protocol
   516   files "document/root.tex"
   517 
   518 session "HOL-Matrix_LP" in Matrix_LP = HOL +
   519   options [document_graph]
   520   theories Cplex
   521   files "document/root.tex"
   522 
   523 session "HOL-TLA" in TLA = HOL +
   524   description {* The Temporal Logic of Actions *}
   525   options [document = false]
   526   theories TLA
   527 
   528 session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" +
   529   options [document = false]
   530   theories Inc
   531 
   532 session "HOL-TLA-Buffer" in "TLA/Buffer" = "HOL-TLA" +
   533   options [document = false]
   534   theories DBuffer
   535 
   536 session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" +
   537   options [document = false]
   538   theories MemoryImplementation
   539 
   540 session "HOL-TPTP" in TPTP = HOL +
   541   description {*
   542     Author:     Jasmin Blanchette, TU Muenchen
   543     Author:     Nik Sultana, University of Cambridge
   544     Copyright   2011
   545 
   546     TPTP-related extensions.
   547   *}
   548   options [document = false]
   549   theories
   550     ATP_Theory_Export
   551     MaSh_Eval
   552     MaSh_Export
   553     TPTP_Interpret
   554     THF_Arith
   555   theories [proofs = 0]  (* FIXME !? *)
   556     ATP_Problem_Import
   557 
   558 session "HOL-Multivariate_Analysis" (main) in Multivariate_Analysis = HOL +
   559   options [document_graph]
   560   theories
   561     Multivariate_Analysis
   562     Determinants
   563   files
   564     "document/root.tex"
   565 
   566 session "HOL-Probability" in "Probability" = "HOL-Multivariate_Analysis" +
   567   options [document_graph]
   568   theories [document = false]
   569     "~~/src/HOL/Library/Countable"
   570     "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits"
   571     "~~/src/HOL/Library/Permutation"
   572   theories
   573     Probability
   574     "ex/Dining_Cryptographers"
   575     "ex/Koepf_Duermuth_Countermeasure"
   576   files "document/root.tex"
   577 
   578 session "HOL-Nominal" (main) in Nominal = HOL +
   579   options [document = false]
   580   theories Nominal
   581 
   582 session "HOL-Nominal-Examples" in "Nominal/Examples" = "HOL-Nominal" +
   583   options [timeout = 3600, condition = ISABELLE_POLYML, document = false]
   584   theories Nominal_Examples
   585   theories [quick_and_dirty] VC_Condition
   586 
   587 session "HOL-Cardinals-Base" in Cardinals = HOL +
   588   description {* Ordinals and Cardinals, Base Theories *}
   589   options [document = false]
   590   theories Cardinal_Arithmetic
   591 
   592 session "HOL-Cardinals" in Cardinals = "HOL-Cardinals-Base" +
   593   description {* Ordinals and Cardinals, Full Theories *}
   594   options [document = false]
   595   theories Cardinals
   596   files
   597     "document/intro.tex"
   598     "document/root.tex"
   599     "document/root.bib"
   600 
   601 session "HOL-BNF-LFP" in BNF = "HOL-Cardinals-Base" +
   602   description {* Bounded Natural Functors for Datatypes *}
   603   options [document = false]
   604   theories BNF_LFP
   605 
   606 session "HOL-BNF" in BNF = "HOL-Cardinals" +
   607   description {* Bounded Natural Functors for (Co)datatypes *}
   608   options [document = false]
   609   theories BNF
   610 
   611 session "HOL-BNF-Examples" in "BNF/Examples" = "HOL-BNF" +
   612   description {* Examples for Bounded Natural Functors *}
   613   options [document = false]
   614   theories
   615     Lambda_Term
   616     Process
   617     TreeFsetI
   618     "Derivation_Trees/Gram_Lang"
   619     "Derivation_Trees/Parallel"
   620     Koenig
   621   theories [condition = ISABELLE_FULL_TEST]
   622     Misc_Codata
   623     Misc_Data
   624 
   625 session "HOL-Word" (main) in Word = HOL +
   626   options [document_graph]
   627   theories Word
   628   files "document/root.bib" "document/root.tex"
   629 
   630 session "HOL-Word-Examples" in "Word/Examples" = "HOL-Word" +
   631   options [document = false]
   632   theories WordExamples
   633 
   634 session "HOL-Statespace" in Statespace = HOL +
   635   theories StateSpaceEx
   636   files "document/root.tex"
   637 
   638 session "HOL-NSA" in NSA = HOL +
   639   options [document_graph]
   640   theories Hypercomplex
   641   files "document/root.tex"
   642 
   643 session "HOL-NSA-Examples" in "NSA/Examples" = "HOL-NSA" +
   644   options [document = false]
   645   theories NSPrimes
   646 
   647 session "HOL-Mirabelle" in Mirabelle = HOL +
   648   options [document = false]
   649   theories Mirabelle_Test
   650 
   651 session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
   652   options [document = false, timeout = 60]
   653   theories Ex
   654 
   655 session "HOL-Word-SMT_Examples" in SMT_Examples = "HOL-Word" +
   656   options [document = false, quick_and_dirty]
   657   theories
   658     SMT_Examples
   659     SMT_Word_Examples
   660   theories [condition = ISABELLE_FULL_TEST]
   661     SMT_Tests
   662   files
   663     "SMT_Examples.certs"
   664     "SMT_Word_Examples.certs"
   665 
   666 session "HOL-Boogie" in "Boogie" = "HOL-Word" +
   667   options [document = false]
   668   theories Boogie
   669 
   670 session "HOL-Boogie-Examples" in "Boogie/Examples" = "HOL-Boogie" +
   671   options [document = false]
   672   theories
   673     Boogie_Max_Stepwise
   674     Boogie_Max
   675     Boogie_Dijkstra
   676     VCC_Max
   677   files
   678     "Boogie_Dijkstra.b2i"
   679     "Boogie_Dijkstra.certs"
   680     "Boogie_Max.b2i"
   681     "Boogie_Max.certs"
   682     "VCC_Max.b2i"
   683     "VCC_Max.certs"
   684 
   685 session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" +
   686   options [document = false]
   687   theories SPARK
   688 
   689 session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
   690   options [document = false]
   691   theories
   692     "Gcd/Greatest_Common_Divisor"
   693 
   694     "Liseq/Longest_Increasing_Subsequence"
   695 
   696     "RIPEMD-160/F"
   697     "RIPEMD-160/Hash"
   698     "RIPEMD-160/K_L"
   699     "RIPEMD-160/K_R"
   700     "RIPEMD-160/R_L"
   701     "RIPEMD-160/Round"
   702     "RIPEMD-160/R_R"
   703     "RIPEMD-160/S_L"
   704     "RIPEMD-160/S_R"
   705 
   706     "Sqrt/Sqrt"
   707   files
   708     "Gcd/greatest_common_divisor/g_c_d.fdl"
   709     "Gcd/greatest_common_divisor/g_c_d.rls"
   710     "Gcd/greatest_common_divisor/g_c_d.siv"
   711     "Liseq/liseq/liseq_length.fdl"
   712     "Liseq/liseq/liseq_length.rls"
   713     "Liseq/liseq/liseq_length.siv"
   714     "RIPEMD-160/rmd/f.fdl"
   715     "RIPEMD-160/rmd/f.rls"
   716     "RIPEMD-160/rmd/f.siv"
   717     "RIPEMD-160/rmd/hash.fdl"
   718     "RIPEMD-160/rmd/hash.rls"
   719     "RIPEMD-160/rmd/hash.siv"
   720     "RIPEMD-160/rmd/k_l.fdl"
   721     "RIPEMD-160/rmd/k_l.rls"
   722     "RIPEMD-160/rmd/k_l.siv"
   723     "RIPEMD-160/rmd/k_r.fdl"
   724     "RIPEMD-160/rmd/k_r.rls"
   725     "RIPEMD-160/rmd/k_r.siv"
   726     "RIPEMD-160/rmd/r_l.fdl"
   727     "RIPEMD-160/rmd/r_l.rls"
   728     "RIPEMD-160/rmd/r_l.siv"
   729     "RIPEMD-160/rmd/round.fdl"
   730     "RIPEMD-160/rmd/round.rls"
   731     "RIPEMD-160/rmd/round.siv"
   732     "RIPEMD-160/rmd/r_r.fdl"
   733     "RIPEMD-160/rmd/r_r.rls"
   734     "RIPEMD-160/rmd/r_r.siv"
   735     "RIPEMD-160/rmd/s_l.fdl"
   736     "RIPEMD-160/rmd/s_l.rls"
   737     "RIPEMD-160/rmd/s_l.siv"
   738     "RIPEMD-160/rmd/s_r.fdl"
   739     "RIPEMD-160/rmd/s_r.rls"
   740     "RIPEMD-160/rmd/s_r.siv"
   741 
   742 session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +
   743   options [show_question_marks = false]
   744   theories
   745     Example_Verification
   746     VC_Principles
   747     Reference
   748     Complex_Types
   749   files
   750     "complex_types_app/initialize.fdl"
   751     "complex_types_app/initialize.rls"
   752     "complex_types_app/initialize.siv"
   753     "document/complex_types.ads"
   754     "document/complex_types_app.adb"
   755     "document/complex_types_app.ads"
   756     "document/Gcd.adb"
   757     "document/Gcd.ads"
   758     "document/intro.tex"
   759     "document/loop_invariant.adb"
   760     "document/loop_invariant.ads"
   761     "document/root.bib"
   762     "document/root.tex"
   763     "document/Simple_Gcd.adb"
   764     "document/Simple_Gcd.ads"
   765     "loop_invariant/proc1.fdl"
   766     "loop_invariant/proc1.rls"
   767     "loop_invariant/proc1.siv"
   768     "loop_invariant/proc2.fdl"
   769     "loop_invariant/proc2.rls"
   770     "loop_invariant/proc2.siv"
   771     "simple_greatest_common_divisor/g_c_d.fdl"
   772     "simple_greatest_common_divisor/g_c_d.rls"
   773     "simple_greatest_common_divisor/g_c_d.siv"
   774 
   775 session "HOL-Mutabelle" in Mutabelle = HOL +
   776   options [document = false]
   777   theories MutabelleExtra
   778 
   779 session "HOL-Quickcheck_Examples" in Quickcheck_Examples = HOL +
   780   options [document = false]
   781   theories
   782     Quickcheck_Examples
   783   (* FIXME
   784     Quickcheck_Lattice_Examples
   785     Completeness
   786     Quickcheck_Interfaces
   787     Hotel_Example *)
   788   theories [condition = ISABELLE_GHC]
   789     Quickcheck_Narrowing_Examples
   790 
   791 session "HOL-Quickcheck_Benchmark" in Quickcheck_Benchmark = HOL +
   792   theories [condition = ISABELLE_FULL_TEST, quick_and_dirty]
   793     Find_Unused_Assms_Examples
   794     Needham_Schroeder_No_Attacker_Example
   795     Needham_Schroeder_Guided_Attacker_Example
   796     Needham_Schroeder_Unguided_Attacker_Example
   797 
   798 session "HOL-Quotient_Examples" in Quotient_Examples = HOL +
   799   description {*
   800     Author:     Cezary Kaliszyk and Christian Urban
   801   *}
   802   options [document = false]
   803   theories
   804     DList
   805     FSet
   806     Quotient_Int
   807     Quotient_Message
   808     Lift_FSet
   809     Lift_Set
   810     Lift_Fun
   811     Quotient_Rat
   812     Lift_DList
   813 
   814 session "HOL-Predicate_Compile_Examples" in Predicate_Compile_Examples = HOL +
   815   options [document = false]
   816   theories
   817     Examples
   818     Predicate_Compile_Tests
   819     (* FIXME
   820     Predicate_Compile_Quickcheck_Examples  -- should be added again soon (since 21-Oct-2010) *)
   821     Specialisation_Examples
   822     (* FIXME since 21-Jul-2011
   823     Hotel_Example_Small_Generator
   824     IMP_1
   825     IMP_2
   826     IMP_3
   827     IMP_4 *)
   828   theories [condition = "ISABELLE_SWIPL"]  (* FIXME: *or* ISABELLE_YAP (??) *)
   829     Code_Prolog_Examples
   830     Context_Free_Grammar_Example
   831     Hotel_Example_Prolog
   832     Lambda_Example
   833     List_Examples
   834   theories [condition = "ISABELLE_SWIPL", quick_and_dirty]  (* FIXME: *or* ISABELLE_YAP (??) *)
   835     Reg_Exp_Example
   836 
   837 session HOLCF (main) in HOLCF = HOL +
   838   description {*
   839     Author:     Franz Regensburger
   840     Author:     Brian Huffman
   841 
   842     HOLCF -- a semantic extension of HOL by the LCF logic.
   843   *}
   844   options [document_graph]
   845   theories [document = false]
   846     "~~/src/HOL/Library/Nat_Bijection"
   847     "~~/src/HOL/Library/Countable"
   848   theories
   849     Plain_HOLCF
   850     Fixrec
   851     HOLCF
   852   files "document/root.tex"
   853 
   854 session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF +
   855   theories
   856     Domain_ex
   857     Fixrec_ex
   858     New_Domain
   859   files "document/root.tex"
   860 
   861 session "HOLCF-Library" in "HOLCF/Library" = HOLCF +
   862   options [document = false]
   863   theories HOLCF_Library
   864 
   865 session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF +
   866   options [document = false]
   867   theories HoareEx
   868   files "document/root.tex"
   869 
   870 session "HOLCF-ex" in "HOLCF/ex" = HOLCF +
   871   description {* Misc HOLCF examples *}
   872   options [document = false]
   873   theories
   874     Dnat
   875     Dagstuhl
   876     Focus_ex
   877     Fix2
   878     Hoare
   879     Concurrency_Monad
   880     Loop
   881     Powerdomain_ex
   882     Domain_Proofs
   883     Letrec
   884     Pattern_Match
   885 
   886 session "HOLCF-FOCUS" in "HOLCF/FOCUS" = HOLCF +
   887   options [document = false]
   888   theories
   889     Fstreams
   890     FOCUS
   891     Buffer_adm
   892 
   893 session IOA in "HOLCF/IOA" = HOLCF +
   894   description {*
   895     Author:     Olaf Mueller
   896 
   897     Formalization of a semantic model of I/O-Automata.
   898   *}
   899   options [document = false]
   900   theories "meta_theory/Abstraction"
   901 
   902 session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
   903   description {*
   904     Author:     Olaf Mueller
   905 
   906     The Alternating Bit Protocol performed in I/O-Automata.
   907   *}
   908   options [document = false]
   909   theories Correctness
   910 
   911 session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA +
   912   description {*
   913     Author:     Tobias Nipkow & Konrad Slind
   914 
   915     A network transmission protocol, performed in the
   916     I/O automata formalization by Olaf Mueller.
   917   *}
   918   options [document = false]
   919   theories Correctness
   920 
   921 session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA +
   922   description {*
   923     Author:     Olaf Mueller
   924 
   925     Memory storage case study.
   926   *}
   927   options [document = false]
   928   theories Correctness
   929 
   930 session "IOA-ex" in "HOLCF/IOA/ex" = IOA +
   931   description {*
   932     Author:     Olaf Mueller
   933   *}
   934   options [document = false]
   935   theories
   936     TrivEx
   937     TrivEx2
   938 
   939 session "HOL-Datatype_Benchmark" in Datatype_Benchmark = HOL +
   940   description {* Some rather large datatype examples (from John Harrison). *}
   941   options [document = false]
   942   theories [condition = ISABELLE_FULL_TEST, timing]
   943     Brackin
   944     Instructions
   945     SML
   946     Verilog
   947 
   948 session "HOL-Record_Benchmark" in Record_Benchmark = HOL +
   949   description {* Some benchmark on large record. *}
   950   options [document = false]
   951   theories [condition = ISABELLE_FULL_TEST, timing]
   952     Record_Benchmark
   953