src/HOL/ROOT
author haftmann
Wed Nov 07 11:08:12 2018 +0000 (7 months ago)
changeset 69252 fc359b60121c
parent 69145 806be481aa57
child 69272 15e9ed5b28fb
permissions -rw-r--r--
dedicated examples for sorting
     1 chapter HOL
     2 
     3 session HOL (main) = Pure +
     4   description {*
     5     Classical Higher-order Logic.
     6   *}
     7   options [strict_facts]
     8   theories
     9     Main (global)
    10     Complex_Main (global)
    11   document_files
    12     "root.bib"
    13     "root.tex"
    14 
    15 session "HOL-Proofs" (timing) = Pure +
    16   description {*
    17     HOL-Main with explicit proof terms.
    18   *}
    19   options [quick_and_dirty = false, record_proofs = 2, parallel_proofs = 0, parallel_limit = 500]
    20   sessions
    21     "HOL-Library"
    22   theories
    23     "HOL-Library.Realizers"
    24 
    25 session "HOL-Library" (main timing) in Library = HOL +
    26   description {*
    27     Classical Higher-order Logic -- batteries included.
    28   *}
    29   theories
    30     Library
    31     (*conflicting type class instantiations and dependent applications*)
    32     Finite_Lattice
    33     List_Lexorder
    34     Prefix_Order
    35     Product_Lexorder
    36     Product_Order
    37     Subseq_Order
    38     (*conflicting syntax*)
    39     Datatype_Records
    40     (*data refinements and dependent applications*)
    41     AList_Mapping
    42     Code_Binary_Nat
    43     Code_Prolog
    44     Code_Real_Approx_By_Float
    45     Code_Target_Numeral
    46     DAList
    47     DAList_Multiset
    48     RBT_Mapping
    49     RBT_Set
    50     (*printing modifications*)
    51     OptionalSugar
    52     (*prototypic tools*)
    53     Predicate_Compile_Quickcheck
    54     (*legacy tools*)
    55     Old_Datatype
    56     Old_Recdef
    57     Realizers
    58     Refute
    59   document_files "root.bib" "root.tex"
    60 
    61 session "HOL-Analysis" (main timing) in Analysis = HOL +
    62   options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant",
    63     document_variants = "document:manual=-proof,-ML,-unimportant"]
    64   sessions
    65     "HOL-Library"
    66     "HOL-Computational_Algebra"
    67   theories
    68     L2_Norm
    69     Analysis
    70   document_files
    71     "root.tex"
    72 
    73 session "HOL-Analysis-ex" in "Analysis/ex" = "HOL-Analysis" +
    74   theories
    75     Approximations
    76 
    77 session "HOL-Computational_Algebra" (main timing) in "Computational_Algebra" = "HOL-Library" +
    78   theories
    79     Computational_Algebra
    80     (*conflicting type class instantiations and dependent applications*)
    81     Field_as_Ring
    82 
    83 session "HOL-Real_Asymp" in Real_Asymp = HOL +
    84   sessions
    85     "HOL-Decision_Procs"
    86   theories
    87     Real_Asymp
    88     Real_Asymp_Approx
    89     Real_Asymp_Examples
    90 
    91 session "HOL-Real_Asymp-Manual" in "Real_Asymp/Manual" = "HOL-Real_Asymp" +
    92   theories
    93     Real_Asymp_Doc
    94   document_files (in "~~/src/Doc")
    95     "iman.sty"
    96     "extra.sty"
    97     "isar.sty"
    98   document_files
    99     "root.tex"
   100     "style.sty"
   101 
   102 session "HOL-Hahn_Banach" in Hahn_Banach = "HOL-Library" +
   103   description {*
   104     Author:     Gertrud Bauer, TU Munich
   105 
   106     The Hahn-Banach theorem for real vector spaces.
   107 
   108     This is the proof of the Hahn-Banach theorem for real vectorspaces,
   109     following H. Heuser, Funktionalanalysis, p. 228 -232. The Hahn-Banach
   110     theorem is one of the fundamental theorems of functional analysis. It is a
   111     conclusion of Zorn's lemma.
   112 
   113     Two different formaulations of the theorem are presented, one for general
   114     real vectorspaces and its application to normed vectorspaces.
   115 
   116     The theorem says, that every continous linearform, defined on arbitrary
   117     subspaces (not only one-dimensional subspaces), can be extended to a
   118     continous linearform on the whole vectorspace.
   119   *}
   120   sessions
   121     "HOL-Analysis"
   122   theories
   123     Hahn_Banach
   124   document_files "root.bib" "root.tex"
   125 
   126 session "HOL-Induct" in Induct = "HOL-Library" +
   127   description {*
   128     Examples of (Co)Inductive Definitions.
   129 
   130     Comb proves the Church-Rosser theorem for combinators (see
   131     http://www.cl.cam.ac.uk/ftp/papers/reports/TR396-lcp-generic-automatic-proof-tools.ps.gz).
   132 
   133     Mutil is the famous Mutilated Chess Board problem (see
   134     http://www.cl.cam.ac.uk/ftp/papers/reports/TR394-lcp-mutilated-chess-board.dvi.gz).
   135 
   136     PropLog proves the completeness of a formalization of propositional logic
   137     (see
   138     http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz).
   139 
   140     Exp demonstrates the use of iterated inductive definitions to reason about
   141     mutually recursive relations.
   142   *}
   143   theories [quick_and_dirty]
   144     Common_Patterns
   145   theories
   146     Nested_Datatype
   147     QuoDataType
   148     QuoNestedDataType
   149     Term
   150     SList
   151     ABexp
   152     Infinitely_Branching_Tree
   153     Ordinals
   154     Sigma_Algebra
   155     Comb
   156     PropLog
   157     Com
   158   document_files "root.tex"
   159 
   160 session "HOL-IMP" (timing) in IMP = "HOL-Library" +
   161   options [document_variants = document]
   162   theories
   163     BExp
   164     ASM
   165     Finite_Reachable
   166     Denotational
   167     Compiler2
   168     Poly_Types
   169     Sec_Typing
   170     Sec_TypingT
   171     Def_Init_Big
   172     Def_Init_Small
   173     Fold
   174     Live
   175     Live_True
   176     Hoare_Examples
   177     Hoare_Sound_Complete
   178     VCG
   179     Hoare_Total
   180     VCG_Total_EX
   181     VCG_Total_EX2
   182     Collecting1
   183     Collecting_Examples
   184     Abs_Int_Tests
   185     Abs_Int1_parity
   186     Abs_Int1_const
   187     Abs_Int3
   188     Procs_Dyn_Vars_Dyn
   189     Procs_Stat_Vars_Dyn
   190     Procs_Stat_Vars_Stat
   191     C_like
   192     OO
   193   document_files "root.bib" "root.tex"
   194 
   195 session "HOL-IMPP" in IMPP = HOL +
   196   description {*
   197     Author:     David von Oheimb
   198     Copyright   1999 TUM
   199 
   200     IMPP -- An imperative language with procedures.
   201 
   202     This is an extension of IMP with local variables and mutually recursive
   203     procedures. For documentation see "Hoare Logic for Mutual Recursion and
   204     Local Variables" (https://isabelle.in.tum.de/Bali/papers/FSTTCS99.html).
   205   *}
   206   theories EvenOdd
   207 
   208 session "HOL-Data_Structures" (timing) in Data_Structures = HOL +
   209   options [document_variants = document]
   210   sessions
   211     "HOL-Number_Theory"
   212   theories [document = false]
   213     Less_False
   214   theories
   215     Sorting
   216     Balance
   217     Tree_Map
   218     AVL_Map
   219     RBT_Map
   220     Tree23_Map
   221     Tree234_Map
   222     Brother12_Map
   223     AA_Map
   224     Set2_Join_RBT
   225     Array_Braun
   226     Trie
   227     Leftist_Heap
   228     Binomial_Heap
   229   document_files "root.tex" "root.bib"
   230 
   231 session "HOL-Import" in Import = HOL +
   232   theories HOL_Light_Maps
   233   theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import
   234 
   235 session "HOL-Number_Theory" (main timing) in Number_Theory = "HOL-Computational_Algebra" +
   236   description {*
   237     Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler
   238     Theorem, Wilson's Theorem, some lemmas for Quadratic Reciprocity.
   239   *}
   240   sessions
   241     "HOL-Algebra"
   242   theories
   243     Number_Theory
   244   document_files
   245     "root.tex"
   246 
   247 session "HOL-Hoare" in Hoare = HOL +
   248   description {*
   249     Verification of imperative programs (verification conditions are generated
   250     automatically from pre/post conditions and loop invariants).
   251   *}
   252   theories Hoare
   253   document_files "root.bib" "root.tex"
   254 
   255 session "HOL-Hoare_Parallel" (timing) in Hoare_Parallel = HOL +
   256   description {*
   257     Verification of shared-variable imperative programs a la Owicki-Gries.
   258     (verification conditions are generated automatically).
   259   *}
   260   theories Hoare_Parallel
   261   document_files "root.bib" "root.tex"
   262 
   263 session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Number_Theory" +
   264   sessions
   265     "HOL-Data_Structures"
   266     "HOL-ex"
   267   theories
   268     Generate
   269     Generate_Binary_Nat
   270     Generate_Target_Nat
   271     Generate_Efficient_Datastructures
   272     Code_Lazy_Test
   273     Code_Test_PolyML
   274     Code_Test_Scala
   275   theories [condition = ISABELLE_GHC]
   276     Code_Test_GHC
   277   theories [condition = ISABELLE_MLTON]
   278     Code_Test_MLton
   279   theories [condition = ISABELLE_OCAMLC]
   280     Code_Test_OCaml
   281   theories [condition = ISABELLE_SMLNJ]
   282     Code_Test_SMLNJ
   283 
   284 session "HOL-Metis_Examples" (timing) in Metis_Examples = "HOL-Library" +
   285   description {*
   286     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   287     Author:     Jasmin Blanchette, TU Muenchen
   288 
   289     Testing Metis and Sledgehammer.
   290   *}
   291   sessions
   292     "HOL-Decision_Procs"
   293   theories
   294     Abstraction
   295     Big_O
   296     Binary_Tree
   297     Clausification
   298     Message
   299     Proxies
   300     Tarski
   301     Trans_Closure
   302     Sets
   303 
   304 session "HOL-Nitpick_Examples" in Nitpick_Examples = "HOL-Library" +
   305   description {*
   306     Author:     Jasmin Blanchette, TU Muenchen
   307     Copyright   2009
   308   *}
   309   theories [quick_and_dirty] Nitpick_Examples
   310 
   311 session "HOL-Algebra" (main timing) in Algebra = "HOL-Computational_Algebra" +
   312   description {*
   313     Author: Clemens Ballarin, started 24 September 1999, and many others
   314 
   315     The Isabelle Algebraic Library.
   316   *}
   317   theories
   318     (* Orders and Lattices *)
   319     Galois_Connection    (* Knaster-Tarski theorem and Galois connections *)
   320     (* Groups *)
   321     FiniteProduct        (* Product operator for commutative groups *)
   322     Sylow                (* Sylow's theorem *)
   323     Bij                  (* Automorphism Groups *)
   324     Multiplicative_Group
   325     Zassenhaus            (* The Zassenhaus lemma *)
   326     (* Rings *)
   327     Divisibility         (* Rings *)
   328     IntRing              (* Ideals and residue classes *)
   329     UnivPoly             (* Polynomials *)
   330     (* Main theory *)
   331     Algebra             
   332   document_files "root.bib" "root.tex"
   333 
   334 session "HOL-Auth" (timing) in Auth = "HOL-Library" +
   335   description {*
   336     A new approach to verifying authentication protocols.
   337   *}
   338   theories
   339     Auth_Shared
   340     Auth_Public
   341     "Smartcard/Auth_Smartcard"
   342     "Guard/Auth_Guard_Shared"
   343     "Guard/Auth_Guard_Public"
   344   document_files "root.tex"
   345 
   346 session "HOL-UNITY" (timing) in UNITY = "HOL-Auth" +
   347   description {*
   348     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   349     Copyright   1998  University of Cambridge
   350 
   351     Verifying security protocols using Chandy and Misra's UNITY formalism.
   352   *}
   353   theories
   354     (*Basic meta-theory*)
   355     UNITY_Main
   356 
   357     (*Simple examples: no composition*)
   358     "Simple/Deadlock"
   359     "Simple/Common"
   360     "Simple/Network"
   361     "Simple/Token"
   362     "Simple/Channel"
   363     "Simple/Lift"
   364     "Simple/Mutex"
   365     "Simple/Reach"
   366     "Simple/Reachability"
   367 
   368     (*Verifying security protocols using UNITY*)
   369     "Simple/NSP_Bad"
   370 
   371     (*Example of composition*)
   372     "Comp/Handshake"
   373 
   374     (*Universal properties examples*)
   375     "Comp/Counter"
   376     "Comp/Counterc"
   377     "Comp/Priority"
   378 
   379     "Comp/TimerArray"
   380     "Comp/Progress"
   381 
   382     "Comp/Alloc"
   383     "Comp/AllocImpl"
   384     "Comp/Client"
   385 
   386     (*obsolete*)
   387     ELT
   388   document_files "root.tex"
   389 
   390 session "HOL-Unix" in Unix = "HOL-Library" +
   391   options [print_mode = "no_brackets,no_type_brackets"]
   392   theories Unix
   393   document_files "root.bib" "root.tex"
   394 
   395 session "HOL-ZF" in ZF = "HOL-Library" +
   396   theories
   397     MainZF
   398     Games
   399   document_files "root.tex"
   400 
   401 session "HOL-Imperative_HOL" (timing) in Imperative_HOL = "HOL-Library" +
   402   options [print_mode = "iff,no_brackets"]
   403   theories Imperative_HOL_ex
   404   document_files "root.bib" "root.tex"
   405 
   406 session "HOL-Decision_Procs" (timing) in Decision_Procs = "HOL-Algebra" +
   407   description {*
   408     Various decision procedures, typically involving reflection.
   409   *}
   410   theories
   411     Decision_Procs
   412 
   413 session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
   414   sessions
   415     "HOL-Isar_Examples"
   416   theories
   417     Hilbert_Classical
   418     Proof_Terms
   419     XML_Data
   420 
   421 session "HOL-Proofs-Extraction" (timing) in "Proofs/Extraction" = "HOL-Proofs" +
   422   description {*
   423     Examples for program extraction in Higher-Order Logic.
   424   *}
   425   options [parallel_proofs = 0, quick_and_dirty = false]
   426   sessions
   427     "HOL-Computational_Algebra"
   428   theories
   429     Greatest_Common_Divisor
   430     Warshall
   431     Higman_Extraction
   432     Pigeonhole
   433     Euclid
   434   document_files "root.bib" "root.tex"
   435 
   436 session "HOL-Proofs-Lambda" (timing) in "Proofs/Lambda" = "HOL-Proofs" +
   437   description {*
   438     Lambda Calculus in de Bruijn's Notation.
   439 
   440     This session defines lambda-calculus terms with de Bruijn indixes and
   441     proves confluence of beta, eta and beta+eta.
   442 
   443     The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole
   444     theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html).
   445   *}
   446   options [print_mode = "no_brackets",
   447     parallel_proofs = 0, quick_and_dirty = false]
   448   sessions
   449     "HOL-Library"
   450   theories
   451     Eta
   452     StrongNorm
   453     Standardization
   454     WeakNorm
   455   document_files "root.bib" "root.tex"
   456 
   457 session "HOL-Prolog" in Prolog = HOL +
   458   description {*
   459     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
   460 
   461     A bare-bones implementation of Lambda-Prolog.
   462 
   463     This is a simple exploratory implementation of Lambda-Prolog in HOL,
   464     including some minimal examples (in Test.thy) and a more typical example of
   465     a little functional language and its type system.
   466   *}
   467   theories Test Type
   468 
   469 session "HOL-MicroJava" (timing) in MicroJava = "HOL-Library" +
   470   description {*
   471     Formalization of a fragment of Java, together with a corresponding virtual
   472     machine and a specification of its bytecode verifier and a lightweight
   473     bytecode verifier, including proofs of type-safety.
   474   *}
   475   sessions
   476     "HOL-Eisbach"
   477   theories
   478     MicroJava
   479   document_files
   480     "introduction.tex"
   481     "root.bib"
   482     "root.tex"
   483 
   484 session "HOL-NanoJava" in NanoJava = HOL +
   485   description {*
   486     Hoare Logic for a tiny fragment of Java.
   487   *}
   488   theories Example
   489   document_files "root.bib" "root.tex"
   490 
   491 session "HOL-Bali" (timing) in Bali = "HOL-Library" +
   492   theories
   493     AxExample
   494     AxSound
   495     AxCompl
   496     Trans
   497     TypeSafe
   498   document_files "root.tex"
   499 
   500 session "HOL-IOA" in IOA = HOL +
   501   description {*
   502     Author:     Tobias Nipkow and Konrad Slind and Olaf Müller
   503     Copyright   1994--1996  TU Muenchen
   504 
   505     The meta-theory of I/O-Automata in HOL. This formalization has been
   506     significantly changed and extended, see HOLCF/IOA. There are also the
   507     proofs of two communication protocols which formerly have been here.
   508 
   509     @inproceedings{Nipkow-Slind-IOA,
   510     author={Tobias Nipkow and Konrad Slind},
   511     title={{I/O} Automata in {Isabelle/HOL}},
   512     booktitle={Proc.\ TYPES Workshop 1994},
   513     publisher=Springer,
   514     series=LNCS,
   515     note={To appear}}
   516     ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz
   517 
   518     and
   519 
   520     @inproceedings{Mueller-Nipkow,
   521     author={Olaf M\"uller and Tobias Nipkow},
   522     title={Combining Model Checking and Deduction for {I/O}-Automata},
   523     booktitle={Proc.\ TACAS Workshop},
   524     organization={Aarhus University, BRICS report},
   525     year=1995}
   526     ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz
   527   *}
   528   theories Solve
   529 
   530 session "HOL-Lattice" in Lattice = HOL +
   531   description {*
   532     Author:     Markus Wenzel, TU Muenchen
   533 
   534     Basic theory of lattices and orders.
   535   *}
   536   theories CompleteLattice
   537   document_files "root.tex"
   538 
   539 session "HOL-ex" (timing) in ex = "HOL-Number_Theory" +
   540   description {*
   541     Miscellaneous examples for Higher-Order Logic.
   542   *}
   543   theories
   544     Adhoc_Overloading_Examples
   545     Antiquote
   546     Argo_Examples
   547     Arith_Examples
   548     Ballot
   549     BinEx
   550     Birthday_Paradox
   551     Bit_Lists
   552     Bubblesort
   553     CTL
   554     Cartouche_Examples
   555     Case_Product
   556     Chinese
   557     Classical
   558     Code_Binary_Nat_examples
   559     Code_Lazy_Demo
   560     Code_Timing
   561     Coercion_Examples
   562     Coherent
   563     Commands
   564     Computations
   565     Conditional_Parametricity_Examples
   566     Cubic_Quartic
   567     Datatype_Record_Examples
   568     Dedekind_Real
   569     Erdoes_Szekeres
   570     Eval_Examples
   571     Executable_Relation
   572     Execute_Choice
   573     Functions
   574     Function_Growth
   575     Gauge_Integration
   576     Groebner_Examples
   577     Guess
   578     HarmonicSeries
   579     Hebrew
   580     Hex_Bin_Examples
   581     IArray_Examples
   582     Iff_Oracle
   583     Induction_Schema
   584     Intuitionistic
   585     Lagrange
   586     List_to_Set_Comprehension_Examples
   587     LocaleTest2
   588     "ML"
   589     MergeSort
   590     MonoidGroup
   591     Multiquote
   592     NatSum
   593     Normalization_by_Evaluation
   594     PER
   595     Parallel_Example
   596     Peano_Axioms
   597     Perm_Fragments
   598     PresburgerEx
   599     Primrec
   600     Pythagoras
   601     Quicksort
   602     Radix_Sort
   603     Records
   604     Reflection_Examples
   605     Refute_Examples
   606     Residue_Ring
   607     Rewrite_Examples
   608     SOS
   609     SOS_Cert
   610     Seq
   611     Serbian
   612     Set_Comprehension_Pointfree_Examples
   613     Set_Theory
   614     Simproc_Tests
   615     Simps_Case_Conv_Examples
   616     Sorting_Algorithms_Examples
   617     Sqrt
   618     Sqrt_Script
   619     Sudoku
   620     Sum_of_Powers
   621     Tarski
   622     Termination
   623     ThreeDivides
   624     Transfer_Debug
   625     Transfer_Int_Nat
   626     Transitive_Closure_Table_Ex
   627     Tree23
   628     Unification
   629     While_Combinator_Example
   630     Word_Type
   631     veriT_Preprocessing
   632   theories [skip_proofs = false]
   633     SAT_Examples
   634     Meson_Test
   635 
   636 session "HOL-Isar_Examples" in Isar_Examples = "HOL-Computational_Algebra" +
   637   description {*
   638     Miscellaneous Isabelle/Isar examples.
   639   *}
   640   options [quick_and_dirty]
   641   theories
   642     Knaster_Tarski
   643     Peirce
   644     Drinker
   645     Cantor
   646     Structured_Statements
   647     Basic_Logic
   648     Expr_Compiler
   649     Fibonacci
   650     Group
   651     Group_Context
   652     Group_Notepad
   653     Hoare_Ex
   654     Mutilated_Checkerboard
   655     Puzzle
   656     Summation
   657     First_Order_Logic
   658     Higher_Order_Logic
   659   document_files
   660     "root.bib"
   661     "root.tex"
   662 
   663 session "HOL-Eisbach" in Eisbach = HOL +
   664   description {*
   665     The Eisbach proof method language and "match" method.
   666   *}
   667   sessions
   668     FOL
   669   theories
   670     Eisbach
   671     Tests
   672     Examples
   673     Examples_FOL
   674 
   675 session "HOL-SET_Protocol" (timing) in SET_Protocol = "HOL-Library" +
   676   description {*
   677     Verification of the SET Protocol.
   678   *}
   679   theories
   680     SET_Protocol
   681   document_files "root.tex"
   682 
   683 session "HOL-Matrix_LP" in Matrix_LP = "HOL-Library" +
   684   description {*
   685     Two-dimensional matrices and linear programming.
   686   *}
   687   theories Cplex
   688   document_files "root.tex"
   689 
   690 session "HOL-TLA" in TLA = HOL +
   691   description {*
   692     Lamport's Temporal Logic of Actions.
   693   *}
   694   theories TLA
   695 
   696 session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" +
   697   theories Inc
   698 
   699 session "HOL-TLA-Buffer" in "TLA/Buffer" = "HOL-TLA" +
   700   theories DBuffer
   701 
   702 session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" +
   703   theories MemoryImplementation
   704 
   705 session "HOL-TPTP" in TPTP = "HOL-Library" +
   706   description {*
   707     Author:     Jasmin Blanchette, TU Muenchen
   708     Author:     Nik Sultana, University of Cambridge
   709     Copyright   2011
   710 
   711     TPTP-related extensions.
   712   *}
   713   theories
   714     ATP_Theory_Export
   715     MaSh_Eval
   716     TPTP_Interpret
   717     THF_Arith
   718     TPTP_Proof_Reconstruction
   719   theories
   720     ATP_Problem_Import
   721 
   722 session "HOL-Probability" (main timing) in "Probability" = "HOL-Analysis" +
   723   theories
   724     Probability
   725   document_files "root.tex"
   726 
   727 session "HOL-Probability-ex" (timing) in "Probability/ex" = "HOL-Probability" +
   728   theories
   729     Dining_Cryptographers
   730     Koepf_Duermuth_Countermeasure
   731     Measure_Not_CCC
   732 
   733 session "HOL-Nominal" in Nominal = "HOL-Library" +
   734   theories
   735     Nominal
   736 
   737 session "HOL-Nominal-Examples" (timing) in "Nominal/Examples" = "HOL-Nominal" +
   738   theories
   739     Class3
   740     CK_Machine
   741     Compile
   742     Contexts
   743     Crary
   744     CR_Takahashi
   745     CR
   746     Fsub
   747     Height
   748     Lambda_mu
   749     Lam_Funs
   750     LocalWeakening
   751     Pattern
   752     SN
   753     SOS
   754     Standardization
   755     Support
   756     Type_Preservation
   757     Weakening
   758     W
   759   theories [quick_and_dirty]
   760     VC_Condition
   761 
   762 session "HOL-Cardinals" (timing) in Cardinals = "HOL-Library" +
   763   description {*
   764     Ordinals and Cardinals, Full Theories.
   765   *}
   766   theories
   767     Cardinals
   768     Bounded_Set
   769   document_files
   770     "intro.tex"
   771     "root.tex"
   772     "root.bib"
   773 
   774 session "HOL-Datatype_Examples" (timing) in Datatype_Examples = "HOL-Library" +
   775   description {*
   776     (Co)datatype Examples.
   777   *}
   778   theories
   779     Compat
   780     Lambda_Term
   781     Process
   782     TreeFsetI
   783     "Derivation_Trees/Gram_Lang"
   784     "Derivation_Trees/Parallel_Composition"
   785     Koenig
   786     Lift_BNF
   787     Milner_Tofte
   788     Stream_Processor
   789     Misc_Codatatype
   790     Misc_Datatype
   791     Misc_Primcorec
   792     Misc_Primrec
   793 
   794 session "HOL-Corec_Examples" (timing) in Corec_Examples = "HOL-Library" +
   795   description {*
   796     Corecursion Examples.
   797   *}
   798   theories
   799     LFilter
   800     Paper_Examples
   801     Stream_Processor
   802     "Tests/Simple_Nesting"
   803     "Tests/Iterate_GPV"
   804   theories [quick_and_dirty]
   805     "Tests/GPV_Bare_Bones"
   806     "Tests/Merge_D"
   807     "Tests/Merge_Poly"
   808     "Tests/Misc_Mono"
   809     "Tests/Misc_Poly"
   810     "Tests/Small_Concrete"
   811     "Tests/Stream_Friends"
   812     "Tests/TLList_Friends"
   813     "Tests/Type_Class"
   814 
   815 session "HOL-Word" (main timing) in Word = HOL +
   816   sessions
   817     "HOL-Library"
   818   theories
   819     Word
   820     WordBitwise
   821     Bit_Comparison
   822     WordExamples
   823   document_files "root.bib" "root.tex"
   824 
   825 session "HOL-Statespace" in Statespace = HOL +
   826   theories [skip_proofs = false]
   827     StateSpaceEx
   828   document_files "root.tex"
   829 
   830 session "HOL-Nonstandard_Analysis" (timing) in Nonstandard_Analysis = "HOL-Computational_Algebra" +
   831   description {*
   832     Nonstandard analysis.
   833   *}
   834   theories
   835     Nonstandard_Analysis
   836   document_files "root.tex"
   837 
   838 session "HOL-Nonstandard_Analysis-Examples" (timing) in "Nonstandard_Analysis/Examples" = "HOL-Nonstandard_Analysis" +
   839   theories
   840     NSPrimes
   841 
   842 session "HOL-Mirabelle" in Mirabelle = HOL +
   843   theories Mirabelle_Test
   844 
   845 session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
   846   options [timeout = 60]
   847   theories Ex
   848 
   849 session "HOL-Word-SMT_Examples" (timing) in SMT_Examples = "HOL-Word" +
   850   options [quick_and_dirty]
   851   theories
   852     Boogie
   853     SMT_Examples
   854     SMT_Word_Examples
   855     SMT_Tests
   856 
   857 session "HOL-SPARK" in "SPARK" = "HOL-Word" +
   858   theories
   859     SPARK
   860 
   861 session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
   862   theories
   863     "Gcd/Greatest_Common_Divisor"
   864     "Liseq/Longest_Increasing_Subsequence"
   865     "RIPEMD-160/F"
   866     "RIPEMD-160/Hash"
   867     "RIPEMD-160/K_L"
   868     "RIPEMD-160/K_R"
   869     "RIPEMD-160/R_L"
   870     "RIPEMD-160/Round"
   871     "RIPEMD-160/R_R"
   872     "RIPEMD-160/S_L"
   873     "RIPEMD-160/S_R"
   874     "Sqrt/Sqrt"
   875 
   876 session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +
   877   options [show_question_marks = false]
   878   sessions
   879     "HOL-SPARK-Examples"
   880   theories
   881     Example_Verification
   882     VC_Principles
   883     Reference
   884     Complex_Types
   885   document_files
   886     "complex_types.ads"
   887     "complex_types_app.adb"
   888     "complex_types_app.ads"
   889     "Gcd.adb"
   890     "Gcd.ads"
   891     "intro.tex"
   892     "loop_invariant.adb"
   893     "loop_invariant.ads"
   894     "root.bib"
   895     "root.tex"
   896     "Simple_Gcd.adb"
   897     "Simple_Gcd.ads"
   898 
   899 session "HOL-Mutabelle" in Mutabelle = "HOL-Library" +
   900   theories MutabelleExtra
   901 
   902 session "HOL-Quickcheck_Examples" (timing) in Quickcheck_Examples = "HOL-Library" +
   903   theories
   904     Quickcheck_Examples
   905     Quickcheck_Lattice_Examples
   906     Completeness
   907     Quickcheck_Interfaces
   908     Quickcheck_Nesting_Example
   909   theories [condition = ISABELLE_GHC]
   910     Hotel_Example
   911     Quickcheck_Narrowing_Examples
   912 
   913 session "HOL-Quotient_Examples" (timing) in Quotient_Examples = "HOL-Algebra" +
   914   description {*
   915     Author:     Cezary Kaliszyk and Christian Urban
   916   *}
   917   theories
   918     DList
   919     Quotient_FSet
   920     Quotient_Int
   921     Quotient_Message
   922     Lift_FSet
   923     Lift_Set
   924     Lift_Fun
   925     Quotient_Rat
   926     Lift_DList
   927     Int_Pow
   928     Lifting_Code_Dt_Test
   929 
   930 session "HOL-Predicate_Compile_Examples" (timing) in Predicate_Compile_Examples = "HOL-Library" +
   931   theories
   932     Examples
   933     Predicate_Compile_Tests
   934     Predicate_Compile_Quickcheck_Examples
   935     Specialisation_Examples
   936     IMP_1
   937     IMP_2
   938     (* FIXME since 21-Jul-2011
   939     Hotel_Example_Small_Generator *)
   940     IMP_3
   941     IMP_4
   942   theories [condition = ISABELLE_SWIPL]
   943     Code_Prolog_Examples
   944     Context_Free_Grammar_Example
   945     Hotel_Example_Prolog
   946     Lambda_Example
   947     List_Examples
   948   theories [condition = ISABELLE_SWIPL, quick_and_dirty]
   949     Reg_Exp_Example
   950 
   951 session "HOL-Types_To_Sets" in Types_To_Sets = HOL +
   952   description {*
   953     Experimental extension of Higher-Order Logic to allow translation of types to sets.
   954   *}
   955   theories
   956     Types_To_Sets
   957     "Examples/Prerequisites"
   958     "Examples/Finite"
   959     "Examples/T2_Spaces"
   960     "Examples/Linear_Algebra_On"
   961 
   962 session HOLCF (main timing) in HOLCF = HOL +
   963   description {*
   964     Author:     Franz Regensburger
   965     Author:     Brian Huffman
   966 
   967     HOLCF -- a semantic extension of HOL by the LCF logic.
   968   *}
   969   sessions
   970     "HOL-Library"
   971   theories
   972     HOLCF (global)
   973   document_files "root.tex"
   974 
   975 session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF +
   976   theories
   977     Domain_ex
   978     Fixrec_ex
   979     New_Domain
   980   document_files "root.tex"
   981 
   982 session "HOLCF-Library" in "HOLCF/Library" = HOLCF +
   983   theories
   984     HOLCF_Library
   985     HOL_Cpo
   986 
   987 session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF +
   988   description {*
   989     IMP -- A WHILE-language and its Semantics.
   990 
   991     This is the HOLCF-based denotational semantics of a simple WHILE-language.
   992   *}
   993   sessions
   994     "HOL-IMP"
   995   theories
   996     HoareEx
   997   document_files
   998     "isaverbatimwrite.sty"
   999     "root.tex"
  1000     "root.bib"
  1001 
  1002 session "HOLCF-ex" in "HOLCF/ex" = "HOLCF-Library" +
  1003   description {*
  1004     Miscellaneous examples for HOLCF.
  1005   *}
  1006   theories
  1007     Dnat
  1008     Dagstuhl
  1009     Focus_ex
  1010     Fix2
  1011     Hoare
  1012     Concurrency_Monad
  1013     Loop
  1014     Powerdomain_ex
  1015     Domain_Proofs
  1016     Letrec
  1017     Pattern_Match
  1018 
  1019 session "HOLCF-FOCUS" in "HOLCF/FOCUS" = "HOLCF-Library" +
  1020   description {*
  1021     FOCUS: a theory of stream-processing functions Isabelle/HOLCF.
  1022 
  1023     For introductions to FOCUS, see
  1024 
  1025     "The Design of Distributed Systems - An Introduction to FOCUS"
  1026     http://www4.in.tum.de/publ/html.php?e=2
  1027 
  1028     "Specification and Refinement of a Buffer of Length One"
  1029     http://www4.in.tum.de/publ/html.php?e=15
  1030 
  1031     "Specification and Development of Interactive Systems: Focus on Streams,
  1032     Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321
  1033   *}
  1034   theories
  1035     Fstreams
  1036     FOCUS
  1037     Buffer_adm
  1038 
  1039 session IOA (timing) in "HOLCF/IOA" = HOLCF +
  1040   description {*
  1041     Author:     Olaf Mueller
  1042     Copyright   1997 TU München
  1043 
  1044     A formalization of I/O automata in HOLCF.
  1045 
  1046     The distribution contains simulation relations, temporal logic, and an
  1047     abstraction theory. Everything is based upon a domain-theoretic model of
  1048     finite and infinite sequences.
  1049   *}
  1050   theories Abstraction
  1051 
  1052 session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
  1053   description {*
  1054     Author:     Olaf Mueller
  1055 
  1056     The Alternating Bit Protocol performed in I/O-Automata.
  1057   *}
  1058   theories
  1059     Correctness
  1060     Spec
  1061 
  1062 session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA +
  1063   description {*
  1064     Author:     Tobias Nipkow & Konrad Slind
  1065 
  1066     A network transmission protocol, performed in the
  1067     I/O automata formalization by Olaf Mueller.
  1068   *}
  1069   theories Correctness
  1070 
  1071 session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA +
  1072   description {*
  1073     Author:     Olaf Mueller
  1074 
  1075     Memory storage case study.
  1076   *}
  1077   theories Correctness
  1078 
  1079 session "IOA-ex" in "HOLCF/IOA/ex" = IOA +
  1080   description {*
  1081     Author:     Olaf Mueller
  1082   *}
  1083   theories
  1084     TrivEx
  1085     TrivEx2