wneuper/isa: src/HOL/ROOT@80b1963215c8

     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"

    11 session "HOL-Base" = Pure +

    12   description {* Raw HOL base, with minimal tools *}

    13   options [document = false]

    14   theories HOL

    16 session "HOL-Plain" = Pure +

    17   description {* HOL side-entry after bootstrap of many tools and packages *}

    18   options [document = false]

    19   theories Plain

    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"

    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"

    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"

    56 session "HOL-Hahn_Banach" in Hahn_Banach = HOL +

    57   description {*

    58     Author:     Gertrud Bauer, TU Munich

    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"

    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"

    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"

   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

   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

   137 session "HOL-Number_Theory" in Number_Theory = HOL +

   138   options [document = false]

   139   theories Number_Theory

   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"

   157 session "HOL-Hoare" in Hoare = HOL +

   158   theories Hoare

   159   files "document/root.bib" "document/root.tex"

   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"

   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

   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

   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

   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

   197 session "HOL-Algebra" in Algebra = HOL +

   198   description {*

   199     Author: Clemens Ballarin, started 24 September 1999

   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 *)

   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"

   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"

   237 session "HOL-UNITY" in UNITY = HOL +

   238   description {*

   239     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

   240     Copyright   1998  University of Cambridge

   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"

   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"

   261     (*Verifying security protocols using UNITY*)

   262     "Simple/NSP_Bad"

   264     (*Example of composition*)

   265     "Comp/Handshake"

   267     (*Universal properties examples*)

   268     "Comp/Counter"

   269     "Comp/Counterc"

   270     "Comp/Priority"

   272     "Comp/TimerArray"

   273     "Comp/Progress"

   275     "Comp/Alloc"

   276     "Comp/AllocImpl"

   277     "Comp/Client"

   279     (*obsolete*)

   280     "ELT"

   281   files "document/root.tex"

   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"

   288 session "HOL-ZF" in ZF = HOL +

   289   description {* *}

   290   theories MainZF Games

   291   files "document/root.tex"

   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"

   304 session "HOL-Decision_Procs" in Decision_Procs = HOL +

   305   options [condition = ISABELLE_POLYML, document = false]

   306   theories Decision_Procs

   308 session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +

   309   options [document = false, proofs = 2, parallel_proofs = 0]

   310   theories Hilbert_Classical

   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"

   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"

   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

   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"

   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

   360 session "HOL-NanoJava" in NanoJava = HOL +

   361   options [document_graph]

   362   theories Example

   363   files "document/root.bib" "document/root.tex"

   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"

   374 session "HOL-IOA" in IOA = HOL +

   375   description {*

   376     Author:     Tobias Nipkow & Konrad Slind

   377     Copyright   1994  TU Muenchen

   379     The meta theory of I/O-Automata.

   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

   390     and

   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

   403 session "HOL-Lattice" in Lattice = HOL +

   404   description {*

   405     Author:     Markus Wenzel, TU Muenchen

   407     Basic theory of lattices and orders.

   408   *}

   409   theories CompleteLattice

   410   files "document/root.tex"

   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"

   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"

   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"

   530 session "HOL-Matrix_LP" in Matrix_LP = HOL +

   531   options [document_graph]

   532   theories Cplex

   533   files "document/root.tex"

   535 session "HOL-TLA" in TLA = HOL +

   536   description {* The Temporal Logic of Actions *}

   537   options [document = false]

   538   theories TLA

   540 session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" +

   541   options [document = false]

   542   theories Inc

   544 session "HOL-TLA-Buffer" in "TLA/Buffer" = "HOL-TLA" +

   545   options [document = false]

   546   theories DBuffer

   548 session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" +

   549   options [document = false]

   550   theories MemoryImplementation

   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

   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

   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"

   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"

   591 session "HOL-Nominal" (main) in Nominal = HOL +

   592   options [document = false]

   593   theories Nominal

   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

   600 session "HOL-Cardinals-Base" in Cardinals = HOL +

   601   description {* Ordinals and Cardinals, Base Theories *}

   602   options [document = false]

   603   theories Cardinal_Arithmetic

   605 session "HOL-Cardinals" in Cardinals = "HOL-Cardinals-Base" +

   606   description {* Ordinals and Cardinals, Full Theories *}

   607   theories Cardinals

   608   files

   609     "document/intro.tex"

   610     "document/root.tex"

   611     "document/root.bib"

   613 session "HOL-Codatatype" in Codatatype = "HOL-Cardinals-Base" +

   614   description {* New (Co)datatype Package *}

   615   options [document = false]

   616   theories Codatatype

   618 session "HOL-Codatatype-Examples" in "Codatatype/Examples" = "HOL-Codatatype" +

   619   description {* Examples for the New (Co)datatype Package *}

   620   options [document = false]

   621   theories

   622     HFset

   623     Lambda_Term

   624     Process

   625     TreeFsetI

   626     "Infinite_Derivation_Trees/Gram_Lang"

   627     "Infinite_Derivation_Trees/Parallel"

   628     Stream

   629   theories [condition = ISABELLE_FULL_TEST]

   630     Misc_Codata

   631     Misc_Data

   633 session "HOL-Word" in Word = HOL +

   634   options [document_graph]

   635   theories Word

   636   files "document/root.bib" "document/root.tex"

   638 session "HOL-Word-Examples" in "Word/Examples" = "HOL-Word" +

   639   options [document = false]

   640   theories WordExamples

   642 session "HOL-Statespace" in Statespace = HOL +

   643   theories StateSpaceEx

   644   files "document/root.tex"

   646 session "HOL-NSA" in NSA = HOL +

   647   options [document_graph]

   648   theories Hypercomplex

   649   files "document/root.tex"

   651 session "HOL-NSA-Examples" in "NSA/Examples" = "HOL-NSA" +

   652   options [document = false]

   653   theories NSPrimes

   655 session "HOL-Mirabelle" in Mirabelle = HOL +

   656   options [document = false]

   657   theories Mirabelle_Test

   659 session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +

   660   options [document = false, timeout = 600 (* FIXME avoid "hang" of external bash *) ]

   661   theories [condition = ISABELLE_FULL_TEST] Ex

   663 session "HOL-Word-SMT_Examples" in SMT_Examples = "HOL-Word" +

   664   options [document = false, quick_and_dirty]

   665   theories

   666     SMT_Tests

   667     SMT_Examples

   668     SMT_Word_Examples

   669   files

   670     "SMT_Examples.certs"

   671     "SMT_Tests.certs"

   673 session "HOL-Boogie" in "Boogie" = "HOL-Word" +

   674   options [document = false]

   675   theories Boogie

   677 session "HOL-Boogie-Examples" in "Boogie/Examples" = "HOL-Boogie" +

   678   options [document = false]

   679   theories

   680     Boogie_Max_Stepwise

   681     Boogie_Max

   682     Boogie_Dijkstra

   683     VCC_Max

   684   files

   685     "Boogie_Dijkstra.b2i"

   686     "Boogie_Dijkstra.certs"

   687     "Boogie_Max.b2i"

   688     "Boogie_Max.certs"

   689     "VCC_Max.b2i"

   690     "VCC_Max.certs"

   692 session "HOL-SPARK" in "SPARK" = "HOL-Word" +

   693   options [document = false]

   694   theories SPARK

   696 session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +

   697   options [document = false]

   698   theories

   699     "Gcd/Greatest_Common_Divisor"

   701     "Liseq/Longest_Increasing_Subsequence"

   703     "RIPEMD-160/F"

   704     "RIPEMD-160/Hash"

   705     "RIPEMD-160/K_L"

   706     "RIPEMD-160/K_R"

   707     "RIPEMD-160/R_L"

   708     "RIPEMD-160/Round"

   709     "RIPEMD-160/R_R"

   710     "RIPEMD-160/S_L"

   711     "RIPEMD-160/S_R"

   713     "Sqrt/Sqrt"

   714   files

   715     "Gcd/greatest_common_divisor/g_c_d.fdl"

   716     "Gcd/greatest_common_divisor/g_c_d.rls"

   717     "Gcd/greatest_common_divisor/g_c_d.siv"

   718     "Liseq/liseq/liseq_length.fdl"

   719     "Liseq/liseq/liseq_length.rls"

   720     "Liseq/liseq/liseq_length.siv"

   721     "RIPEMD-160/rmd/f.fdl"

   722     "RIPEMD-160/rmd/f.rls"

   723     "RIPEMD-160/rmd/f.siv"

   724     "RIPEMD-160/rmd/hash.fdl"

   725     "RIPEMD-160/rmd/hash.rls"

   726     "RIPEMD-160/rmd/hash.siv"

   727     "RIPEMD-160/rmd/k_l.fdl"

   728     "RIPEMD-160/rmd/k_l.rls"

   729     "RIPEMD-160/rmd/k_l.siv"

   730     "RIPEMD-160/rmd/k_r.fdl"

   731     "RIPEMD-160/rmd/k_r.rls"

   732     "RIPEMD-160/rmd/k_r.siv"

   733     "RIPEMD-160/rmd/r_l.fdl"

   734     "RIPEMD-160/rmd/r_l.rls"

   735     "RIPEMD-160/rmd/r_l.siv"

   736     "RIPEMD-160/rmd/round.fdl"

   737     "RIPEMD-160/rmd/round.rls"

   738     "RIPEMD-160/rmd/round.siv"

   739     "RIPEMD-160/rmd/r_r.fdl"

   740     "RIPEMD-160/rmd/r_r.rls"

   741     "RIPEMD-160/rmd/r_r.siv"

   742     "RIPEMD-160/rmd/s_l.fdl"

   743     "RIPEMD-160/rmd/s_l.rls"

   744     "RIPEMD-160/rmd/s_l.siv"

   745     "RIPEMD-160/rmd/s_r.fdl"

   746     "RIPEMD-160/rmd/s_r.rls"

   747     "RIPEMD-160/rmd/s_r.siv"

   749 session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +

   750   options [show_question_marks = false]

   751   theories

   752     Example_Verification

   753     VC_Principles

   754     Reference

   755     Complex_Types

   756   files

   757     "complex_types_app/initialize.fdl"

   758     "complex_types_app/initialize.rls"

   759     "complex_types_app/initialize.siv"

   760     "document/complex_types.ads"

   761     "document/complex_types_app.adb"

   762     "document/complex_types_app.ads"

   763     "document/Gcd.adb"

   764     "document/Gcd.ads"

   765     "document/intro.tex"

   766     "document/loop_invariant.adb"

   767     "document/loop_invariant.ads"

   768     "document/root.bib"

   769     "document/root.tex"

   770     "document/Simple_Gcd.adb"

   771     "document/Simple_Gcd.ads"

   772     "loop_invariant/proc1.fdl"

   773     "loop_invariant/proc1.rls"

   774     "loop_invariant/proc1.siv"

   775     "loop_invariant/proc2.fdl"

   776     "loop_invariant/proc2.rls"

   777     "loop_invariant/proc2.siv"

   778     "simple_greatest_common_divisor/g_c_d.fdl"

   779     "simple_greatest_common_divisor/g_c_d.rls"

   780     "simple_greatest_common_divisor/g_c_d.siv"

   782 session "HOL-Mutabelle" in Mutabelle = HOL +

   783   options [document = false]

   784   theories MutabelleExtra

   786 session "HOL-Quickcheck_Examples" in Quickcheck_Examples = HOL +

   787   options [timeout = 3600, document = false]

   788   theories

   789     Quickcheck_Examples

   790   (* FIXME

   791     Quickcheck_Lattice_Examples

   792     Completeness

   793     Quickcheck_Interfaces

   794     Hotel_Example *)

   795   theories [condition = ISABELLE_GHC]

   796     Quickcheck_Narrowing_Examples

   798 session "HOL-Quickcheck_Benchmark" in Quickcheck_Benchmark = HOL +

   799   theories [condition = ISABELLE_FULL_TEST, quick_and_dirty]

   800     Find_Unused_Assms_Examples

   801     Needham_Schroeder_No_Attacker_Example

   802     Needham_Schroeder_Guided_Attacker_Example

   803     Needham_Schroeder_Unguided_Attacker_Example

   805 session "HOL-Quotient_Examples" in Quotient_Examples = HOL +

   806   description {*

   807     Author:     Cezary Kaliszyk and Christian Urban

   808   *}

   809   options [document = false]

   810   theories

   811     DList

   812     FSet

   813     Quotient_Int

   814     Quotient_Message

   815     Lift_FSet

   816     Lift_Set

   817     Lift_Fun

   818     Quotient_Rat

   819     Lift_DList

   821 session "HOL-Predicate_Compile_Examples" in Predicate_Compile_Examples = HOL +

   822   options [document = false]

   823   theories

   824     Examples

   825     Predicate_Compile_Tests

   826     (* FIXME

   827     Predicate_Compile_Quickcheck_Examples  -- should be added again soon (since 21-Oct-2010) *)

   828     Specialisation_Examples

   829     (* FIXME since 21-Jul-2011

   830     Hotel_Example_Small_Generator

   831     IMP_1

   832     IMP_2

   833     IMP_3

   834     IMP_4 *)

   835   theories [condition = "ISABELLE_SWIPL"]  (* FIXME: *or* ISABELLE_YAP (??) *)

   836     Code_Prolog_Examples

   837     Context_Free_Grammar_Example

   838     Hotel_Example_Prolog

   839     Lambda_Example

   840     List_Examples

   841   theories [condition = "ISABELLE_SWIPL", quick_and_dirty]  (* FIXME: *or* ISABELLE_YAP (??) *)

   842     Reg_Exp_Example

   844 session HOLCF (main) in HOLCF = HOL +

   845   description {*

   846     Author:     Franz Regensburger

   847     Author:     Brian Huffman

   849     HOLCF -- a semantic extension of HOL by the LCF logic.

   850   *}

   851   options [document_graph]

   852   theories [document = false]

   853     "~~/src/HOL/Library/Nat_Bijection"

   854     "~~/src/HOL/Library/Countable"

   855   theories

   856     Plain_HOLCF

   857     Fixrec

   858     HOLCF

   859   files "document/root.tex"

   861 session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF +

   862   theories

   863     Domain_ex

   864     Fixrec_ex

   865     New_Domain

   866   files "document/root.tex"

   868 session "HOLCF-Library" in "HOLCF/Library" = HOLCF +

   869   options [document = false]

   870   theories HOLCF_Library

   872 session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF +

   873   options [document = false]

   874   theories HoareEx

   875   files "document/root.tex"

   877 session "HOLCF-ex" in "HOLCF/ex" = HOLCF +

   878   description {* Misc HOLCF examples *}

   879   options [document = false]

   880   theories

   881     Dnat

   882     Dagstuhl

   883     Focus_ex

   884     Fix2

   885     Hoare

   886     Concurrency_Monad

   887     Loop

   888     Powerdomain_ex

   889     Domain_Proofs

   890     Letrec

   891     Pattern_Match

   893 session "HOLCF-FOCUS" in "HOLCF/FOCUS" = HOLCF +

   894   options [document = false]

   895   theories

   896     Fstreams

   897     FOCUS

   898     Buffer_adm

   900 session IOA in "HOLCF/IOA" = HOLCF +

   901   description {*

   902     Author:     Olaf Mueller

   904     Formalization of a semantic model of I/O-Automata.

   905   *}

   906   options [document = false]

   907   theories "meta_theory/Abstraction"

   909 session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +

   910   description {*

   911     Author:     Olaf Mueller

   913     The Alternating Bit Protocol performed in I/O-Automata.

   914   *}

   915   options [document = false]

   916   theories Correctness

   918 session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA +

   919   description {*

   920     Author:     Tobias Nipkow & Konrad Slind

   922     A network transmission protocol, performed in the

   923     I/O automata formalization by Olaf Mueller.

   924   *}

   925   options [document = false]

   926   theories Correctness

   928 session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA +

   929   description {*

   930     Author:     Olaf Mueller

   932     Memory storage case study.

   933   *}

   934   options [document = false]

   935   theories Correctness

   937 session "IOA-ex" in "HOLCF/IOA/ex" = IOA +

   938   description {*

   939     Author:     Olaf Mueller

   940   *}

   941   options [document = false]

   942   theories

   943     TrivEx

   944     TrivEx2

   946 session "HOL-Datatype_Benchmark" in Datatype_Benchmark = HOL +

   947   description {* Some rather large datatype examples (from John Harrison). *}

   948   options [document = false]

   949   theories [condition = ISABELLE_FULL_TEST, timing]

   950     Brackin

   951     Instructions

   952     SML

   953     Verilog

   955 session "HOL-Record_Benchmark" in Record_Benchmark = HOL +

   956   description {* Some benchmark on large record. *}

   957   options [document = false]

   958   theories [condition = ISABELLE_FULL_TEST, timing]

   959     Record_Benchmark

author	popescua
	Tue, 18 Sep 2012 13:38:10 +0200
changeset 50454	80b1963215c8
parent 50419	a93d920707bb
child 50463	8a232a4e3fd8
permissions	-rw-r--r--