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