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