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