isabelle: src/HOL/ROOT@c9b75c03de3c

     1 chapter HOL

     3 session HOL (main) = Pure +

     4   description {*

     5     Classical Higher-order Logic.

     6   *}

     7   options [document_graph]

     8   global_theories

     9     Main

    10     Complex_Main

    11   files

    12     "Tools/Quickcheck/Narrowing_Engine.hs"

    13     "Tools/Quickcheck/PNF_Narrowing_Engine.hs"

    14   document_files

    15     "root.bib"

    16     "root.tex"

    18 session "HOL-Proofs" = Pure +

    19   description {*

    20     HOL-Main with explicit proof terms.

    21   *}

    22   options [document = false, quick_and_dirty = false]

    23   theories Proofs (*sequential change of global flag!*)

    24   theories "~~/src/HOL/Library/Old_Datatype"

    25   files

    26     "Tools/Quickcheck/Narrowing_Engine.hs"

    27     "Tools/Quickcheck/PNF_Narrowing_Engine.hs"

    29 session "HOL-Library" (main) in Library = HOL +

    30   description {*

    31     Classical Higher-order Logic -- batteries included.

    32   *}

    33   theories

    34     Library

    35     (*conflicting type class instantiations*)

    36     List_lexord

    37     Sublist_Order

    38     Product_Lexorder

    39     Product_Order

    40     Finite_Lattice

    41     (*data refinements and dependent applications*)

    42     AList_Mapping

    43     Code_Binary_Nat

    44     Code_Char

    45     Code_Prolog

    46     Code_Real_Approx_By_Float

    47     Code_Target_Numeral

    48     DAList

    49     DAList_Multiset

    50     RBT_Mapping

    51     RBT_Set

    52     (*legacy tools*)

    53     Refute

    54     Old_Datatype

    55     Old_Recdef

    56     Old_SMT

    57   document_files "root.bib" "root.tex"

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

    60   description {*

    61     Author:     Gertrud Bauer, TU Munich

    63     The Hahn-Banach theorem for real vector spaces.

    65     This is the proof of the Hahn-Banach theorem for real vectorspaces,

    66     following H. Heuser, Funktionalanalysis, p. 228 -232. The Hahn-Banach

    67     theorem is one of the fundamental theorems of functional analysis. It is a

    68     conclusion of Zorn's lemma.

    70     Two different formaulations of the theorem are presented, one for general

    71     real vectorspaces and its application to normed vectorspaces.

    73     The theorem says, that every continous linearform, defined on arbitrary

    74     subspaces (not only one-dimensional subspaces), can be extended to a

    75     continous linearform on the whole vectorspace.

    76   *}

    77   options [document_graph]

    78   theories Hahn_Banach

    79   document_files "root.bib" "root.tex"

    81 session "HOL-Induct" in Induct = HOL +

    82   description {*

    83     Examples of (Co)Inductive Definitions.

    85     Comb proves the Church-Rosser theorem for combinators (see

    86     http://www.cl.cam.ac.uk/ftp/papers/reports/TR396-lcp-generic-automatic-proof-tools.ps.gz).

    88     Mutil is the famous Mutilated Chess Board problem (see

    89     http://www.cl.cam.ac.uk/ftp/papers/reports/TR394-lcp-mutilated-chess-board.dvi.gz).

    91     PropLog proves the completeness of a formalization of propositional logic

    92     (see

    93     http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz).

    95     Exp demonstrates the use of iterated inductive definitions to reason about

    96     mutually recursive relations.

    97   *}

    98   theories [document = false]

    99     "~~/src/HOL/Library/Old_Datatype"

   100   theories [quick_and_dirty]

   101     Common_Patterns

   102   theories

   103     QuoDataType

   104     QuoNestedDataType

   105     Term

   106     SList

   107     ABexp

   108     Tree

   109     Ordinals

   110     Sigma_Algebra

   111     Comb

   112     PropLog

   113     Com

   114   document_files "root.tex"

   116 session "HOL-IMP" in IMP = HOL +

   117   options [document_graph, document_variants=document]

   118   theories [document = false]

   119     "~~/src/Tools/Permanent_Interpretation"

   120     "~~/src/HOL/Library/While_Combinator"

   121     "~~/src/HOL/Library/Char_ord"

   122     "~~/src/HOL/Library/List_lexord"

   123     "~~/src/HOL/Library/Quotient_List"

   124     "~~/src/HOL/Library/Extended"

   125   theories

   126     BExp

   127     ASM

   128     Finite_Reachable

   129     Denotational

   130     Compiler2

   131     Poly_Types

   132     Sec_Typing

   133     Sec_TypingT

   134     Def_Init_Big

   135     Def_Init_Small

   136     Fold

   137     Live

   138     Live_True

   139     Hoare_Examples

   140     VCG

   141     Hoare_Total

   142     Collecting1

   143     Collecting_Examples

   144     Abs_Int_Tests

   145     Abs_Int1_parity

   146     Abs_Int1_const

   147     Abs_Int3

   148     "Abs_Int_ITP/Abs_Int1_parity_ITP"

   149     "Abs_Int_ITP/Abs_Int1_const_ITP"

   150     "Abs_Int_ITP/Abs_Int3_ITP"

   151     "Abs_Int_Den/Abs_Int_den2"

   152     Procs_Dyn_Vars_Dyn

   153     Procs_Stat_Vars_Dyn

   154     Procs_Stat_Vars_Stat

   155     C_like

   156     OO

   157   document_files "root.bib" "root.tex"

   159 session "HOL-IMPP" in IMPP = HOL +

   160   description {*

   161     Author:     David von Oheimb

   162     Copyright   1999 TUM

   164     IMPP -- An imperative language with procedures.

   166     This is an extension of IMP with local variables and mutually recursive

   167     procedures. For documentation see "Hoare Logic for Mutual Recursion and

   168     Local Variables" (http://isabelle.in.tum.de/Bali/papers/FSTTCS99.html).

   169   *}

   170   options [document = false]

   171   theories EvenOdd

   173 session "HOL-Import" in Import = HOL +

   174   options [document_graph]

   175   theories HOL_Light_Maps

   176   theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import

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

   179   description {*

   180     Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler

   181     Theorem, Wilson's Theorem, some lemmas for Quadratic Reciprocity.

   182   *}

   183   options [document_graph]

   184   theories [document = false]

   185     "~~/src/HOL/Library/FuncSet"

   186     "~~/src/HOL/Library/Multiset"

   187     "~~/src/HOL/Algebra/Ring"

   188     "~~/src/HOL/Algebra/FiniteProduct"

   189   theories

   190     Pocklington

   191     Gauss

   192     Number_Theory

   193     Euclidean_Algorithm

   194   document_files

   195     "root.tex"

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

   198   description {*

   199     Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler

   200     Theorem, Wilson's Theorem, Quadratic Reciprocity.

   201   *}

   202   options [document_graph]

   203   theories [document = false]

   204     "~~/src/HOL/Library/Infinite_Set"

   205     "~~/src/HOL/Library/Permutation"

   206   theories

   207     Fib

   208     Factorization

   209     Chinese

   210     WilsonRuss

   211     WilsonBij

   212     Quadratic_Reciprocity

   213     Primes

   214     Pocklington

   215   document_files

   216     "root.bib"

   217     "root.tex"

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

   220   description {*

   221     Verification of imperative programs (verification conditions are generated

   222     automatically from pre/post conditions and loop invariants).

   223   *}

   224   theories Hoare

   225   document_files "root.bib" "root.tex"

   227 session "HOL-Hoare_Parallel" in Hoare_Parallel = HOL +

   228   description {*

   229     Verification of shared-variable imperative programs a la Owicki-Gries.

   230     (verification conditions are generated automatically).

   231   *}

   232   options [document_graph]

   233   theories Hoare_Parallel

   234   document_files "root.bib" "root.tex"

   236 session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" +

   237   options [document = false, document_graph = false, browser_info = false]

   238   theories

   239     Generate

   240     Generate_Binary_Nat

   241     Generate_Target_Nat

   242     Generate_Efficient_Datastructures

   243     Generate_Pretty_Char

   244   theories [condition = ISABELLE_GHC]

   245     Code_Test_GHC

   246   theories [condition = ISABELLE_MLTON]

   247     Code_Test_MLton

   248   theories [condition = ISABELLE_OCAMLC]

   249     Code_Test_OCaml

   250   theories [condition = ISABELLE_POLYML]

   251     Code_Test_PolyML

   252   theories [condition = ISABELLE_SCALA]

   253     Code_Test_Scala

   254   theories [condition = ISABELLE_SMLNJ]

   255     Code_Test_SMLNJ

   257 session "HOL-Metis_Examples" in Metis_Examples = HOL +

   258   description {*

   259     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

   260     Author:     Jasmin Blanchette, TU Muenchen

   262     Testing Metis and Sledgehammer.

   263   *}

   264   options [document = false]

   265   theories

   266     Abstraction

   267     Big_O

   268     Binary_Tree

   269     Clausification

   270     Message

   271     Proxies

   272     Tarski

   273     Trans_Closure

   274     Sets

   276 session "HOL-Nitpick_Examples" in Nitpick_Examples = HOL +

   277   description {*

   278     Author:     Jasmin Blanchette, TU Muenchen

   279     Copyright   2009

   280   *}

   281   options [document = false]

   282   theories [quick_and_dirty] Nitpick_Examples

   284 session "HOL-Algebra" (main) in Algebra = HOL +

   285   description {*

   286     Author: Clemens Ballarin, started 24 September 1999

   288     The Isabelle Algebraic Library.

   289   *}

   290   options [document_graph]

   291   theories [document = false]

   292     (* Preliminaries from set and number theory *)

   293     "~~/src/HOL/Library/FuncSet"

   294     "~~/src/HOL/Number_Theory/Primes"

   295     "~~/src/HOL/Number_Theory/Binomial"

   296     "~~/src/HOL/Library/Permutation"

   297   theories

   298     (*** New development, based on explicit structures ***)

   299     (* Groups *)

   300     FiniteProduct        (* Product operator for commutative groups *)

   301     Sylow                (* Sylow's theorem *)

   302     Bij                  (* Automorphism Groups *)

   304     (* Rings *)

   305     Divisibility         (* Rings *)

   306     IntRing              (* Ideals and residue classes *)

   307     UnivPoly             (* Polynomials *)

   308   document_files "root.bib" "root.tex"

   310 session "HOL-Auth" in Auth = HOL +

   311   description {*

   312     A new approach to verifying authentication protocols.

   313   *}

   314   options [document_graph]

   315   theories

   316     Auth_Shared

   317     Auth_Public

   318     "Smartcard/Auth_Smartcard"

   319     "Guard/Auth_Guard_Shared"

   320     "Guard/Auth_Guard_Public"

   321   document_files "root.tex"

   323 session "HOL-UNITY" in UNITY = "HOL-Auth" +

   324   description {*

   325     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

   326     Copyright   1998  University of Cambridge

   328     Verifying security protocols using Chandy and Misra's UNITY formalism.

   329   *}

   330   options [document_graph]

   331   theories

   332     (*Basic meta-theory*)

   333     "UNITY_Main"

   335     (*Simple examples: no composition*)

   336     "Simple/Deadlock"

   337     "Simple/Common"

   338     "Simple/Network"

   339     "Simple/Token"

   340     "Simple/Channel"

   341     "Simple/Lift"

   342     "Simple/Mutex"

   343     "Simple/Reach"

   344     "Simple/Reachability"

   346     (*Verifying security protocols using UNITY*)

   347     "Simple/NSP_Bad"

   349     (*Example of composition*)

   350     "Comp/Handshake"

   352     (*Universal properties examples*)

   353     "Comp/Counter"

   354     "Comp/Counterc"

   355     "Comp/Priority"

   357     "Comp/TimerArray"

   358     "Comp/Progress"

   360     "Comp/Alloc"

   361     "Comp/AllocImpl"

   362     "Comp/Client"

   364     (*obsolete*)

   365     "ELT"

   366   document_files "root.tex"

   368 session "HOL-Unix" in Unix = HOL +

   369   options [print_mode = "no_brackets,no_type_brackets"]

   370   theories Unix

   371   document_files "root.bib" "root.tex"

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

   374   theories MainZF Games

   375   document_files "root.tex"

   377 session "HOL-Imperative_HOL" in Imperative_HOL = HOL +

   378   options [document_graph, print_mode = "iff,no_brackets"]

   379   theories [document = false]

   380     "~~/src/HOL/Library/Countable"

   381     "~~/src/HOL/Library/Monad_Syntax"

   382     "~~/src/HOL/Library/LaTeXsugar"

   383   theories Imperative_HOL_ex

   384   document_files "root.bib" "root.tex"

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

   387   description {*

   388     Various decision procedures, typically involving reflection.

   389   *}

   390   options [condition = ML_SYSTEM_POLYML, document = false]

   391   theories Decision_Procs

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

   394   options [document = false, parallel_proofs = 0]

   395   theories

   396     Hilbert_Classical

   397     XML_Data

   399 session "HOL-Proofs-Extraction" in "Proofs/Extraction" = "HOL-Proofs" +

   400   description {*

   401     Examples for program extraction in Higher-Order Logic.

   402   *}

   403   options [condition = ML_SYSTEM_POLYML, parallel_proofs = 0, quick_and_dirty = false]

   404   theories [document = false]

   405     "~~/src/HOL/Library/Code_Target_Numeral"

   406     "~~/src/HOL/Library/Monad_Syntax"

   407     "~~/src/HOL/Number_Theory/Primes"

   408     "~~/src/HOL/Number_Theory/UniqueFactorization"

   409     "~~/src/HOL/Library/State_Monad"

   410   theories

   411     Greatest_Common_Divisor

   412     Warshall

   413     Higman_Extraction

   414     Pigeonhole

   415     Euclid

   416   document_files "root.bib" "root.tex"

   418 session "HOL-Proofs-Lambda" in "Proofs/Lambda" = "HOL-Proofs" +

   419   description {*

   420     Lambda Calculus in de Bruijn's Notation.

   422     This session defines lambda-calculus terms with de Bruijn indixes and

   423     proves confluence of beta, eta and beta+eta.

   425     The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole

   426     theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html).

   427   *}

   428   options [document_graph, print_mode = "no_brackets", parallel_proofs = 0,

   429     quick_and_dirty = false]

   430   theories [document = false]

   431     "~~/src/HOL/Library/Code_Target_Int"

   432   theories

   433     Eta

   434     StrongNorm

   435     Standardization

   436     WeakNorm

   437   document_files "root.bib" "root.tex"

   439 session "HOL-Prolog" in Prolog = HOL +

   440   description {*

   441     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)

   443     A bare-bones implementation of Lambda-Prolog.

   445     This is a simple exploratory implementation of Lambda-Prolog in HOL,

   446     including some minimal examples (in Test.thy) and a more typical example of

   447     a little functional language and its type system.

   448   *}

   449   options [document = false]

   450   theories Test Type

   452 session "HOL-MicroJava" in MicroJava = HOL +

   453   description {*

   454     Formalization of a fragment of Java, together with a corresponding virtual

   455     machine and a specification of its bytecode verifier and a lightweight

   456     bytecode verifier, including proofs of type-safety.

   457   *}

   458   options [document_graph]

   459   theories [document = false] "~~/src/HOL/Library/While_Combinator"

   460   theories MicroJava

   461   document_files

   462     "introduction.tex"

   463     "root.bib"

   464     "root.tex"

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

   467   description {*

   468     Hoare Logic for a tiny fragment of Java.

   469   *}

   470   options [document_graph]

   471   theories Example

   472   document_files "root.bib" "root.tex"

   474 session "HOL-Bali" in Bali = HOL +

   475   options [document_graph]

   476   theories

   477     AxExample

   478     AxSound

   479     AxCompl

   480     Trans

   481   document_files "root.tex"

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

   484   description {*

   485     Author:     Tobias Nipkow and Konrad Slind and Olaf Müller

   486     Copyright   1994--1996  TU Muenchen

   488     The meta-theory of I/O-Automata in HOL. This formalization has been

   489     significantly changed and extended, see HOLCF/IOA. There are also the

   490     proofs of two communication protocols which formerly have been here.

   492     @inproceedings{Nipkow-Slind-IOA,

   493     author={Tobias Nipkow and Konrad Slind},

   494     title={{I/O} Automata in {Isabelle/HOL}},

   495     booktitle={Proc.\ TYPES Workshop 1994},

   496     publisher=Springer,

   497     series=LNCS,

   498     note={To appear}}

   499     ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz

   501     and

   503     @inproceedings{Mueller-Nipkow,

   504     author={Olaf M\"uller and Tobias Nipkow},

   505     title={Combining Model Checking and Deduction for {I/O}-Automata},

   506     booktitle={Proc.\ TACAS Workshop},

   507     organization={Aarhus University, BRICS report},

   508     year=1995}

   509     ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz

   510   *}

   511   options [document = false]

   512   theories Solve

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

   515   description {*

   516     Author:     Markus Wenzel, TU Muenchen

   518     Basic theory of lattices and orders.

   519   *}

   520   theories CompleteLattice

   521   document_files "root.tex"

   523 session "HOL-ex" in ex = HOL +

   524   description {*

   525     Miscellaneous examples for Higher-Order Logic.

   526   *}

   527   options [condition = ML_SYSTEM_POLYML]

   528   theories [document = false]

   529     "~~/src/HOL/Library/State_Monad"

   530     Code_Binary_Nat_examples

   531     "~~/src/HOL/Library/FuncSet"

   532     Eval_Examples

   533     Normalization_by_Evaluation

   534     Hebrew

   535     Chinese

   536     Serbian

   537     "~~/src/HOL/Library/FinFun_Syntax"

   538     "~~/src/HOL/Library/Refute"

   539     "~~/src/HOL/Library/Transitive_Closure_Table"

   540     Cartouche_Examples

   541   theories

   542     Commands

   543     Adhoc_Overloading_Examples

   544     Iff_Oracle

   545     Coercion_Examples

   546     Higher_Order_Logic

   547     Abstract_NAT

   548     Guess

   549     Fundefs

   550     Induction_Schema

   551     LocaleTest2

   552     Records

   553     While_Combinator_Example

   554     MonoidGroup

   555     BinEx

   556     Hex_Bin_Examples

   557     Antiquote

   558     Multiquote

   559     PER

   560     NatSum

   561     ThreeDivides

   562     Intuitionistic

   563     CTL

   564     Arith_Examples

   565     BT

   566     Tree23

   567     Bubblesort

   568     MergeSort

   569     Lagrange

   570     Groebner_Examples

   571     MT

   572     Unification

   573     Primrec

   574     Tarski

   575     Classical

   576     Set_Theory

   577     Termination

   578     Coherent

   579     PresburgerEx

   580     Reflection_Examples

   581     Sqrt

   582     Sqrt_Script

   583     Transfer_Ex

   584     Transfer_Int_Nat

   585     Transitive_Closure_Table_Ex

   586     HarmonicSeries

   587     Refute_Examples

   588     Execute_Choice

   589     Gauge_Integration

   590     Dedekind_Real

   591     Quicksort

   592     Birthday_Paradox

   593     List_to_Set_Comprehension_Examples

   594     Seq

   595     Simproc_Tests

   596     Executable_Relation

   597     FinFunPred

   598     Set_Comprehension_Pointfree_Examples

   599     Parallel_Example

   600     IArray_Examples

   601     SVC_Oracle

   602     Simps_Case_Conv_Examples

   603     ML

   604     SAT_Examples

   605     SOS

   606     SOS_Cert

   607   theories [skip_proofs = false]

   608     Meson_Test

   609   theories [condition = SVC_HOME]

   610     svc_test

   611   theories [condition = ISABELLE_FULL_TEST]

   612     Sudoku

   613   document_files "root.bib" "root.tex"

   615 session "HOL-Isar_Examples" in Isar_Examples = HOL +

   616   description {*

   617     Miscellaneous Isabelle/Isar examples for Higher-Order Logic.

   618   *}

   619   theories [document = false]

   620     "~~/src/HOL/Library/Lattice_Syntax"

   621     "../Number_Theory/Primes"

   622   theories

   623     Basic_Logic

   624     Cantor

   625     Drinker

   626     Expr_Compiler

   627     Fibonacci

   628     Group

   629     Group_Context

   630     Group_Notepad

   631     Hoare_Ex

   632     Knaster_Tarski

   633     Mutilated_Checkerboard

   634     Nested_Datatype

   635     Peirce

   636     Puzzle

   637     Summation

   638   document_files

   639     "root.bib"

   640     "root.tex"

   641     "style.tex"

   643 session "HOL-SET_Protocol" in SET_Protocol = HOL +

   644   description {*

   645     Verification of the SET Protocol.

   646   *}

   647   options [document_graph]

   648   theories [document = false] "~~/src/HOL/Library/Nat_Bijection"

   649   theories SET_Protocol

   650   document_files "root.tex"

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

   653   description {*

   654     Two-dimensional matrices and linear programming.

   655   *}

   656   options [document_graph]

   657   theories Cplex

   658   document_files "root.tex"

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

   661   description {*

   662     Lamport's Temporal Logic of Actions.

   663   *}

   664   options [document = false]

   665   theories TLA

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

   668   options [document = false]

   669   theories Inc

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

   672   options [document = false]

   673   theories DBuffer

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

   676   options [document = false]

   677   theories MemoryImplementation

   679 session "HOL-TPTP" in TPTP = HOL +

   680   description {*

   681     Author:     Jasmin Blanchette, TU Muenchen

   682     Author:     Nik Sultana, University of Cambridge

   683     Copyright   2011

   685     TPTP-related extensions.

   686   *}

   687   options [document = false]

   688   theories

   689     ATP_Theory_Export

   690     MaSh_Eval

   691     TPTP_Interpret

   692     THF_Arith

   693     TPTP_Proof_Reconstruction

   694   theories

   695     ATP_Problem_Import

   697 session "HOL-Multivariate_Analysis" (main) in Multivariate_Analysis = HOL +

   698   options [document_graph]

   699   theories

   700     Multivariate_Analysis

   701     Determinants

   702     PolyRoots

   703     Complex_Analysis_Basics

   704   document_files

   705     "root.tex"

   707 session "HOL-Probability" in "Probability" = "HOL-Multivariate_Analysis" +

   708   options [document_graph]

   709   theories [document = false]

   710     "~~/src/HOL/Library/Countable"

   711     "~~/src/HOL/Library/Permutation"

   712     "~~/src/HOL/Library/Order_Continuity"

   713     "~~/src/HOL/Library/Diagonal_Subsequence"

   714   theories

   715     Probability

   716     "ex/Dining_Cryptographers"

   717     "ex/Koepf_Duermuth_Countermeasure"

   718     "ex/Measure_Not_CCC"

   719   document_files "root.tex"

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

   722   options [document = false]

   723   theories Nominal

   725 session "HOL-Nominal-Examples" in "Nominal/Examples" = "HOL-Nominal" +

   726   options [condition = ML_SYSTEM_POLYML, document = false]

   727   theories

   728     Nominal_Examples_Base

   729   theories [condition = ISABELLE_FULL_TEST]

   730     Nominal_Examples

   731   theories [quick_and_dirty]

   732     VC_Condition

   734 session "HOL-Cardinals" in Cardinals = HOL +

   735   description {*

   736     Ordinals and Cardinals, Full Theories.

   737   *}

   738   options [document = false]

   739   theories Cardinals

   740   document_files

   741     "intro.tex"

   742     "root.tex"

   743     "root.bib"

   745 session "HOL-Datatype_Examples" in Datatype_Examples = HOL +

   746   description {*

   747     (Co)datatype Examples, including large ones from John Harrison.

   748   *}

   749   options [document = false]

   750   theories

   751     "~~/src/HOL/Library/Old_Datatype"

   752     Compat

   753     Lambda_Term

   754     Process

   755     TreeFsetI

   756     "Derivation_Trees/Gram_Lang"

   757     "Derivation_Trees/Parallel"

   758     Koenig

   759     Stream_Processor

   760     Misc_Codatatype

   761     Misc_Datatype

   762     Misc_Primcorec

   763     Misc_Primrec

   764   theories [condition = ISABELLE_FULL_TEST]

   765     Brackin

   766     IsaFoR

   767     Misc_N2M

   769 session "HOL-Word" (main) in Word = HOL +

   770   options [document_graph]

   771   theories Word

   772   document_files "root.bib" "root.tex"

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

   775   options [document = false]

   776   theories WordExamples

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

   779   theories [skip_proofs = false]

   780     StateSpaceEx

   781   document_files "root.tex"

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

   784   description {*

   785     Nonstandard analysis.

   786   *}

   787   options [document_graph]

   788   theories Hypercomplex

   789   document_files "root.tex"

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

   792   options [document = false]

   793   theories NSPrimes

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

   796   options [document = false]

   797   theories Mirabelle_Test

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

   800   options [document = false, timeout = 60]

   801   theories Ex

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

   804   options [document = false, quick_and_dirty]

   805   theories

   806     Boogie

   807     SMT_Examples

   808     SMT_Word_Examples

   809   theories [condition = ISABELLE_FULL_TEST]

   810     SMT_Tests

   811   files

   812     "Boogie_Dijkstra.certs"

   813     "Boogie_Max.certs"

   814     "SMT_Examples.certs"

   815     "SMT_Word_Examples.certs"

   816     "VCC_Max.certs"

   818 session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" +

   819   options [document = false]

   820   theories SPARK

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

   823   options [document = false]

   824   theories

   825     "Gcd/Greatest_Common_Divisor"

   827     "Liseq/Longest_Increasing_Subsequence"

   829     "RIPEMD-160/F"

   830     "RIPEMD-160/Hash"

   831     "RIPEMD-160/K_L"

   832     "RIPEMD-160/K_R"

   833     "RIPEMD-160/R_L"

   834     "RIPEMD-160/Round"

   835     "RIPEMD-160/R_R"

   836     "RIPEMD-160/S_L"

   837     "RIPEMD-160/S_R"

   839     "Sqrt/Sqrt"

   840   files

   841     "Gcd/greatest_common_divisor/g_c_d.fdl"

   842     "Gcd/greatest_common_divisor/g_c_d.rls"

   843     "Gcd/greatest_common_divisor/g_c_d.siv"

   844     "Liseq/liseq/liseq_length.fdl"

   845     "Liseq/liseq/liseq_length.rls"

   846     "Liseq/liseq/liseq_length.siv"

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   876   options [show_question_marks = false]

   877   theories

   878     Example_Verification

   879     VC_Principles

   880     Reference

   881     Complex_Types

   882   files

   883     "complex_types_app/initialize.fdl"

   884     "complex_types_app/initialize.rls"

   885     "complex_types_app/initialize.siv"

   886     "loop_invariant/proc1.fdl"

   887     "loop_invariant/proc1.rls"

   888     "loop_invariant/proc1.siv"

   889     "loop_invariant/proc2.fdl"

   890     "loop_invariant/proc2.rls"

   891     "loop_invariant/proc2.siv"

   892     "simple_greatest_common_divisor/g_c_d.fdl"

   893     "simple_greatest_common_divisor/g_c_d.rls"

   894     "simple_greatest_common_divisor/g_c_d.siv"

   895   document_files

   896     "complex_types.ads"

   897     "complex_types_app.adb"

   898     "complex_types_app.ads"

   899     "Gcd.adb"

   900     "Gcd.ads"

   901     "intro.tex"

   902     "loop_invariant.adb"

   903     "loop_invariant.ads"

   904     "root.bib"

   905     "root.tex"

   906     "Simple_Gcd.adb"

   907     "Simple_Gcd.ads"

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

   910   options [document = false]

   911   theories MutabelleExtra

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

   914   options [document = false]

   915   theories

   916     Quickcheck_Examples

   917     Quickcheck_Lattice_Examples

   918     Completeness

   919     Quickcheck_Interfaces

   920   theories [condition = ISABELLE_GHC]

   921     Hotel_Example

   922     Quickcheck_Narrowing_Examples

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

   925   theories [condition = ISABELLE_FULL_TEST, quick_and_dirty]

   926     Find_Unused_Assms_Examples

   927     Needham_Schroeder_No_Attacker_Example

   928     Needham_Schroeder_Guided_Attacker_Example

   929     Needham_Schroeder_Unguided_Attacker_Example

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

   932   description {*

   933     Author:     Cezary Kaliszyk and Christian Urban

   934   *}

   935   options [document = false]

   936   theories

   937     DList

   938     FSet

   939     Quotient_Int

   940     Quotient_Message

   941     Lift_FSet

   942     Lift_Set

   943     Lift_Fun

   944     Quotient_Rat

   945     Lift_DList

   946     Int_Pow

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

   949   options [document = false]

   950   theories

   951     Examples

   952     Predicate_Compile_Tests

   953     (* FIXME

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

   955     Specialisation_Examples

   956     IMP_1

   957     IMP_2

   958     (* FIXME since 21-Jul-2011

   959     Hotel_Example_Small_Generator

   960     IMP_3

   961     IMP_4 *)

   962   theories [condition = "ISABELLE_SWIPL"]

   963     Code_Prolog_Examples

   964     Context_Free_Grammar_Example

   965     Hotel_Example_Prolog

   966     Lambda_Example

   967     List_Examples

   968   theories [condition = "ISABELLE_SWIPL", quick_and_dirty]

   969     Reg_Exp_Example

   971 session HOLCF (main) in HOLCF = HOL +

   972   description {*

   973     Author:     Franz Regensburger

   974     Author:     Brian Huffman

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

   977   *}

   978   options [document_graph]

   979   theories [document = false]

   980     "~~/src/HOL/Library/Nat_Bijection"

   981     "~~/src/HOL/Library/Countable"

   982   theories

   983     Plain_HOLCF

   984     Fixrec

   985     HOLCF

   986   document_files "root.tex"

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

   989   theories

   990     Domain_ex

   991     Fixrec_ex

   992     New_Domain

   993   document_files "root.tex"

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

   996   options [document = false]

   997   theories HOLCF_Library

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

  1000   description {*

  1001     IMP -- A WHILE-language and its Semantics.

  1003     This is the HOLCF-based denotational semantics of a simple WHILE-language.

  1004   *}

  1005   options [document = false]

  1006   theories HoareEx

  1007   document_files "root.tex"

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

  1010   description {*

  1011     Miscellaneous examples for HOLCF.

  1012   *}

  1013   options [document = false]

  1014   theories

  1015     Dnat

  1016     Dagstuhl

  1017     Focus_ex

  1018     Fix2

  1019     Hoare

  1020     Concurrency_Monad

  1021     Loop

  1022     Powerdomain_ex

  1023     Domain_Proofs

  1024     Letrec

  1025     Pattern_Match

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

  1028   description {*

  1029     FOCUS: a theory of stream-processing functions Isabelle/HOLCF.

  1031     For introductions to FOCUS, see

  1033     "The Design of Distributed Systems - An Introduction to FOCUS"

  1034     http://www4.in.tum.de/publ/html.php?e=2

  1036     "Specification and Refinement of a Buffer of Length One"

  1037     http://www4.in.tum.de/publ/html.php?e=15

  1039     "Specification and Development of Interactive Systems: Focus on Streams,

  1040     Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321

  1041   *}

  1042   options [document = false]

  1043   theories

  1044     Fstreams

  1045     FOCUS

  1046     Buffer_adm

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

  1049   description {*

  1050     Author:     Olaf Mueller

  1051     Copyright   1997 TU München

  1053     A formalization of I/O automata in HOLCF.

  1055     The distribution contains simulation relations, temporal logic, and an

  1056     abstraction theory. Everything is based upon a domain-theoretic model of

  1057     finite and infinite sequences.

  1058   *}

  1059   options [document = false]

  1060   theories "meta_theory/Abstraction"

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

  1063   description {*

  1064     Author:     Olaf Mueller

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

  1067   *}

  1068   options [document = false]

  1069   theories Correctness

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

  1072   description {*

  1073     Author:     Tobias Nipkow & Konrad Slind

  1075     A network transmission protocol, performed in the

  1076     I/O automata formalization by Olaf Mueller.

  1077   *}

  1078   options [document = false]

  1079   theories Correctness

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

  1082   description {*

  1083     Author:     Olaf Mueller

  1085     Memory storage case study.

  1086   *}

  1087   options [document = false]

  1088   theories Correctness

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

  1091   description {*

  1092     Author:     Olaf Mueller

  1093   *}

  1094   options [document = false]

  1095   theories

  1096     TrivEx

  1097     TrivEx2

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

  1100   description {*

  1101     Some benchmark on large record.

  1102   *}

  1103   options [document = false]

  1104   theories [condition = ISABELLE_FULL_TEST]

  1105     Record_Benchmark

author	hoelzl
	Wed Dec 17 16:10:30 2014 +0100 (2014-12-17)
changeset 59144	c9b75c03de3c
parent 59090	a0a05a4edb36
child 59162	dca5594761f2
permissions	-rw-r--r--