# HG changeset patch # User wenzelm # Date 1492858375 -7200 # Node ID d164c4fc0d2c0f3cde402872ac2bb84151e79117 # Parent 701bb74c5f97ba13263470a964b7582883d5a279# Parent e957b1f004499d859cba5da826cbf1e0b57c8a3f merged diff -r 701bb74c5f97 -r d164c4fc0d2c src/HOL/ROOT --- a/src/HOL/ROOT Fri Apr 21 21:37:01 2017 +0200 +++ b/src/HOL/ROOT Sat Apr 22 12:52:55 2017 +0200 @@ -62,10 +62,7 @@ Refute document_files "root.bib" "root.tex" -session "HOL-Analysis" (main timing) in Analysis = HOL + - sessions - "HOL-Library" - "HOL-Computational_Algebra" +session "HOL-Analysis" (main timing) in Analysis = "HOL-Computational_Algebra" + theories Analysis document_files @@ -76,16 +73,14 @@ Approximations Circle_Area -session "HOL-Computational_Algebra" in "Computational_Algebra" = HOL + - sessions - "HOL-Library" +session "HOL-Computational_Algebra" in "Computational_Algebra" = "HOL-Library" + theories Computational_Algebra (*conflicting type class instantiations and dependent applications*) Field_as_Ring Polynomial_Factorial -session "HOL-Hahn_Banach" in Hahn_Banach = HOL + +session "HOL-Hahn_Banach" in Hahn_Banach = "HOL-Library" + description {* Author: Gertrud Bauer, TU Munich @@ -103,13 +98,11 @@ subspaces (not only one-dimensional subspaces), can be extended to a continous linearform on the whole vectorspace. *} - sessions - "HOL-Library" theories Hahn_Banach document_files "root.bib" "root.tex" -session "HOL-Induct" in Induct = HOL + +session "HOL-Induct" in Induct = "HOL-Library" + description {* Examples of (Co)Inductive Definitions. @@ -126,8 +119,6 @@ Exp demonstrates the use of iterated inductive definitions to reason about mutually recursive relations. *} - sessions - "HOL-Library" theories [document = false] "~~/src/HOL/Library/Old_Datatype" theories [quick_and_dirty] @@ -224,15 +215,13 @@ theories HOL_Light_Maps theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import -session "HOL-Number_Theory" (timing) in Number_Theory = HOL + +session "HOL-Number_Theory" (timing) in Number_Theory = "HOL-Computational_Algebra" + description {* Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler Theorem, Wilson's Theorem, some lemmas for Quadratic Reciprocity. *} sessions - "HOL-Library" "HOL-Algebra" - "HOL-Computational_Algebra" theories [document = false] "~~/src/HOL/Library/FuncSet" "~~/src/HOL/Library/Multiset" @@ -259,11 +248,8 @@ theories Hoare_Parallel document_files "root.bib" "root.tex" -session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" + +session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Number_Theory" + options [document = false, browser_info = false] - sessions - "HOL-Computational_Algebra" - "HOL-Number_Theory" theories Generate Generate_Binary_Nat @@ -318,15 +304,12 @@ options [document = false] theories Nunchaku -session "HOL-Algebra" (main timing) in Algebra = HOL + +session "HOL-Algebra" (main timing) in Algebra = "HOL-Computational_Algebra" + description {* Author: Clemens Ballarin, started 24 September 1999 The Isabelle Algebraic Library. *} - sessions - "HOL-Library" - "HOL-Computational_Algebra" theories [document = false] (* Preliminaries from set and number theory *) "~~/src/HOL/Library/FuncSet" @@ -416,10 +399,8 @@ theories MainZF Games document_files "root.tex" -session "HOL-Imperative_HOL" in Imperative_HOL = HOL + +session "HOL-Imperative_HOL" in Imperative_HOL = "HOL-Library" + options [print_mode = "iff,no_brackets"] - sessions - "HOL-Library" theories [document = false] "~~/src/HOL/Library/Countable" "~~/src/HOL/Library/Monad_Syntax" @@ -427,14 +408,11 @@ theories Imperative_HOL_ex document_files "root.bib" "root.tex" -session "HOL-Decision_Procs" (timing) in Decision_Procs = HOL + +session "HOL-Decision_Procs" (timing) in Decision_Procs = "HOL-Algebra" + description {* Various decision procedures, typically involving reflection. *} options [document = false] - sessions - "HOL-Library" - "HOL-Algebra" theories Decision_Procs @@ -500,14 +478,12 @@ options [document = false] theories Test Type -session "HOL-MicroJava" (timing) in MicroJava = HOL + +session "HOL-MicroJava" (timing) in MicroJava = "HOL-Library" + description {* Formalization of a fragment of Java, together with a corresponding virtual machine and a specification of its bytecode verifier and a lightweight bytecode verifier, including proofs of type-safety. *} - sessions - "HOL-Library" theories [document = false] "~~/src/HOL/Library/While_Combinator" theories @@ -573,112 +549,103 @@ theories CompleteLattice document_files "root.tex" -session "HOL-ex" in ex = HOL + +session "HOL-ex" in ex = "HOL-Library" + description {* Miscellaneous examples for Higher-Order Logic. *} + options [document = false] sessions - "HOL-Library" "HOL-Number_Theory" - theories [document = false] - "~~/src/HOL/Library/State_Monad" - Code_Binary_Nat_examples - "~~/src/HOL/Library/FuncSet" - Eval_Examples - Normalization_by_Evaluation - Hebrew + theories + Adhoc_Overloading_Examples + Antiquote + Argo_Examples + Arith_Examples + Ballot + BinEx + Birthday_Paradox + Bubblesort + CTL + Cartouche_Examples Chinese - Serbian - "~~/src/HOL/Library/Refute" - "~~/src/HOL/Library/Transitive_Closure_Table" - Cartouche_Examples - Computations - theories + Classical + Code_Binary_Nat_examples + Code_Timing + Coercion_Examples + Coherent Commands - Adhoc_Overloading_Examples + Computations + Cubic_Quartic + Dedekind_Real + Erdoes_Szekeres + Eval_Examples + Executable_Relation + Execute_Choice + Functions + Gauge_Integration + Groebner_Examples + Guess + HarmonicSeries + Hebrew + Hex_Bin_Examples + IArray_Examples Iff_Oracle - Coercion_Examples + Induction_Schema + Intuitionistic + Lagrange + List_to_Set_Comprehension_Examples + LocaleTest2 + ML + MergeSort + MonoidGroup + Multiquote + NatSum + Normalization_by_Evaluation + PER + Parallel_Example Peano_Axioms - Guess - Functions - Induction_Schema - LocaleTest2 + Perm_Fragments + PresburgerEx + Primrec + Pythagoras + Quicksort Records - While_Combinator_Example - MonoidGroup - BinEx - Hex_Bin_Examples - Antiquote - Multiquote - PER - NatSum - ThreeDivides - Cubic_Quartic - Pythagoras - Intuitionistic - CTL - Arith_Examples - Tree23 - Bubblesort - MergeSort - Lagrange - Groebner_Examples - Unification - Primrec - Tarski - Classical + Reflection_Examples + Refute_Examples + Rewrite_Examples + SAT_Examples + SOS + SOS_Cert + Seq + Serbian + Set_Comprehension_Pointfree_Examples Set_Theory - Termination - Coherent - PresburgerEx - Reflection_Examples + Simproc_Tests + Simps_Case_Conv_Examples Sqrt Sqrt_Script + Sudoku + Sum_of_Powers + Tarski + Termination + ThreeDivides Transfer_Debug Transfer_Ex Transfer_Int_Nat Transitive_Closure_Table_Ex - HarmonicSeries - Refute_Examples - Execute_Choice - Gauge_Integration - Dedekind_Real - Quicksort - Birthday_Paradox - List_to_Set_Comprehension_Examples - Seq - Simproc_Tests - Executable_Relation - Set_Comprehension_Pointfree_Examples - Parallel_Example - IArray_Examples - Simps_Case_Conv_Examples - ML - Rewrite_Examples - SAT_Examples - SOS - SOS_Cert - Ballot - Erdoes_Szekeres - Sum_of_Powers - Sudoku - Code_Timing - Perm_Fragments - Argo_Examples + Tree23 + Unification + While_Combinator_Example Word_Type veriT_Preprocessing theories [skip_proofs = false] Meson_Test - document_files "root.bib" "root.tex" -session "HOL-Isar_Examples" in Isar_Examples = HOL + +session "HOL-Isar_Examples" in Isar_Examples = "HOL-Computational_Algebra" + description {* Miscellaneous Isabelle/Isar examples. *} options [quick_and_dirty] - sessions - "HOL-Library" - "HOL-Computational_Algebra" theories [document = false] "~~/src/HOL/Library/Lattice_Syntax" "../Computational_Algebra/Primes" @@ -714,12 +681,10 @@ Examples Examples_FOL -session "HOL-SET_Protocol" (timing) in SET_Protocol = HOL + +session "HOL-SET_Protocol" (timing) in SET_Protocol = "HOL-Library" + description {* Verification of the SET Protocol. *} - sessions - "HOL-Library" theories [document = false] "~~/src/HOL/Library/Nat_Bijection" theories @@ -771,8 +736,6 @@ ATP_Problem_Import session "HOL-Probability" (main timing) in "Probability" = "HOL-Analysis" + - sessions - "HOL-Library" theories [document = false] "~~/src/HOL/Library/Countable" "~~/src/HOL/Library/Permutation" @@ -889,7 +852,7 @@ StateSpaceEx document_files "root.tex" -session "HOL-Nonstandard_Analysis" (timing) in Nonstandard_Analysis = HOL + +session "HOL-Nonstandard_Analysis" (timing) in Nonstandard_Analysis = "HOL-Computational_Algebra" + description {* Nonstandard analysis. *} @@ -899,8 +862,6 @@ session "HOL-Nonstandard_Analysis-Examples" (timing) in "Nonstandard_Analysis/Examples" = "HOL-Nonstandard_Analysis" + options [document = false] - sessions - "HOL-Computational_Algebra" theories NSPrimes @@ -1034,13 +995,11 @@ Hotel_Example Quickcheck_Narrowing_Examples -session "HOL-Quotient_Examples" (timing) in Quotient_Examples = HOL + +session "HOL-Quotient_Examples" (timing) in Quotient_Examples = "HOL-Library" + description {* Author: Cezary Kaliszyk and Christian Urban *} options [document = false] - sessions - "HOL-Library" theories DList Quotient_FSet diff -r 701bb74c5f97 -r d164c4fc0d2c src/HOL/ex/document/root.bib --- a/src/HOL/ex/document/root.bib Fri Apr 21 21:37:01 2017 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,111 +0,0 @@ -@inproceedings{HuttonW04,author={Graham Hutton and Joel Wright}, -title={Compiling Exceptions Correctly}, -booktitle={Proc.\ Conf.\ Mathematics of Program Construction}, -year=2004,note={To appear}} - -@InProceedings{Kamm-et-al:1999, - author = {Florian Kamm{\"u}ller and Markus Wenzel and - Lawrence C. Paulson}, - title = {Locales: A Sectioning Concept for {Isabelle}}, - booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '99}, - editor = {Bertot, Y. and Dowek, G. and Hirschowitz, A. and - Paulin, C. and Thery, L.}, - series = {LNCS}, - volume = 1690, - year = 1999} - -@InProceedings{Naraschewski-Wenzel:1998, - author = {Wolfgang Naraschewski and Markus Wenzel}, - title = {Object-Oriented Verification based on Record Subtyping in - {H}igher-{O}rder {L}ogic}, - booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '98}, - editor = {Jim Grundy and Malcom Newey}, - series = {LNCS}, - volume = 1479, - year = 1998} - -@Manual{Nipkow-et-al:2001:HOL, - author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel}, - title = {{Isabelle}'s Logics: {HOL}}, - institution = {Institut f{\"u}r Informatik, Technische Universi{\"a}t - M{\"u}nchen and Computer Laboratory, University of Cambridge}, - year = 2001, - note = {Part of the Isabelle distribution, - \url{http://isabelle.in.tum.de/doc/logics-HOL.pdf}} -} - -@Article{Paulson:1989, - author = {L. C. Paulson}, - title = {The foundation of a generic Theorem Prover}, - journal = {Journal of Automated Reasoning}, - year = 1989, - volume = 5, - number = 3, - pages = {363--397} -} - -@Book{Paulson:1994:Isabelle, - author = {L. C. Paulson and T. Nipkow}, - title = {{Isabelle}: A Generic Theorem Prover}, - year = 1994, - series = {LNCS}, - volume = {828}, - publisher = {Springer} -} - -@InProceedings{Wenzel:1999, - author = {Markus Wenzel}, - title = {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents}, - booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '99}, - editor = {Bertot, Y. and Dowek, G. and Hirschowitz, A. and - Paulin, C. and Thery, L.}, - series = {LNCS}, - volume = 1690, - year = 1999} - -@Unpublished{Wenzel:2001:Isar-examples, - author = {Markus Wenzel}, - title = {Miscellaneous {I}sabelle/{I}sar examples for - Higher-Order Logic}, - year = 2001, - note = {Part of the Isabelle distribution, - \url{http://isabelle.in.tum.de/library/HOL/Isar_Examples/document.pdf}} -} - -@PhdThesis{Wenzel:2001:Thesis, - author = {Markus Wenzel}, - title = {Isabelle/Isar --- a versatile environment for human-readable - formal proof documents}, - school = {Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen}, - year = 2001, - month = {September}, - note = {Submitted} -} -@Manual{Wenzel:2001:isar-ref, - author = {Markus Wenzel}, - title = {The {Isabelle/Isar} Reference Manual}, - year = 2001, - institution = {TU M{\"u}nchen}, - note = {Part of the Isabelle distribution, - \url{http://isabelle.in.tum.de/doc/isar-ref.pdf}} -} - -@Book{isabelle-hol-book, - author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel}, - title = {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic}, - publisher = {Springer}, - year = 2002, - note = {LNCS 2283}} - -@Misc{McMillan-LectureNotes, - author = {Ken McMillan}, - title = {Lecture notes on verification of digital and hybrid systems}, - note = {{NATO} summer school, \url{http://www-cad.eecs.berkeley.edu/~kenmcmil/tutorial/toc.html}} -} - -@PhdThesis{McMillan-PhDThesis, - author = {Ken McMillan}, - title = {Symbolic Model Checking: an approach to the state explosion problem}, - school = {Carnegie Mellon University}, - year = 1992 -} \ No newline at end of file diff -r 701bb74c5f97 -r d164c4fc0d2c src/HOL/ex/document/root.tex --- a/src/HOL/ex/document/root.tex Fri Apr 21 21:37:01 2017 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,27 +0,0 @@ -\documentclass[11pt,a4paper]{article} -\usepackage{isabelle,isabellesym} -\usepackage[utf8]{inputenc} -\usepackage[english]{babel} -\usepackage{textcomp} -\usepackage{amssymb} -\usepackage{wasysym} -\usepackage{pdfsetup} - -\urlstyle{rm} -\isabellestyle{it} - - -\begin{document} - -\title{Miscellaneous HOL Examples} -\maketitle - -\tableofcontents - -\parindent 0pt\parskip 0.5ex -\input{session} - -\bibliographystyle{abbrv} -\bibliography{root} - -\end{document}