# HG changeset patch # User wenzelm # Date 1492803409 -7200 # Node ID b7caa2b8bdbfdc027e4cacc9604eac66fa78b206 # Parent 42c4b87e98c27c20d87981e78ca1a3afdb0c02d8 removed pointless document; diff -r 42c4b87e98c2 -r b7caa2b8bdbf src/HOL/ROOT --- a/src/HOL/ROOT Fri Apr 21 21:06:02 2017 +0200 +++ b/src/HOL/ROOT Fri Apr 21 21:36:49 2017 +0200 @@ -577,23 +577,19 @@ description {* Miscellaneous examples for Higher-Order Logic. *} + options [document = false] sessions "HOL-Library" "HOL-Number_Theory" - theories [document = false] - "~~/src/HOL/Library/State_Monad" + theories Code_Binary_Nat_examples - "~~/src/HOL/Library/FuncSet" Eval_Examples Normalization_by_Evaluation Hebrew Chinese Serbian - "~~/src/HOL/Library/Refute" - "~~/src/HOL/Library/Transitive_Closure_Table" Cartouche_Examples Computations - theories Commands Adhoc_Overloading_Examples Iff_Oracle @@ -669,7 +665,6 @@ veriT_Preprocessing theories [skip_proofs = false] Meson_Test - document_files "root.bib" "root.tex" session "HOL-Isar_Examples" in Isar_Examples = HOL + description {* diff -r 42c4b87e98c2 -r b7caa2b8bdbf src/HOL/ex/document/root.bib --- a/src/HOL/ex/document/root.bib Fri Apr 21 21:06:02 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 42c4b87e98c2 -r b7caa2b8bdbf src/HOL/ex/document/root.tex --- a/src/HOL/ex/document/root.tex Fri Apr 21 21:06:02 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}