src/HOL/ROOT
author wenzelm
Thu Sep 13 16:43:33 2012 +0200 (2012-09-13)
changeset 49349 be27a453aacc
parent 49310 6e30078de4f0
child 49404 a93d920707bb
permissions -rw-r--r--
workaround for HOL-Mirabelle-ex oddities;
     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   theories Cardinal_Order_Relation
   608   files
   609     "document/intro.tex"
   610     "document/root.tex"
   611     "document/root.bib"
   612 
   613 session "HOL-Codatatype" in Codatatype = "HOL-Cardinals-Base" +
   614   description {* New (Co)datatype Package *}
   615   options [document = false]
   616   theories Codatatype
   617 
   618 session "HOL-Codatatype-Examples" in "Codatatype/Examples" = "HOL-Codatatype" +
   619   description {* Examples for the New (Co)datatype Package *}
   620   options [document = false]
   621   theories
   622     HFset
   623     Lambda_Term
   624     Process
   625     TreeFsetI
   626     "Infinite_Derivation_Trees/Gram_Lang"
   627     "Infinite_Derivation_Trees/Parallel"
   628     Stream
   629   theories [condition = ISABELLE_FULL_TEST]
   630     Misc_Codata
   631     Misc_Data
   632 
   633 session "HOL-Word" in Word = HOL +
   634   options [document_graph]
   635   theories Word
   636   files "document/root.bib" "document/root.tex"
   637 
   638 session "HOL-Word-Examples" in "Word/Examples" = "HOL-Word" +
   639   options [document = false]
   640   theories WordExamples
   641 
   642 session "HOL-Statespace" in Statespace = HOL +
   643   theories StateSpaceEx
   644   files "document/root.tex"
   645 
   646 session "HOL-NSA" in NSA = HOL +
   647   options [document_graph]
   648   theories Hypercomplex
   649   files "document/root.tex"
   650 
   651 session "HOL-NSA-Examples" in "NSA/Examples" = "HOL-NSA" +
   652   options [document = false]
   653   theories NSPrimes
   654 
   655 session "HOL-Mirabelle" in Mirabelle = HOL +
   656   options [document = false]
   657   theories Mirabelle_Test
   658 
   659 session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
   660   options [document = false, timeout = 600 (* FIXME avoid "hang" of external bash *) ]
   661   theories Ex
   662 
   663 session "HOL-Word-SMT_Examples" in SMT_Examples = "HOL-Word" +
   664   options [document = false, quick_and_dirty]
   665   theories
   666     SMT_Tests
   667     SMT_Examples
   668     SMT_Word_Examples
   669   files
   670     "SMT_Examples.certs"
   671     "SMT_Tests.certs"
   672 
   673 session "HOL-Boogie" in "Boogie" = "HOL-Word" +
   674   options [document = false]
   675   theories Boogie
   676 
   677 session "HOL-Boogie-Examples" in "Boogie/Examples" = "HOL-Boogie" +
   678   options [document = false]
   679   theories
   680     Boogie_Max_Stepwise
   681     Boogie_Max
   682     Boogie_Dijkstra
   683     VCC_Max
   684   files
   685     "Boogie_Dijkstra.b2i"
   686     "Boogie_Dijkstra.certs"
   687     "Boogie_Max.b2i"
   688     "Boogie_Max.certs"
   689     "VCC_Max.b2i"
   690     "VCC_Max.certs"
   691 
   692 session "HOL-SPARK" in "SPARK" = "HOL-Word" +
   693   options [document = false]
   694   theories SPARK
   695 
   696 session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
   697   options [document = false]
   698   theories
   699     "Gcd/Greatest_Common_Divisor"
   700 
   701     "Liseq/Longest_Increasing_Subsequence"
   702 
   703     "RIPEMD-160/F"
   704     "RIPEMD-160/Hash"
   705     "RIPEMD-160/K_L"
   706     "RIPEMD-160/K_R"
   707     "RIPEMD-160/R_L"
   708     "RIPEMD-160/Round"
   709     "RIPEMD-160/R_R"
   710     "RIPEMD-160/S_L"
   711     "RIPEMD-160/S_R"
   712 
   713     "Sqrt/Sqrt"
   714   files
   715     "Gcd/greatest_common_divisor/g_c_d.fdl"
   716     "Gcd/greatest_common_divisor/g_c_d.rls"
   717     "Gcd/greatest_common_divisor/g_c_d.siv"
   718     "Liseq/liseq/liseq_length.fdl"
   719     "Liseq/liseq/liseq_length.rls"
   720     "Liseq/liseq/liseq_length.siv"
   721     "RIPEMD-160/rmd/f.fdl"
   722     "RIPEMD-160/rmd/f.rls"
   723     "RIPEMD-160/rmd/f.siv"
   724     "RIPEMD-160/rmd/hash.fdl"
   725     "RIPEMD-160/rmd/hash.rls"
   726     "RIPEMD-160/rmd/hash.siv"
   727     "RIPEMD-160/rmd/k_l.fdl"
   728     "RIPEMD-160/rmd/k_l.rls"
   729     "RIPEMD-160/rmd/k_l.siv"
   730     "RIPEMD-160/rmd/k_r.fdl"
   731     "RIPEMD-160/rmd/k_r.rls"
   732     "RIPEMD-160/rmd/k_r.siv"
   733     "RIPEMD-160/rmd/r_l.fdl"
   734     "RIPEMD-160/rmd/r_l.rls"
   735     "RIPEMD-160/rmd/r_l.siv"
   736     "RIPEMD-160/rmd/round.fdl"
   737     "RIPEMD-160/rmd/round.rls"
   738     "RIPEMD-160/rmd/round.siv"
   739     "RIPEMD-160/rmd/r_r.fdl"
   740     "RIPEMD-160/rmd/r_r.rls"
   741     "RIPEMD-160/rmd/r_r.siv"
   742     "RIPEMD-160/rmd/s_l.fdl"
   743     "RIPEMD-160/rmd/s_l.rls"
   744     "RIPEMD-160/rmd/s_l.siv"
   745     "RIPEMD-160/rmd/s_r.fdl"
   746     "RIPEMD-160/rmd/s_r.rls"
   747     "RIPEMD-160/rmd/s_r.siv"
   748 
   749 session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +
   750   options [show_question_marks = false]
   751   theories
   752     Example_Verification
   753     VC_Principles
   754     Reference
   755     Complex_Types
   756   files
   757     "complex_types_app/initialize.fdl"
   758     "complex_types_app/initialize.rls"
   759     "complex_types_app/initialize.siv"
   760     "document/complex_types.ads"
   761     "document/complex_types_app.adb"
   762     "document/complex_types_app.ads"
   763     "document/Gcd.adb"
   764     "document/Gcd.ads"
   765     "document/intro.tex"
   766     "document/loop_invariant.adb"
   767     "document/loop_invariant.ads"
   768     "document/root.bib"
   769     "document/root.tex"
   770     "document/Simple_Gcd.adb"
   771     "document/Simple_Gcd.ads"
   772     "loop_invariant/proc1.fdl"
   773     "loop_invariant/proc1.rls"
   774     "loop_invariant/proc1.siv"
   775     "loop_invariant/proc2.fdl"
   776     "loop_invariant/proc2.rls"
   777     "loop_invariant/proc2.siv"
   778     "simple_greatest_common_divisor/g_c_d.fdl"
   779     "simple_greatest_common_divisor/g_c_d.rls"
   780     "simple_greatest_common_divisor/g_c_d.siv"
   781 
   782 session "HOL-Mutabelle" in Mutabelle = HOL +
   783   options [document = false]
   784   theories MutabelleExtra
   785 
   786 session "HOL-Quickcheck_Examples" in Quickcheck_Examples = HOL +
   787   options [timeout = 3600, document = false]
   788   theories
   789     Quickcheck_Examples
   790   (* FIXME
   791     Quickcheck_Lattice_Examples
   792     Completeness
   793     Quickcheck_Interfaces
   794     Hotel_Example *)
   795   theories [condition = ISABELLE_GHC]
   796     Quickcheck_Narrowing_Examples
   797 
   798 session "HOL-Quickcheck_Benchmark" in Quickcheck_Benchmark = HOL +
   799   theories [condition = ISABELLE_FULL_TEST, quick_and_dirty]
   800     Find_Unused_Assms_Examples
   801     Needham_Schroeder_No_Attacker_Example
   802     Needham_Schroeder_Guided_Attacker_Example
   803     Needham_Schroeder_Unguided_Attacker_Example
   804 
   805 session "HOL-Quotient_Examples" in Quotient_Examples = HOL +
   806   description {*
   807     Author:     Cezary Kaliszyk and Christian Urban
   808   *}
   809   options [document = false]
   810   theories
   811     DList
   812     FSet
   813     Quotient_Int
   814     Quotient_Message
   815     Lift_FSet
   816     Lift_Set
   817     Lift_Fun
   818     Quotient_Rat
   819     Lift_DList
   820 
   821 session "HOL-Predicate_Compile_Examples" in Predicate_Compile_Examples = HOL +
   822   options [document = false]
   823   theories
   824     Examples
   825     Predicate_Compile_Tests
   826     (* FIXME
   827     Predicate_Compile_Quickcheck_Examples  -- should be added again soon (since 21-Oct-2010) *)
   828     Specialisation_Examples
   829     (* FIXME since 21-Jul-2011
   830     Hotel_Example_Small_Generator
   831     IMP_1
   832     IMP_2
   833     IMP_3
   834     IMP_4 *)
   835   theories [condition = "ISABELLE_SWIPL"]  (* FIXME: *or* ISABELLE_YAP (??) *)
   836     Code_Prolog_Examples
   837     Context_Free_Grammar_Example
   838     Hotel_Example_Prolog
   839     Lambda_Example
   840     List_Examples
   841   theories [condition = "ISABELLE_SWIPL", quick_and_dirty]  (* FIXME: *or* ISABELLE_YAP (??) *)
   842     Reg_Exp_Example
   843 
   844 session HOLCF (main) in HOLCF = HOL +
   845   description {*
   846     Author:     Franz Regensburger
   847     Author:     Brian Huffman
   848 
   849     HOLCF -- a semantic extension of HOL by the LCF logic.
   850   *}
   851   options [document_graph]
   852   theories [document = false]
   853     "~~/src/HOL/Library/Nat_Bijection"
   854     "~~/src/HOL/Library/Countable"
   855   theories
   856     Plain_HOLCF
   857     Fixrec
   858     HOLCF
   859   files "document/root.tex"
   860 
   861 session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF +
   862   theories
   863     Domain_ex
   864     Fixrec_ex
   865     New_Domain
   866   files "document/root.tex"
   867 
   868 session "HOLCF-Library" in "HOLCF/Library" = HOLCF +
   869   options [document = false]
   870   theories HOLCF_Library
   871 
   872 session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF +
   873   options [document = false]
   874   theories HoareEx
   875   files "document/root.tex"
   876 
   877 session "HOLCF-ex" in "HOLCF/ex" = HOLCF +
   878   description {* Misc HOLCF examples *}
   879   options [document = false]
   880   theories
   881     Dnat
   882     Dagstuhl
   883     Focus_ex
   884     Fix2
   885     Hoare
   886     Concurrency_Monad
   887     Loop
   888     Powerdomain_ex
   889     Domain_Proofs
   890     Letrec
   891     Pattern_Match
   892 
   893 session "HOLCF-FOCUS" in "HOLCF/FOCUS" = HOLCF +
   894   options [document = false]
   895   theories
   896     Fstreams
   897     FOCUS
   898     Buffer_adm
   899 
   900 session IOA in "HOLCF/IOA" = HOLCF +
   901   description {*
   902     Author:     Olaf Mueller
   903 
   904     Formalization of a semantic model of I/O-Automata.
   905   *}
   906   options [document = false]
   907   theories "meta_theory/Abstraction"
   908 
   909 session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
   910   description {*
   911     Author:     Olaf Mueller
   912 
   913     The Alternating Bit Protocol performed in I/O-Automata.
   914   *}
   915   options [document = false]
   916   theories Correctness
   917 
   918 session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA +
   919   description {*
   920     Author:     Tobias Nipkow & Konrad Slind
   921 
   922     A network transmission protocol, performed in the
   923     I/O automata formalization by Olaf Mueller.
   924   *}
   925   options [document = false]
   926   theories Correctness
   927 
   928 session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA +
   929   description {*
   930     Author:     Olaf Mueller
   931 
   932     Memory storage case study.
   933   *}
   934   options [document = false]
   935   theories Correctness
   936 
   937 session "IOA-ex" in "HOLCF/IOA/ex" = IOA +
   938   description {*
   939     Author:     Olaf Mueller
   940   *}
   941   options [document = false]
   942   theories
   943     TrivEx
   944     TrivEx2
   945 
   946 session "HOL-Datatype_Benchmark" in Datatype_Benchmark = HOL +
   947   description {* Some rather large datatype examples (from John Harrison). *}
   948   options [document = false]
   949   theories [condition = ISABELLE_FULL_TEST, timing]
   950     Brackin
   951     Instructions
   952     SML
   953     Verilog
   954 
   955 session "HOL-Record_Benchmark" in Record_Benchmark = HOL +
   956   description {* Some benchmark on large record. *}
   957   options [document = false]
   958   theories [condition = ISABELLE_FULL_TEST, timing]
   959     Record_Benchmark
   960