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