isabelle: src/HOL/ROOT@a0a05a4edb36

     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   document_files "root.tex"

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

   721   options [document = false]

   722   theories Nominal

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

   725   options [condition = ML_SYSTEM_POLYML, document = false]

   726   theories

   727     Nominal_Examples_Base

   728   theories [condition = ISABELLE_FULL_TEST]

   729     Nominal_Examples

   730   theories [quick_and_dirty]

   731     VC_Condition

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

   734   description {*

   735     Ordinals and Cardinals, Full Theories.

   736   *}

   737   options [document = false]

   738   theories Cardinals

   739   document_files

   740     "intro.tex"

   741     "root.tex"

   742     "root.bib"

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

   745   description {*

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

   747   *}

   748   options [document = false]

   749   theories

   750     "~~/src/HOL/Library/Old_Datatype"

   751     Compat

   752     Lambda_Term

   753     Process

   754     TreeFsetI

   755     "Derivation_Trees/Gram_Lang"

   756     "Derivation_Trees/Parallel"

   757     Koenig

   758     Stream_Processor

   759     Misc_Codatatype

   760     Misc_Datatype

   761     Misc_Primcorec

   762     Misc_Primrec

   763   theories [condition = ISABELLE_FULL_TEST]

   764     Brackin

   765     IsaFoR

   766     Misc_N2M

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

   769   options [document_graph]

   770   theories Word

   771   document_files "root.bib" "root.tex"

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

   774   options [document = false]

   775   theories WordExamples

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

   778   theories [skip_proofs = false]

   779     StateSpaceEx

   780   document_files "root.tex"

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

   783   description {*

   784     Nonstandard analysis.

   785   *}

   786   options [document_graph]

   787   theories Hypercomplex

   788   document_files "root.tex"

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

   791   options [document = false]

   792   theories NSPrimes

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

   795   options [document = false]

   796   theories Mirabelle_Test

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

   799   options [document = false, timeout = 60]

   800   theories Ex

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

   803   options [document = false, quick_and_dirty]

   804   theories

   805     Boogie

   806     SMT_Examples

   807     SMT_Word_Examples

   808   theories [condition = ISABELLE_FULL_TEST]

   809     SMT_Tests

   810   files

   811     "Boogie_Dijkstra.certs"

   812     "Boogie_Max.certs"

   813     "SMT_Examples.certs"

   814     "SMT_Word_Examples.certs"

   815     "VCC_Max.certs"

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

   818   options [document = false]

   819   theories SPARK

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

   822   options [document = false]

   823   theories

   824     "Gcd/Greatest_Common_Divisor"

   826     "Liseq/Longest_Increasing_Subsequence"

   828     "RIPEMD-160/F"

   829     "RIPEMD-160/Hash"

   830     "RIPEMD-160/K_L"

   831     "RIPEMD-160/K_R"

   832     "RIPEMD-160/R_L"

   833     "RIPEMD-160/Round"

   834     "RIPEMD-160/R_R"

   835     "RIPEMD-160/S_L"

   836     "RIPEMD-160/S_R"

   838     "Sqrt/Sqrt"

   839   files

   840     "Gcd/greatest_common_divisor/g_c_d.fdl"

   841     "Gcd/greatest_common_divisor/g_c_d.rls"

   842     "Gcd/greatest_common_divisor/g_c_d.siv"

   843     "Liseq/liseq/liseq_length.fdl"

   844     "Liseq/liseq/liseq_length.rls"

   845     "Liseq/liseq/liseq_length.siv"

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   875   options [show_question_marks = false]

   876   theories

   877     Example_Verification

   878     VC_Principles

   879     Reference

   880     Complex_Types

   881   files

   882     "complex_types_app/initialize.fdl"

   883     "complex_types_app/initialize.rls"

   884     "complex_types_app/initialize.siv"

   885     "loop_invariant/proc1.fdl"

   886     "loop_invariant/proc1.rls"

   887     "loop_invariant/proc1.siv"

   888     "loop_invariant/proc2.fdl"

   889     "loop_invariant/proc2.rls"

   890     "loop_invariant/proc2.siv"

   891     "simple_greatest_common_divisor/g_c_d.fdl"

   892     "simple_greatest_common_divisor/g_c_d.rls"

   893     "simple_greatest_common_divisor/g_c_d.siv"

   894   document_files

   895     "complex_types.ads"

   896     "complex_types_app.adb"

   897     "complex_types_app.ads"

   898     "Gcd.adb"

   899     "Gcd.ads"

   900     "intro.tex"

   901     "loop_invariant.adb"

   902     "loop_invariant.ads"

   903     "root.bib"

   904     "root.tex"

   905     "Simple_Gcd.adb"

   906     "Simple_Gcd.ads"

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

   909   options [document = false]

   910   theories MutabelleExtra

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

   913   options [document = false]

   914   theories

   915     Quickcheck_Examples

   916     Quickcheck_Lattice_Examples

   917     Completeness

   918     Quickcheck_Interfaces

   919   theories [condition = ISABELLE_GHC]

   920     Hotel_Example

   921     Quickcheck_Narrowing_Examples

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

   924   theories [condition = ISABELLE_FULL_TEST, quick_and_dirty]

   925     Find_Unused_Assms_Examples

   926     Needham_Schroeder_No_Attacker_Example

   927     Needham_Schroeder_Guided_Attacker_Example

   928     Needham_Schroeder_Unguided_Attacker_Example

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

   931   description {*

   932     Author:     Cezary Kaliszyk and Christian Urban

   933   *}

   934   options [document = false]

   935   theories

   936     DList

   937     FSet

   938     Quotient_Int

   939     Quotient_Message

   940     Lift_FSet

   941     Lift_Set

   942     Lift_Fun

   943     Quotient_Rat

   944     Lift_DList

   945     Int_Pow

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

   948   options [document = false]

   949   theories

   950     Examples

   951     Predicate_Compile_Tests

   952     (* FIXME

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

   954     Specialisation_Examples

   955     IMP_1

   956     IMP_2

   957     (* FIXME since 21-Jul-2011

   958     Hotel_Example_Small_Generator

   959     IMP_3

   960     IMP_4 *)

   961   theories [condition = "ISABELLE_SWIPL"]

   962     Code_Prolog_Examples

   963     Context_Free_Grammar_Example

   964     Hotel_Example_Prolog

   965     Lambda_Example

   966     List_Examples

   967   theories [condition = "ISABELLE_SWIPL", quick_and_dirty]

   968     Reg_Exp_Example

   970 session HOLCF (main) in HOLCF = HOL +

   971   description {*

   972     Author:     Franz Regensburger

   973     Author:     Brian Huffman

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

   976   *}

   977   options [document_graph]

   978   theories [document = false]

   979     "~~/src/HOL/Library/Nat_Bijection"

   980     "~~/src/HOL/Library/Countable"

   981   theories

   982     Plain_HOLCF

   983     Fixrec

   984     HOLCF

   985   document_files "root.tex"

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

   988   theories

   989     Domain_ex

   990     Fixrec_ex

   991     New_Domain

   992   document_files "root.tex"

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

   995   options [document = false]

   996   theories HOLCF_Library

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

   999   description {*

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

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

  1003   *}

  1004   options [document = false]

  1005   theories HoareEx

  1006   document_files "root.tex"

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

  1009   description {*

  1010     Miscellaneous examples for HOLCF.

  1011   *}

  1012   options [document = false]

  1013   theories

  1014     Dnat

  1015     Dagstuhl

  1016     Focus_ex

  1017     Fix2

  1018     Hoare

  1019     Concurrency_Monad

  1020     Loop

  1021     Powerdomain_ex

  1022     Domain_Proofs

  1023     Letrec

  1024     Pattern_Match

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

  1027   description {*

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

  1030     For introductions to FOCUS, see

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

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

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

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

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

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

  1040   *}

  1041   options [document = false]

  1042   theories

  1043     Fstreams

  1044     FOCUS

  1045     Buffer_adm

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

  1048   description {*

  1049     Author:     Olaf Mueller

  1050     Copyright   1997 TU München

  1052     A formalization of I/O automata in HOLCF.

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

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

  1056     finite and infinite sequences.

  1057   *}

  1058   options [document = false]

  1059   theories "meta_theory/Abstraction"

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

  1062   description {*

  1063     Author:     Olaf Mueller

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

  1066   *}

  1067   options [document = false]

  1068   theories Correctness

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

  1071   description {*

  1072     Author:     Tobias Nipkow & Konrad Slind

  1074     A network transmission protocol, performed in the

  1075     I/O automata formalization by Olaf Mueller.

  1076   *}

  1077   options [document = false]

  1078   theories Correctness

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

  1081   description {*

  1082     Author:     Olaf Mueller

  1084     Memory storage case study.

  1085   *}

  1086   options [document = false]

  1087   theories Correctness

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

  1090   description {*

  1091     Author:     Olaf Mueller

  1092   *}

  1093   options [document = false]

  1094   theories

  1095     TrivEx

  1096     TrivEx2

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

  1099   description {*

  1100     Some benchmark on large record.

  1101   *}

  1102   options [document = false]

  1103   theories [condition = ISABELLE_FULL_TEST]

  1104     Record_Benchmark

author	wenzelm
	Thu Dec 04 20:56:38 2014 +0100 (2014-12-04)
changeset 59090	a0a05a4edb36
parent 59006	272d7fb92396
child 59144	c9b75c03de3c
permissions	-rw-r--r--