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