--- 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
--- 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
--- 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}