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