wneuper/isa: src/HOL/ROOT@8dd9df88f647

     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]

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

    24   theories Main

    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_Recdef

    55   theories [condition = ISABELLE_FULL_TEST]

    56     Sum_of_Squares_Remote

    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     HREF="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 [quick_and_dirty]

    99     Common_Patterns

   100   theories

   101     QuoDataType

   102     QuoNestedDataType

   103     Term

   104     SList

   105     ABexp

   106     Tree

   107     Ordinals

   108     Sigma_Algebra

   109     Comb

   110     PropLog

   111     Com

   112   document_files "root.tex"

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

   115   options [document_graph, document_variants=document]

   116   theories [document = false]

   117     "~~/src/Tools/Permanent_Interpretation"

   118     "~~/src/HOL/Library/While_Combinator"

   119     "~~/src/HOL/Library/Char_ord"

   120     "~~/src/HOL/Library/List_lexord"

   121     "~~/src/HOL/Library/Quotient_List"

   122     "~~/src/HOL/Library/Extended"

   123   theories

   124     BExp

   125     ASM

   126     Finite_Reachable

   127     Denotational

   128     Compiler2

   129     Poly_Types

   130     Sec_Typing

   131     Sec_TypingT

   132     Def_Init_Big

   133     Def_Init_Small

   134     Fold

   135     Live

   136     Live_True

   137     Hoare_Examples

   138     VCG

   139     Hoare_Total

   140     Collecting1

   141     Collecting_Examples

   142     Abs_Int_Tests

   143     Abs_Int1_parity

   144     Abs_Int1_const

   145     Abs_Int3

   146     "Abs_Int_ITP/Abs_Int1_parity_ITP"

   147     "Abs_Int_ITP/Abs_Int1_const_ITP"

   148     "Abs_Int_ITP/Abs_Int3_ITP"

   149     "Abs_Int_Den/Abs_Int_den2"

   150     Procs_Dyn_Vars_Dyn

   151     Procs_Stat_Vars_Dyn

   152     Procs_Stat_Vars_Stat

   153     C_like

   154     OO

   155   document_files "root.bib" "root.tex"

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

   158   description {*

   159     Author:     David von Oheimb

   160     Copyright   1999 TUM

   162     IMPP -- An imperative language with procedures.

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

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

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

   167   *}

   168   options [document = false]

   169   theories EvenOdd

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

   172   options [document_graph]

   173   theories HOL_Light_Maps

   174   theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import

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

   177   description {*

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

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

   180   *}

   181   options [document_graph]

   182   theories [document = false]

   183     "~~/src/HOL/Library/FuncSet"

   184     "~~/src/HOL/Library/Multiset"

   185     "~~/src/HOL/Algebra/Ring"

   186     "~~/src/HOL/Algebra/FiniteProduct"

   187   theories

   188     Pocklington

   189     Gauss

   190     Number_Theory

   191   document_files

   192     "root.tex"

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

   195   description {*

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

   197     Theorem, Wilson's Theorem, Quadratic Reciprocity.

   198   *}

   199   options [document_graph]

   200   theories [document = false]

   201     "~~/src/HOL/Library/Infinite_Set"

   202     "~~/src/HOL/Library/Permutation"

   203   theories

   204     Fib

   205     Factorization

   206     Chinese

   207     WilsonRuss

   208     WilsonBij

   209     Quadratic_Reciprocity

   210     Primes

   211     Pocklington

   212   document_files "root.tex"

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

   215   description {*

   216     Verification of imperative programs (verification conditions are generated

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

   218   *}

   219   theories Hoare

   220   document_files "root.bib" "root.tex"

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

   223   description {*

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

   225     (verification conditions are generated automatically).

   226   *}

   227   options [document_graph]

   228   theories Hoare_Parallel

   229   document_files "root.bib" "root.tex"

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

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

   233   theories

   234     Generate

   235     Generate_Binary_Nat

   236     Generate_Target_Nat

   237     Generate_Efficient_Datastructures

   238     Generate_Pretty_Char

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

   241   description {*

   242     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

   243     Author:     Jasmin Blanchette, TU Muenchen

   245     Testing Metis and Sledgehammer.

   246   *}

   247   options [timeout = 3600, document = false]

   248   theories

   249     Abstraction

   250     Big_O

   251     Binary_Tree

   252     Clausification

   253     Message

   254     Proxies

   255     Tarski

   256     Trans_Closure

   257     Sets

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

   260   description {*

   261     Author:     Jasmin Blanchette, TU Muenchen

   262     Copyright   2009

   263   *}

   264   options [document = false]

   265   theories [quick_and_dirty] Nitpick_Examples

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

   268   description {*

   269     Author: Clemens Ballarin, started 24 September 1999

   271     The Isabelle Algebraic Library.

   272   *}

   273   options [document_graph]

   274   theories [document = false]

   275     (* Preliminaries from set and number theory *)

   276     "~~/src/HOL/Library/FuncSet"

   277     "~~/src/HOL/Number_Theory/Primes"

   278     "~~/src/HOL/Number_Theory/Binomial"

   279     "~~/src/HOL/Library/Permutation"

   280   theories

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

   282     (* Groups *)

   283     FiniteProduct        (* Product operator for commutative groups *)

   284     Sylow                (* Sylow's theorem *)

   285     Bij                  (* Automorphism Groups *)

   287     (* Rings *)

   288     Divisibility         (* Rings *)

   289     IntRing              (* Ideals and residue classes *)

   290     UnivPoly             (* Polynomials *)

   291   document_files "root.bib" "root.tex"

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

   294   description {*

   295     A new approach to verifying authentication protocols.

   296   *}

   297   options [document_graph]

   298   theories

   299     Auth_Shared

   300     Auth_Public

   301     "Smartcard/Auth_Smartcard"

   302     "Guard/Auth_Guard_Shared"

   303     "Guard/Auth_Guard_Public"

   304   document_files "root.tex"

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

   307   description {*

   308     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

   309     Copyright   1998  University of Cambridge

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

   312   *}

   313   options [document_graph]

   314   theories

   315     (*Basic meta-theory*)

   316     "UNITY_Main"

   318     (*Simple examples: no composition*)

   319     "Simple/Deadlock"

   320     "Simple/Common"

   321     "Simple/Network"

   322     "Simple/Token"

   323     "Simple/Channel"

   324     "Simple/Lift"

   325     "Simple/Mutex"

   326     "Simple/Reach"

   327     "Simple/Reachability"

   329     (*Verifying security protocols using UNITY*)

   330     "Simple/NSP_Bad"

   332     (*Example of composition*)

   333     "Comp/Handshake"

   335     (*Universal properties examples*)

   336     "Comp/Counter"

   337     "Comp/Counterc"

   338     "Comp/Priority"

   340     "Comp/TimerArray"

   341     "Comp/Progress"

   343     "Comp/Alloc"

   344     "Comp/AllocImpl"

   345     "Comp/Client"

   347     (*obsolete*)

   348     "ELT"

   349   document_files "root.tex"

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

   352   options [print_mode = "no_brackets,no_type_brackets"]

   353   theories Unix

   354   document_files "root.bib" "root.tex"

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

   357   theories MainZF Games

   358   document_files "root.tex"

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

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

   362   theories [document = false]

   363     "~~/src/HOL/Library/Countable"

   364     "~~/src/HOL/Library/Monad_Syntax"

   365     "~~/src/HOL/Library/LaTeXsugar"

   366   theories Imperative_HOL_ex

   367   document_files "root.bib" "root.tex"

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

   370   description {*

   371     Various decision procedures, typically involving reflection.

   372   *}

   373   options [condition = ISABELLE_POLYML, document = false]

   374   theories Decision_Procs

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

   377   options [document = false, parallel_proofs = 0]

   378   theories

   379     Hilbert_Classical

   380     XML_Data

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

   383   description {*

   384     Examples for program extraction in Higher-Order Logic.

   385   *}

   386   options [condition = ISABELLE_POLYML, parallel_proofs = 0]

   387   theories [document = false]

   388     "~~/src/HOL/Library/Code_Target_Numeral"

   389     "~~/src/HOL/Library/Monad_Syntax"

   390     "~~/src/HOL/Number_Theory/Primes"

   391     "~~/src/HOL/Number_Theory/UniqueFactorization"

   392     "~~/src/HOL/Library/State_Monad"

   393   theories

   394     Greatest_Common_Divisor

   395     Warshall

   396     Higman_Extraction

   397     Pigeonhole

   398     Euclid

   399   document_files "root.bib" "root.tex"

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

   402   description {*

   403     Lambda Calculus in de Bruijn's Notation.

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

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

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

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

   410   *}

   411   options [document_graph, print_mode = "no_brackets", parallel_proofs = 0]

   412   theories [document = false]

   413     "~~/src/HOL/Library/Code_Target_Int"

   414   theories

   415     Eta

   416     StrongNorm

   417     Standardization

   418     WeakNorm

   419   document_files "root.bib" "root.tex"

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

   422   description {*

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

   425     A bare-bones implementation of Lambda-Prolog.

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

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

   429     a little functional language and its type system.

   430   *}

   431   options [document = false]

   432   theories Test Type

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

   435   description {*

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

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

   438     bytecode verifier, including proofs of type-safety.

   439   *}

   440   options [document_graph]

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

   442   theories MicroJava

   443   document_files

   444     "introduction.tex"

   445     "root.bib"

   446     "root.tex"

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

   449   description {*

   450     Hoare Logic for a tiny fragment of Java.

   451   *}

   452   options [document_graph]

   453   theories Example

   454   document_files "root.bib" "root.tex"

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

   457   options [document_graph]

   458   theories

   459     AxExample

   460     AxSound

   461     AxCompl

   462     Trans

   463   document_files "root.tex"

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

   466   description {*

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

   468     Copyright   1994--1996  TU Muenchen

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

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

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

   474     @inproceedings{Nipkow-Slind-IOA,

   475     author={Tobias Nipkow and Konrad Slind},

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

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

   478     publisher=Springer,

   479     series=LNCS,

   480     note={To appear}}

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

   483     and

   485     @inproceedings{Mueller-Nipkow,

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

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

   488     booktitle={Proc.\ TACAS Workshop},

   489     organization={Aarhus University, BRICS report},

   490     year=1995}

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

   492   *}

   493   options [document = false]

   494   theories Solve

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

   497   description {*

   498     Author:     Markus Wenzel, TU Muenchen

   500     Basic theory of lattices and orders.

   501   *}

   502   theories CompleteLattice

   503   document_files "root.tex"

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

   506   description {*

   507     Miscellaneous examples for Higher-Order Logic.

   508   *}

   509   options [timeout = 3600, condition = ISABELLE_POLYML]

   510   theories [document = false]

   511     "~~/src/HOL/Library/State_Monad"

   512     Code_Binary_Nat_examples

   513     "~~/src/HOL/Library/FuncSet"

   514     Eval_Examples

   515     Normalization_by_Evaluation

   516     Hebrew

   517     Chinese

   518     Serbian

   519     "~~/src/HOL/Library/FinFun_Syntax"

   520     "~~/src/HOL/Library/Refute"

   521     Cartouche_Examples

   522   theories

   523     Iff_Oracle

   524     Coercion_Examples

   525     Higher_Order_Logic

   526     Abstract_NAT

   527     Guess

   528     Fundefs

   529     Induction_Schema

   530     LocaleTest2

   531     Records

   532     While_Combinator_Example

   533     MonoidGroup

   534     BinEx

   535     Hex_Bin_Examples

   536     Antiquote

   537     Multiquote

   538     PER

   539     NatSum

   540     ThreeDivides

   541     Intuitionistic

   542     CTL

   543     Arith_Examples

   544     BT

   545     Tree23

   546     MergeSort

   547     Lagrange

   548     Groebner_Examples

   549     MT

   550     Unification

   551     Primrec

   552     Tarski

   553     Classical

   554     Set_Theory

   555     Termination

   556     Coherent

   557     PresburgerEx

   558     Reflection_Examples

   559     Sqrt

   560     Sqrt_Script

   561     Transfer_Ex

   562     Transfer_Int_Nat

   563     HarmonicSeries

   564     Refute_Examples

   565     Execute_Choice

   566     Gauge_Integration

   567     Dedekind_Real

   568     Quicksort

   569     Birthday_Paradox

   570     List_to_Set_Comprehension_Examples

   571     Seq

   572     Simproc_Tests

   573     Executable_Relation

   574     FinFunPred

   575     Set_Comprehension_Pointfree_Examples

   576     Parallel_Example

   577     IArray_Examples

   578     SVC_Oracle

   579     Simps_Case_Conv_Examples

   580     ML

   581   theories [skip_proofs = false]

   582     Meson_Test

   583   theories [condition = SVC_HOME]

   584     svc_test

   585   theories [condition = ZCHAFF_HOME]

   586     (*requires zChaff (or some other reasonably fast SAT solver)*)

   587     Sudoku

   588 (* FIXME

   589 (*requires a proof-generating SAT solver (zChaff or MiniSAT)*)

   590     SAT_Examples

   591 *)

   592   document_files "root.bib" "root.tex"

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

   595   description {*

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

   597   *}

   598   theories [document = false]

   599     "~~/src/HOL/Library/Lattice_Syntax"

   600     "../Number_Theory/Primes"

   601   theories

   602     Basic_Logic

   603     Cantor

   604     Drinker

   605     Expr_Compiler

   606     Fibonacci

   607     Group

   608     Group_Context

   609     Group_Notepad

   610     Hoare_Ex

   611     Knaster_Tarski

   612     Mutilated_Checkerboard

   613     Nested_Datatype

   614     Peirce

   615     Puzzle

   616     Summation

   617   document_files

   618     "root.bib"

   619     "root.tex"

   620     "style.tex"

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

   623   description {*

   624     Verification of the SET Protocol.

   625   *}

   626   options [document_graph]

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

   628   theories SET_Protocol

   629   document_files "root.tex"

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

   632   description {*

   633     Two-dimensional matrices and linear programming.

   634   *}

   635   options [document_graph]

   636   theories Cplex

   637   document_files "root.tex"

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

   640   description {*

   641     Lamport's Temporal Logic of Actions.

   642   *}

   643   options [document = false]

   644   theories TLA

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

   647   options [document = false]

   648   theories Inc

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

   651   options [document = false]

   652   theories DBuffer

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

   655   options [document = false]

   656   theories MemoryImplementation

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

   659   description {*

   660     Author:     Jasmin Blanchette, TU Muenchen

   661     Author:     Nik Sultana, University of Cambridge

   662     Copyright   2011

   664     TPTP-related extensions.

   665   *}

   666   options [document = false]

   667   theories

   668     ATP_Theory_Export

   669     MaSh_Eval

   670     MaSh_Export

   671     TPTP_Interpret

   672     THF_Arith

   673     TPTP_Proof_Reconstruction

   674   theories

   675     ATP_Problem_Import

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

   678   options [document_graph]

   679   theories

   680     Multivariate_Analysis

   681     Determinants

   682     PolyRoots

   683     Complex_Analysis_Basics

   684   document_files

   685     "root.tex"

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

   688   options [document_graph]

   689   theories [document = false]

   690     "~~/src/HOL/Library/Countable"

   691     "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits"

   692     "~~/src/HOL/Library/Permutation"

   693   theories

   694     Probability

   695     "ex/Dining_Cryptographers"

   696     "ex/Koepf_Duermuth_Countermeasure"

   697   document_files "root.tex"

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

   700   options [document = false]

   701   theories Nominal

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

   704   options [timeout = 3600, condition = ISABELLE_POLYML, document = false]

   705   theories Nominal_Examples

   706   theories [quick_and_dirty] VC_Condition

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

   709   description {*

   710     Ordinals and Cardinals, Full Theories.

   711   *}

   712   options [document = false]

   713   theories Cardinals

   714   document_files

   715     "intro.tex"

   716     "root.tex"

   717     "root.bib"

   719 session "HOL-BNF_Examples" in BNF_Examples = HOL +

   720   description {*

   721     Examples for Bounded Natural Functors.

   722   *}

   723   options [document = false]

   724   theories

   725     Compat

   726     Lambda_Term

   727     Process

   728     TreeFsetI

   729     "Derivation_Trees/Gram_Lang"

   730     "Derivation_Trees/Parallel"

   731     Koenig

   732     Stream_Processor

   733     Misc_Codatatype

   734     Misc_Datatype

   735     Misc_Primcorec

   736     Misc_Primrec

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

   739   options [document_graph]

   740   theories Word

   741   document_files "root.bib" "root.tex"

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

   744   options [document = false]

   745   theories WordExamples

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

   748   theories [skip_proofs = false]

   749     StateSpaceEx

   750   document_files "root.tex"

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

   753   description {*

   754     Nonstandard analysis.

   755   *}

   756   options [document_graph]

   757   theories Hypercomplex

   758   document_files "root.tex"

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

   761   options [document = false]

   762   theories NSPrimes

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

   765   options [document = false]

   766   theories Mirabelle_Test

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

   769   options [document = false, timeout = 60]

   770   theories Ex

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

   773   options [document = false, quick_and_dirty]

   774   theories

   775     Boogie

   776     SMT_Examples

   777     SMT_Word_Examples

   778   theories [condition = ISABELLE_FULL_TEST]

   779     SMT_Tests

   780   files

   781     "Boogie_Dijkstra.certs"

   782     "Boogie_Max.certs"

   783     "SMT_Examples.certs"

   784     "SMT_Examples.certs2"

   785     "SMT_Word_Examples.certs2"

   786     "VCC_Max.certs"

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

   789   options [document = false]

   790   theories SPARK

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

   793   options [document = false]

   794   theories

   795     "Gcd/Greatest_Common_Divisor"

   797     "Liseq/Longest_Increasing_Subsequence"

   799     "RIPEMD-160/F"

   800     "RIPEMD-160/Hash"

   801     "RIPEMD-160/K_L"

   802     "RIPEMD-160/K_R"

   803     "RIPEMD-160/R_L"

   804     "RIPEMD-160/Round"

   805     "RIPEMD-160/R_R"

   806     "RIPEMD-160/S_L"

   807     "RIPEMD-160/S_R"

   809     "Sqrt/Sqrt"

   810   files

   811     "Gcd/greatest_common_divisor/g_c_d.fdl"

   812     "Gcd/greatest_common_divisor/g_c_d.rls"

   813     "Gcd/greatest_common_divisor/g_c_d.siv"

   814     "Liseq/liseq/liseq_length.fdl"

   815     "Liseq/liseq/liseq_length.rls"

   816     "Liseq/liseq/liseq_length.siv"

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   846   options [show_question_marks = false]

   847   theories

   848     Example_Verification

   849     VC_Principles

   850     Reference

   851     Complex_Types

   852   files

   853     "complex_types_app/initialize.fdl"

   854     "complex_types_app/initialize.rls"

   855     "complex_types_app/initialize.siv"

   856     "loop_invariant/proc1.fdl"

   857     "loop_invariant/proc1.rls"

   858     "loop_invariant/proc1.siv"

   859     "loop_invariant/proc2.fdl"

   860     "loop_invariant/proc2.rls"

   861     "loop_invariant/proc2.siv"

   862     "simple_greatest_common_divisor/g_c_d.fdl"

   863     "simple_greatest_common_divisor/g_c_d.rls"

   864     "simple_greatest_common_divisor/g_c_d.siv"

   865   document_files

   866     "complex_types.ads"

   867     "complex_types_app.adb"

   868     "complex_types_app.ads"

   869     "Gcd.adb"

   870     "Gcd.ads"

   871     "intro.tex"

   872     "loop_invariant.adb"

   873     "loop_invariant.ads"

   874     "root.bib"

   875     "root.tex"

   876     "Simple_Gcd.adb"

   877     "Simple_Gcd.ads"

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

   880   options [document = false]

   881   theories MutabelleExtra

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

   884   options [document = false]

   885   theories

   886     Quickcheck_Examples

   887   (* FIXME

   888     Quickcheck_Lattice_Examples

   889     Completeness

   890     Quickcheck_Interfaces

   891     Hotel_Example *)

   892   theories [condition = ISABELLE_GHC]

   893     Quickcheck_Narrowing_Examples

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

   896   theories [condition = ISABELLE_FULL_TEST, quick_and_dirty]

   897     Find_Unused_Assms_Examples

   898     Needham_Schroeder_No_Attacker_Example

   899     Needham_Schroeder_Guided_Attacker_Example

   900     Needham_Schroeder_Unguided_Attacker_Example

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

   903   description {*

   904     Author:     Cezary Kaliszyk and Christian Urban

   905   *}

   906   options [document = false]

   907   theories

   908     DList

   909     FSet

   910     Quotient_Int

   911     Quotient_Message

   912     Lift_FSet

   913     Lift_Set

   914     Lift_Fun

   915     Quotient_Rat

   916     Lift_DList

   917     Int_Pow

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

   920   options [document = false]

   921   theories

   922     Examples

   923     Predicate_Compile_Tests

   924     (* FIXME

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

   926     Specialisation_Examples

   927     IMP_1

   928     IMP_2

   929     (* FIXME since 21-Jul-2011

   930     Hotel_Example_Small_Generator

   931     IMP_3

   932     IMP_4 *)

   933   theories [condition = "ISABELLE_SWIPL"]

   934     Code_Prolog_Examples

   935     Context_Free_Grammar_Example

   936     Hotel_Example_Prolog

   937     Lambda_Example

   938     List_Examples

   939   theories [condition = "ISABELLE_SWIPL", quick_and_dirty]

   940     Reg_Exp_Example

   942 session HOLCF (main) in HOLCF = HOL +

   943   description {*

   944     Author:     Franz Regensburger

   945     Author:     Brian Huffman

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

   948   *}

   949   options [document_graph]

   950   theories [document = false]

   951     "~~/src/HOL/Library/Nat_Bijection"

   952     "~~/src/HOL/Library/Countable"

   953   theories

   954     Plain_HOLCF

   955     Fixrec

   956     HOLCF

   957   document_files "root.tex"

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

   960   theories

   961     Domain_ex

   962     Fixrec_ex

   963     New_Domain

   964   document_files "root.tex"

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

   967   options [document = false]

   968   theories HOLCF_Library

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

   971   description {*

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

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

   975   *}

   976   options [document = false]

   977   theories HoareEx

   978   document_files "root.tex"

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

   981   description {*

   982     Miscellaneous examples for HOLCF.

   983   *}

   984   options [document = false]

   985   theories

   986     Dnat

   987     Dagstuhl

   988     Focus_ex

   989     Fix2

   990     Hoare

   991     Concurrency_Monad

   992     Loop

   993     Powerdomain_ex

   994     Domain_Proofs

   995     Letrec

   996     Pattern_Match

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

   999   description {*

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

  1002     For introductions to FOCUS, see

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

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

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

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

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

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

  1012   *}

  1013   options [document = false]

  1014   theories

  1015     Fstreams

  1016     FOCUS

  1017     Buffer_adm

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

  1020   description {*

  1021     Author:     Olaf Mueller

  1022     Copyright   1997 TU München

  1024     A formalization of I/O automata in HOLCF.

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

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

  1028     finite and infinite sequences.

  1029   *}

  1030   options [document = false]

  1031   theories "meta_theory/Abstraction"

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

  1034   description {*

  1035     Author:     Olaf Mueller

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

  1038   *}

  1039   options [document = false]

  1040   theories Correctness

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

  1043   description {*

  1044     Author:     Tobias Nipkow & Konrad Slind

  1046     A network transmission protocol, performed in the

  1047     I/O automata formalization by Olaf Mueller.

  1048   *}

  1049   options [document = false]

  1050   theories Correctness

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

  1053   description {*

  1054     Author:     Olaf Mueller

  1056     Memory storage case study.

  1057   *}

  1058   options [document = false]

  1059   theories Correctness

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

  1062   description {*

  1063     Author:     Olaf Mueller

  1064   *}

  1065   options [document = false]

  1066   theories

  1067     TrivEx

  1068     TrivEx2

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

  1071   description {*

  1072     Some rather large datatype examples (from John Harrison).

  1073   *}

  1074   options [document = false]

  1075   theories [condition = ISABELLE_FULL_TEST, timing]

  1076     Brackin

  1077     Instructions

  1078     SML

  1079     Verilog

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

  1082   description {*

  1083     Some benchmark on large record.

  1084   *}

  1085   options [document = false]

  1086   theories [condition = ISABELLE_FULL_TEST, timing]

  1087     Record_Benchmark

author	wenzelm
	Wed, 30 Apr 2014 22:34:11 +0200
changeset 58143	8dd9df88f647
parent 58123	f2eb0f22589f
child 58157	848d507584db
permissions	-rw-r--r--