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