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