src/HOL/ROOT
author nipkow
Sat Dec 29 17:18:01 2012 +0100 (2012-12-29)
changeset 50634 009a9fdabbad
parent 50571 b649e33e4821
child 50665 c9daeff9516e
permissions -rw-r--r--
new theory Library/Finite_Lattice
     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 
   681 session "HOL-Boogie" in "Boogie" = "HOL-Word" +
   682   options [document = false]
   683   theories Boogie
   684 
   685 session "HOL-Boogie-Examples" in "Boogie/Examples" = "HOL-Boogie" +
   686   options [document = false]
   687   theories
   688     Boogie_Max_Stepwise
   689     Boogie_Max
   690     Boogie_Dijkstra
   691     VCC_Max
   692   files
   693     "Boogie_Dijkstra.b2i"
   694     "Boogie_Dijkstra.certs"
   695     "Boogie_Max.b2i"
   696     "Boogie_Max.certs"
   697     "VCC_Max.b2i"
   698     "VCC_Max.certs"
   699 
   700 session "HOL-SPARK" in "SPARK" = "HOL-Word" +
   701   options [document = false]
   702   theories SPARK
   703 
   704 session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
   705   options [document = false]
   706   theories
   707     "Gcd/Greatest_Common_Divisor"
   708 
   709     "Liseq/Longest_Increasing_Subsequence"
   710 
   711     "RIPEMD-160/F"
   712     "RIPEMD-160/Hash"
   713     "RIPEMD-160/K_L"
   714     "RIPEMD-160/K_R"
   715     "RIPEMD-160/R_L"
   716     "RIPEMD-160/Round"
   717     "RIPEMD-160/R_R"
   718     "RIPEMD-160/S_L"
   719     "RIPEMD-160/S_R"
   720 
   721     "Sqrt/Sqrt"
   722   files
   723     "Gcd/greatest_common_divisor/g_c_d.fdl"
   724     "Gcd/greatest_common_divisor/g_c_d.rls"
   725     "Gcd/greatest_common_divisor/g_c_d.siv"
   726     "Liseq/liseq/liseq_length.fdl"
   727     "Liseq/liseq/liseq_length.rls"
   728     "Liseq/liseq/liseq_length.siv"
   729     "RIPEMD-160/rmd/f.fdl"
   730     "RIPEMD-160/rmd/f.rls"
   731     "RIPEMD-160/rmd/f.siv"
   732     "RIPEMD-160/rmd/hash.fdl"
   733     "RIPEMD-160/rmd/hash.rls"
   734     "RIPEMD-160/rmd/hash.siv"
   735     "RIPEMD-160/rmd/k_l.fdl"
   736     "RIPEMD-160/rmd/k_l.rls"
   737     "RIPEMD-160/rmd/k_l.siv"
   738     "RIPEMD-160/rmd/k_r.fdl"
   739     "RIPEMD-160/rmd/k_r.rls"
   740     "RIPEMD-160/rmd/k_r.siv"
   741     "RIPEMD-160/rmd/r_l.fdl"
   742     "RIPEMD-160/rmd/r_l.rls"
   743     "RIPEMD-160/rmd/r_l.siv"
   744     "RIPEMD-160/rmd/round.fdl"
   745     "RIPEMD-160/rmd/round.rls"
   746     "RIPEMD-160/rmd/round.siv"
   747     "RIPEMD-160/rmd/r_r.fdl"
   748     "RIPEMD-160/rmd/r_r.rls"
   749     "RIPEMD-160/rmd/r_r.siv"
   750     "RIPEMD-160/rmd/s_l.fdl"
   751     "RIPEMD-160/rmd/s_l.rls"
   752     "RIPEMD-160/rmd/s_l.siv"
   753     "RIPEMD-160/rmd/s_r.fdl"
   754     "RIPEMD-160/rmd/s_r.rls"
   755     "RIPEMD-160/rmd/s_r.siv"
   756 
   757 session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +
   758   options [show_question_marks = false]
   759   theories
   760     Example_Verification
   761     VC_Principles
   762     Reference
   763     Complex_Types
   764   files
   765     "complex_types_app/initialize.fdl"
   766     "complex_types_app/initialize.rls"
   767     "complex_types_app/initialize.siv"
   768     "document/complex_types.ads"
   769     "document/complex_types_app.adb"
   770     "document/complex_types_app.ads"
   771     "document/Gcd.adb"
   772     "document/Gcd.ads"
   773     "document/intro.tex"
   774     "document/loop_invariant.adb"
   775     "document/loop_invariant.ads"
   776     "document/root.bib"
   777     "document/root.tex"
   778     "document/Simple_Gcd.adb"
   779     "document/Simple_Gcd.ads"
   780     "loop_invariant/proc1.fdl"
   781     "loop_invariant/proc1.rls"
   782     "loop_invariant/proc1.siv"
   783     "loop_invariant/proc2.fdl"
   784     "loop_invariant/proc2.rls"
   785     "loop_invariant/proc2.siv"
   786     "simple_greatest_common_divisor/g_c_d.fdl"
   787     "simple_greatest_common_divisor/g_c_d.rls"
   788     "simple_greatest_common_divisor/g_c_d.siv"
   789 
   790 session "HOL-Mutabelle" in Mutabelle = HOL +
   791   options [document = false]
   792   theories MutabelleExtra
   793 
   794 session "HOL-Quickcheck_Examples" in Quickcheck_Examples = HOL +
   795   options [document = false]
   796   theories
   797     Quickcheck_Examples
   798   (* FIXME
   799     Quickcheck_Lattice_Examples
   800     Completeness
   801     Quickcheck_Interfaces
   802     Hotel_Example *)
   803   theories [condition = ISABELLE_GHC]
   804     Quickcheck_Narrowing_Examples
   805 
   806 session "HOL-Quickcheck_Benchmark" in Quickcheck_Benchmark = HOL +
   807   theories [condition = ISABELLE_FULL_TEST, quick_and_dirty]
   808     Find_Unused_Assms_Examples
   809     Needham_Schroeder_No_Attacker_Example
   810     Needham_Schroeder_Guided_Attacker_Example
   811     Needham_Schroeder_Unguided_Attacker_Example
   812 
   813 session "HOL-Quotient_Examples" in Quotient_Examples = HOL +
   814   description {*
   815     Author:     Cezary Kaliszyk and Christian Urban
   816   *}
   817   options [document = false]
   818   theories
   819     DList
   820     FSet
   821     Quotient_Int
   822     Quotient_Message
   823     Lift_FSet
   824     Lift_Set
   825     Lift_Fun
   826     Quotient_Rat
   827     Lift_DList
   828 
   829 session "HOL-Predicate_Compile_Examples" in Predicate_Compile_Examples = HOL +
   830   options [document = false]
   831   theories
   832     Examples
   833     Predicate_Compile_Tests
   834     (* FIXME
   835     Predicate_Compile_Quickcheck_Examples  -- should be added again soon (since 21-Oct-2010) *)
   836     Specialisation_Examples
   837     (* FIXME since 21-Jul-2011
   838     Hotel_Example_Small_Generator
   839     IMP_1
   840     IMP_2
   841     IMP_3
   842     IMP_4 *)
   843   theories [condition = "ISABELLE_SWIPL"]  (* FIXME: *or* ISABELLE_YAP (??) *)
   844     Code_Prolog_Examples
   845     Context_Free_Grammar_Example
   846     Hotel_Example_Prolog
   847     Lambda_Example
   848     List_Examples
   849   theories [condition = "ISABELLE_SWIPL", quick_and_dirty]  (* FIXME: *or* ISABELLE_YAP (??) *)
   850     Reg_Exp_Example
   851 
   852 session HOLCF (main) in HOLCF = HOL +
   853   description {*
   854     Author:     Franz Regensburger
   855     Author:     Brian Huffman
   856 
   857     HOLCF -- a semantic extension of HOL by the LCF logic.
   858   *}
   859   options [document_graph]
   860   theories [document = false]
   861     "~~/src/HOL/Library/Nat_Bijection"
   862     "~~/src/HOL/Library/Countable"
   863   theories
   864     Plain_HOLCF
   865     Fixrec
   866     HOLCF
   867   files "document/root.tex"
   868 
   869 session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF +
   870   theories
   871     Domain_ex
   872     Fixrec_ex
   873     New_Domain
   874   files "document/root.tex"
   875 
   876 session "HOLCF-Library" in "HOLCF/Library" = HOLCF +
   877   options [document = false]
   878   theories HOLCF_Library
   879 
   880 session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF +
   881   options [document = false]
   882   theories HoareEx
   883   files "document/root.tex"
   884 
   885 session "HOLCF-ex" in "HOLCF/ex" = HOLCF +
   886   description {* Misc HOLCF examples *}
   887   options [document = false]
   888   theories
   889     Dnat
   890     Dagstuhl
   891     Focus_ex
   892     Fix2
   893     Hoare
   894     Concurrency_Monad
   895     Loop
   896     Powerdomain_ex
   897     Domain_Proofs
   898     Letrec
   899     Pattern_Match
   900 
   901 session "HOLCF-FOCUS" in "HOLCF/FOCUS" = HOLCF +
   902   options [document = false]
   903   theories
   904     Fstreams
   905     FOCUS
   906     Buffer_adm
   907 
   908 session IOA in "HOLCF/IOA" = HOLCF +
   909   description {*
   910     Author:     Olaf Mueller
   911 
   912     Formalization of a semantic model of I/O-Automata.
   913   *}
   914   options [document = false]
   915   theories "meta_theory/Abstraction"
   916 
   917 session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
   918   description {*
   919     Author:     Olaf Mueller
   920 
   921     The Alternating Bit Protocol performed in I/O-Automata.
   922   *}
   923   options [document = false]
   924   theories Correctness
   925 
   926 session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA +
   927   description {*
   928     Author:     Tobias Nipkow & Konrad Slind
   929 
   930     A network transmission protocol, performed in the
   931     I/O automata formalization by Olaf Mueller.
   932   *}
   933   options [document = false]
   934   theories Correctness
   935 
   936 session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA +
   937   description {*
   938     Author:     Olaf Mueller
   939 
   940     Memory storage case study.
   941   *}
   942   options [document = false]
   943   theories Correctness
   944 
   945 session "IOA-ex" in "HOLCF/IOA/ex" = IOA +
   946   description {*
   947     Author:     Olaf Mueller
   948   *}
   949   options [document = false]
   950   theories
   951     TrivEx
   952     TrivEx2
   953 
   954 session "HOL-Datatype_Benchmark" in Datatype_Benchmark = HOL +
   955   description {* Some rather large datatype examples (from John Harrison). *}
   956   options [document = false]
   957   theories [condition = ISABELLE_FULL_TEST, timing]
   958     Brackin
   959     Instructions
   960     SML
   961     Verilog
   962 
   963 session "HOL-Record_Benchmark" in Record_Benchmark = HOL +
   964   description {* Some benchmark on large record. *}
   965   options [document = false]
   966   theories [condition = ISABELLE_FULL_TEST, timing]
   967     Record_Benchmark
   968