--- a/src/Benchmarks/ROOT Tue Nov 20 13:44:06 2018 +0100
+++ b/src/Benchmarks/ROOT Tue Nov 20 13:46:13 2018 +0100
@@ -1,9 +1,9 @@
chapter HOL
session "HOL-Datatype_Benchmark" in Datatype_Benchmark = "HOL-Library" +
- description \<open>
+ description "
Big (co)datatypes.
-\<close>
+ "
theories
Brackin
IsaFoR
@@ -17,8 +17,8 @@
Needham_Schroeder_Unguided_Attacker_Example
session "HOL-Record_Benchmark" in Record_Benchmark = HOL +
- description \<open>
+ description "
Big records.
-\<close>
+ "
theories
Record_Benchmark
--- a/src/CCL/ROOT Tue Nov 20 13:44:06 2018 +0100
+++ b/src/CCL/ROOT Tue Nov 20 13:46:13 2018 +0100
@@ -1,7 +1,7 @@
chapter CCL
session CCL = Pure +
- description \<open>
+ description "
Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
@@ -9,13 +9,12 @@
A computational logic for an untyped functional language with
evaluation to weak head-normal form.
-\<close>
+ "
sessions
FOL
theories
Wfd
Fix
-
(* Examples for Classical Computational Logic *)
"ex/Nat"
"ex/List"
--- a/src/CTT/ROOT Tue Nov 20 13:44:06 2018 +0100
+++ b/src/CTT/ROOT Tue Nov 20 13:46:13 2018 +0100
@@ -1,7 +1,7 @@
chapter CTT
session CTT = Pure +
- description \<open>
+ description "
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
@@ -15,7 +15,7 @@
Simon Thompson, Type Theory and Functional Programming (Addison-Wesley,
1991)
-\<close>
+ "
options [thy_output_source]
theories
CTT
--- a/src/Cube/ROOT Tue Nov 20 13:44:06 2018 +0100
+++ b/src/Cube/ROOT Tue Nov 20 13:46:13 2018 +0100
@@ -1,7 +1,7 @@
chapter Cube
session Cube = Pure +
- description \<open>
+ description "
Author: Tobias Nipkow
Copyright 1992 University of Cambridge
@@ -12,5 +12,5 @@
For more information about the Lambda-Cube, see H. Barendregt, Introduction
to Generalised Type Systems, J. Functional Programming.
-\<close>
+ "
theories Example
--- a/src/FOL/ROOT Tue Nov 20 13:44:06 2018 +0100
+++ b/src/FOL/ROOT Tue Nov 20 13:46:13 2018 +0100
@@ -1,7 +1,7 @@
chapter FOL
session FOL = Pure +
- description \<open>
+ description "
First-Order Logic with Natural Deduction (constructive and classical
versions). For a classical sequent calculus, see Isabelle/LK.
@@ -14,16 +14,16 @@
Antony Galton, Logic for Information Technology (Wiley, 1990)
Michael Dummett, Elements of Intuitionism (Oxford, 1977)
-\<close>
+ "
theories
IFOL (global)
FOL (global)
document_files "root.tex"
session "FOL-ex" in ex = FOL +
- description \<open>
+ description "
Examples for First-Order Logic.
-\<close>
+ "
theories
Natural_Numbers
Intro
--- a/src/FOLP/ROOT Tue Nov 20 13:44:06 2018 +0100
+++ b/src/FOLP/ROOT Tue Nov 20 13:46:13 2018 +0100
@@ -1,25 +1,25 @@
chapter FOLP
session FOLP = Pure +
- description \<open>
+ description "
Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Modifed version of FOL that contains proof terms.
Presence of unknown proof term means that matching does not behave as expected.
-\<close>
+ "
theories
IFOLP (global)
FOLP (global)
session "FOLP-ex" in ex = FOLP +
- description \<open>
+ description "
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
Examples for First-Order Logic.
-\<close>
+ "
theories
Intro
Nat
--- a/src/HOL/ROOT Tue Nov 20 13:44:06 2018 +0100
+++ b/src/HOL/ROOT Tue Nov 20 13:46:13 2018 +0100
@@ -1,9 +1,9 @@
chapter HOL
session HOL (main) = Pure +
- description \<open>
+ description "
Classical Higher-order Logic.
-\<close>
+ "
options [strict_facts]
theories
Main (global)
@@ -13,9 +13,9 @@
"root.tex"
session "HOL-Proofs" (timing) = Pure +
- description \<open>
+ description "
HOL-Main with explicit proof terms.
-\<close>
+ "
options [quick_and_dirty = false, record_proofs = 2, parallel_proofs = 0, parallel_limit = 500]
sessions
"HOL-Library"
@@ -23,9 +23,9 @@
"HOL-Library.Realizers"
session "HOL-Library" (main timing) in Library = HOL +
- description \<open>
+ description "
Classical Higher-order Logic -- batteries included.
-\<close>
+ "
theories
Library
(*conflicting type class instantiations and dependent applications*)
@@ -100,7 +100,7 @@
"style.sty"
session "HOL-Hahn_Banach" in Hahn_Banach = "HOL-Library" +
- description \<open>
+ description "
Author: Gertrud Bauer, TU Munich
The Hahn-Banach theorem for real vector spaces.
@@ -116,7 +116,7 @@
The theorem says, that every continous linearform, defined on arbitrary
subspaces (not only one-dimensional subspaces), can be extended to a
continous linearform on the whole vectorspace.
-\<close>
+ "
sessions
"HOL-Analysis"
theories
@@ -124,7 +124,7 @@
document_files "root.bib" "root.tex"
session "HOL-Induct" in Induct = "HOL-Library" +
- description \<open>
+ description "
Examples of (Co)Inductive Definitions.
Comb proves the Church-Rosser theorem for combinators (see
@@ -139,7 +139,7 @@
Exp demonstrates the use of iterated inductive definitions to reason about
mutually recursive relations.
-\<close>
+ "
theories [quick_and_dirty]
Common_Patterns
theories
@@ -202,7 +202,7 @@
This is an extension of IMP with local variables and mutually recursive
procedures. For documentation see "Hoare Logic for Mutual Recursion and
Local Variables" (https://isabelle.in.tum.de/Bali/papers/FSTTCS99.html).
-\<close>
+ \<close>
theories EvenOdd
session "HOL-Data_Structures" (timing) in Data_Structures = HOL +
@@ -233,10 +233,10 @@
theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import
session "HOL-Number_Theory" (main timing) in Number_Theory = "HOL-Computational_Algebra" +
- description \<open>
+ description "
Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler
Theorem, Wilson's Theorem, some lemmas for Quadratic Reciprocity.
-\<close>
+ "
sessions
"HOL-Algebra"
theories
@@ -245,18 +245,18 @@
"root.tex"
session "HOL-Hoare" in Hoare = HOL +
- description \<open>
+ description "
Verification of imperative programs (verification conditions are generated
automatically from pre/post conditions and loop invariants).
-\<close>
+ "
theories Hoare
document_files "root.bib" "root.tex"
session "HOL-Hoare_Parallel" (timing) in Hoare_Parallel = HOL +
- description \<open>
+ description "
Verification of shared-variable imperative programs a la Owicki-Gries.
(verification conditions are generated automatically).
-\<close>
+ "
theories Hoare_Parallel
document_files "root.bib" "root.tex"
@@ -282,12 +282,12 @@
Code_Test_SMLNJ
session "HOL-Metis_Examples" (timing) in Metis_Examples = "HOL-Library" +
- description \<open>
+ description "
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Author: Jasmin Blanchette, TU Muenchen
Testing Metis and Sledgehammer.
-\<close>
+ "
sessions
"HOL-Decision_Procs"
theories
@@ -302,18 +302,18 @@
Sets
session "HOL-Nitpick_Examples" in Nitpick_Examples = "HOL-Library" +
- description \<open>
+ description "
Author: Jasmin Blanchette, TU Muenchen
Copyright 2009
-\<close>
+ "
theories [quick_and_dirty] Nitpick_Examples
session "HOL-Algebra" (main timing) in Algebra = "HOL-Computational_Algebra" +
- description \<open>
+ description "
Author: Clemens Ballarin, started 24 September 1999, and many others
The Isabelle Algebraic Library.
-\<close>
+ "
theories
(* Orders and Lattices *)
Galois_Connection (* Knaster-Tarski theorem and Galois connections *)
@@ -332,9 +332,9 @@
document_files "root.bib" "root.tex"
session "HOL-Auth" (timing) in Auth = "HOL-Library" +
- description \<open>
+ description "
A new approach to verifying authentication protocols.
-\<close>
+ "
theories
Auth_Shared
Auth_Public
@@ -344,12 +344,12 @@
document_files "root.tex"
session "HOL-UNITY" (timing) in UNITY = "HOL-Auth" +
- description \<open>
+ description "
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
Verifying security protocols using Chandy and Misra's UNITY formalism.
-\<close>
+ "
theories
(*Basic meta-theory*)
UNITY_Main
@@ -404,9 +404,9 @@
document_files "root.bib" "root.tex"
session "HOL-Decision_Procs" (timing) in Decision_Procs = "HOL-Algebra" +
- description \<open>
+ description "
Various decision procedures, typically involving reflection.
-\<close>
+ "
theories
Decision_Procs
@@ -419,9 +419,9 @@
XML_Data
session "HOL-Proofs-Extraction" (timing) in "Proofs/Extraction" = "HOL-Proofs" +
- description \<open>
+ description "
Examples for program extraction in Higher-Order Logic.
-\<close>
+ "
options [parallel_proofs = 0, quick_and_dirty = false]
sessions
"HOL-Computational_Algebra"
@@ -442,7 +442,7 @@
The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole
theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html).
-\<close>
+ \<close>
options [print_mode = "no_brackets",
parallel_proofs = 0, quick_and_dirty = false]
sessions
@@ -455,7 +455,7 @@
document_files "root.bib" "root.tex"
session "HOL-Prolog" in Prolog = HOL +
- description \<open>
+ description "
Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
A bare-bones implementation of Lambda-Prolog.
@@ -463,15 +463,15 @@
This is a simple exploratory implementation of Lambda-Prolog in HOL,
including some minimal examples (in Test.thy) and a more typical example of
a little functional language and its type system.
-\<close>
+ "
theories Test Type
session "HOL-MicroJava" (timing) in MicroJava = "HOL-Library" +
- description \<open>
+ 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.
-\<close>
+ "
sessions
"HOL-Eisbach"
theories
@@ -482,9 +482,9 @@
"root.tex"
session "HOL-NanoJava" in NanoJava = HOL +
- description \<open>
+ description "
Hoare Logic for a tiny fragment of Java.
-\<close>
+ "
theories Example
document_files "root.bib" "root.tex"
@@ -524,22 +524,22 @@
organization={Aarhus University, BRICS report},
year=1995}
ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz
-\<close>
+ \<close>
theories Solve
session "HOL-Lattice" in Lattice = HOL +
- description \<open>
+ description "
Author: Markus Wenzel, TU Muenchen
Basic theory of lattices and orders.
-\<close>
+ "
theories CompleteLattice
document_files "root.tex"
session "HOL-ex" (timing) in ex = "HOL-Number_Theory" +
- description \<open>
+ description "
Miscellaneous examples for Higher-Order Logic.
-\<close>
+ "
theories
Adhoc_Overloading_Examples
Antiquote
@@ -634,9 +634,9 @@
Meson_Test
session "HOL-Isar_Examples" in Isar_Examples = "HOL-Computational_Algebra" +
- description \<open>
+ description "
Miscellaneous Isabelle/Isar examples.
-\<close>
+ "
options [quick_and_dirty]
theories
Knaster_Tarski
@@ -663,7 +663,7 @@
session "HOL-Eisbach" in Eisbach = HOL +
description \<open>
The Eisbach proof method language and "match" method.
-\<close>
+ \<close>
sessions
FOL
theories
@@ -673,24 +673,24 @@
Examples_FOL
session "HOL-SET_Protocol" (timing) in SET_Protocol = "HOL-Library" +
- description \<open>
+ description "
Verification of the SET Protocol.
-\<close>
+ "
theories
SET_Protocol
document_files "root.tex"
session "HOL-Matrix_LP" in Matrix_LP = "HOL-Library" +
- description \<open>
+ description "
Two-dimensional matrices and linear programming.
-\<close>
+ "
theories Cplex
document_files "root.tex"
session "HOL-TLA" in TLA = HOL +
- description \<open>
+ description "
Lamport's Temporal Logic of Actions.
-\<close>
+ "
theories TLA
session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" +
@@ -703,13 +703,13 @@
theories MemoryImplementation
session "HOL-TPTP" in TPTP = "HOL-Library" +
- description \<open>
+ description "
Author: Jasmin Blanchette, TU Muenchen
Author: Nik Sultana, University of Cambridge
Copyright 2011
TPTP-related extensions.
-\<close>
+ "
theories
ATP_Theory_Export
MaSh_Eval
@@ -760,9 +760,9 @@
VC_Condition
session "HOL-Cardinals" (timing) in Cardinals = "HOL-Library" +
- description \<open>
+ description "
Ordinals and Cardinals, Full Theories.
-\<close>
+ "
theories
Cardinals
Bounded_Set
@@ -772,9 +772,9 @@
"root.bib"
session "HOL-Datatype_Examples" (timing) in Datatype_Examples = "HOL-Library" +
- description \<open>
+ description "
(Co)datatype Examples.
-\<close>
+ "
theories
Compat
Lambda_Term
@@ -792,9 +792,9 @@
Misc_Primrec
session "HOL-Corec_Examples" (timing) in Corec_Examples = "HOL-Library" +
- description \<open>
+ description "
Corecursion Examples.
-\<close>
+ "
theories
LFilter
Paper_Examples
@@ -828,9 +828,9 @@
document_files "root.tex"
session "HOL-Nonstandard_Analysis" (timing) in Nonstandard_Analysis = "HOL-Computational_Algebra" +
- description \<open>
+ description "
Nonstandard analysis.
-\<close>
+ "
theories
Nonstandard_Analysis
document_files "root.tex"
@@ -911,9 +911,9 @@
Quickcheck_Narrowing_Examples
session "HOL-Quotient_Examples" (timing) in Quotient_Examples = "HOL-Algebra" +
- description \<open>
+ description "
Author: Cezary Kaliszyk and Christian Urban
-\<close>
+ "
theories
DList
Quotient_FSet
@@ -949,9 +949,9 @@
Reg_Exp_Example
session "HOL-Types_To_Sets" in Types_To_Sets = HOL +
- description \<open>
+ description "
Experimental extension of Higher-Order Logic to allow translation of types to sets.
-\<close>
+ "
theories
Types_To_Sets
"Examples/Prerequisites"
@@ -960,12 +960,12 @@
"Examples/Linear_Algebra_On"
session HOLCF (main timing) in HOLCF = HOL +
- description \<open>
+ description "
Author: Franz Regensburger
Author: Brian Huffman
HOLCF -- a semantic extension of HOL by the LCF logic.
-\<close>
+ "
sessions
"HOL-Library"
theories
@@ -985,11 +985,11 @@
HOL_Cpo
session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF +
- description \<open>
+ description "
IMP -- A WHILE-language and its Semantics.
This is the HOLCF-based denotational semantics of a simple WHILE-language.
-\<close>
+ "
sessions
"HOL-IMP"
theories
@@ -1000,9 +1000,9 @@
"root.bib"
session "HOLCF-ex" in "HOLCF/ex" = "HOLCF-Library" +
- description \<open>
+ description "
Miscellaneous examples for HOLCF.
-\<close>
+ "
theories
Dnat
Dagstuhl
@@ -1030,14 +1030,14 @@
"Specification and Development of Interactive Systems: Focus on Streams,
Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321
-\<close>
+ \<close>
theories
Fstreams
FOCUS
Buffer_adm
session IOA (timing) in "HOLCF/IOA" = HOLCF +
- description \<open>
+ description "
Author: Olaf Mueller
Copyright 1997 TU München
@@ -1046,40 +1046,40 @@
The distribution contains simulation relations, temporal logic, and an
abstraction theory. Everything is based upon a domain-theoretic model of
finite and infinite sequences.
-\<close>
+ "
theories Abstraction
session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
- description \<open>
+ description "
Author: Olaf Mueller
The Alternating Bit Protocol performed in I/O-Automata.
-\<close>
+ "
theories
Correctness
Spec
session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA +
- description \<open>
+ description "
Author: Tobias Nipkow & Konrad Slind
A network transmission protocol, performed in the
I/O automata formalization by Olaf Mueller.
-\<close>
+ "
theories Correctness
session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA +
- description \<open>
+ description "
Author: Olaf Mueller
Memory storage case study.
-\<close>
+ "
theories Correctness
session "IOA-ex" in "HOLCF/IOA/ex" = IOA +
- description \<open>
+ description "
Author: Olaf Mueller
-\<close>
+ "
theories
TrivEx
TrivEx2
--- a/src/LCF/ROOT Tue Nov 20 13:44:06 2018 +0100
+++ b/src/LCF/ROOT Tue Nov 20 13:46:13 2018 +0100
@@ -1,7 +1,7 @@
chapter LCF
session LCF = Pure +
- description \<open>
+ description "
Author: Tobias Nipkow
Copyright 1992 University of Cambridge
@@ -9,12 +9,11 @@
Useful references on LCF: Lawrence C. Paulson,
Logic and Computation: Interactive proof with Cambridge LCF (CUP, 1987)
-\<close>
+ "
sessions
FOL
theories
LCF
-
(* Some examples from Lawrence Paulson's book Logic and Computation *)
"ex/Ex1"
"ex/Ex2"
--- a/src/Pure/ROOT Tue Nov 20 13:44:06 2018 +0100
+++ b/src/Pure/ROOT Tue Nov 20 13:46:13 2018 +0100
@@ -1,9 +1,9 @@
chapter Pure
session Pure =
- description \<open>
- The Pure logical framework
-\<close>
+ description "
+ The Pure logical framework.
+ "
options [threads = 1, export_theory]
theories
Pure (global)
--- a/src/Sequents/ROOT Tue Nov 20 13:44:06 2018 +0100
+++ b/src/Sequents/ROOT Tue Nov 20 13:46:13 2018 +0100
@@ -1,7 +1,7 @@
chapter Sequents
session Sequents = Pure +
- description \<open>
+ description "
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
@@ -36,7 +36,7 @@
S. Kalvala and V. de Paiva, Linear Logic in Isabelle (in TR 379, University
of Cambridge Computer Lab, 1995, ed L. Paulson)
-\<close>
+ "
theories
LK
ILL
@@ -46,7 +46,6 @@
T
S4
S43
-
(* Examples for Classical Logic *)
"LK/Propositional"
"LK/Quantifiers"
--- a/src/ZF/ROOT Tue Nov 20 13:44:06 2018 +0100
+++ b/src/ZF/ROOT Tue Nov 20 13:46:13 2018 +0100
@@ -1,7 +1,7 @@
chapter ZF
session ZF (main timing) = Pure +
- description \<open>
+ description "
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge
@@ -41,7 +41,7 @@
Kenneth Kunen, Set Theory: An Introduction to Independence Proofs,
(North-Holland, 1980)
-\<close>
+ "
sessions
FOL
theories
@@ -63,7 +63,7 @@
http://www.cl.cam.ac.uk/Research/Reports/TR377-lcp-mechanising-set-theory.ps.gz
"Mechanizing Set Theory", by Paulson and Grabczewski, describes both this
development and ZF's theories of cardinals.
-\<close>
+ \<close>
theories
WO6_WO1
WO1_WO7
@@ -78,7 +78,7 @@
document_files "root.tex" "root.bib"
session "ZF-Coind" in Coind = ZF +
- description \<open>
+ description "
Author: Jacob Frost, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge
@@ -99,11 +99,11 @@
Jacob Frost, A Case Study of Co_induction in Isabelle
Report, Computer Lab, University of Cambridge (1995).
http://www.cl.cam.ac.uk/Research/Reports/TR359-jf10008-co-induction-in-isabelle.dvi.gz
-\<close>
+ "
theories ECR
session "ZF-Constructible" in Constructible = ZF +
- description \<open>
+ description "
Relative Consistency of the Axiom of Choice:
Inner Models, Absoluteness and Consistency Proofs.
@@ -121,7 +121,7 @@
A paper describing this development is
http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-551.pdf
-\<close>
+ "
theories
DPow_absolute
AC_in_L
@@ -129,7 +129,7 @@
document_files "root.tex" "root.bib"
session "ZF-IMP" in IMP = ZF +
- description \<open>
+ description "
Author: Heiko Loetzbeyer & Robert Sandner, TUM
Copyright 1994 TUM
@@ -141,19 +141,19 @@
Glynn Winskel. The Formal Semantics of Programming Languages.
MIT Press, 1993.
-\<close>
+ "
theories Equiv
document_files
"root.tex"
"root.bib"
session "ZF-Induct" in Induct = ZF +
- description \<open>
+ description "
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 2001 University of Cambridge
Inductive definitions.
-\<close>
+ "
theories
(** Datatypes **)
Datatypes (*sample datatypes*)
@@ -181,7 +181,7 @@
"root.tex"
session "ZF-Resid" in Resid = ZF +
- description \<open>
+ description "
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge
@@ -196,23 +196,21 @@
See Rasmussen's report: The Church-Rosser Theorem in Isabelle: A Proof
Porting Experiment.
http://www.cl.cam.ac.uk/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz
-\<close>
+ "
theories Confluence
session "ZF-UNITY" (timing) in UNITY = "ZF-Induct" +
- description \<open>
+ description "
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
ZF/UNITY proofs.
-\<close>
+ "
theories
(*Simple examples: no composition*)
Mutex
-
(*Basic meta-theory*)
Guar
-
(*Prefix relation; the Allocator example*)
Distributor Merge ClientImpl AllocImpl
@@ -231,7 +229,7 @@
describes the theoretical foundations of datatypes while
href="http://www.cl.cam.ac.uk/Research/Reports/TR320-lcp-isabelle-ind-defs.dvi.gz
describes the package that automates their declaration.
-\<close>
+ \<close>
theories
misc
Ring (*abstract algebra*)