isabelle: src/HOL/README.html@652719832159 (annotated)

15283 f21466450330 DOCTYPE declaration added webertj parents: 14543 diff changeset	1	<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
f21466450330 DOCTYPE declaration added webertj parents: 14543 diff changeset	2
15582 7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	3	<!-- $Id$ -->
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	4
10163 d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	5	<html>
d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	6
15582 7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	7	<head>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	8	<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	9	<title>HOL/README</title>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	10	</head>
1339 f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL" clasohm parents: diff changeset	11
10163 d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	12	<body>
d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	13
d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	14	<h2>HOL: Higher-Order Logic</h2>
1339 f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL" clasohm parents: diff changeset	15
10262 3c43e8086cba tuned; wenzelm parents: 10163 diff changeset	16	These are the main sources of the Isabelle system for Higher-Order Logic.
10163 d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	17
d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	18	<p>
2080 12eed4cec935 Fuller description of examples paulson parents: 1341 diff changeset	19
10163 d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	20	There are also several example sessions:
d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	21	<dl>
2080 12eed4cec935 Fuller description of examples paulson parents: 1341 diff changeset	22
10163 d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	23	<dt>Algebra
d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	24	<dd>rings and univariate polynomials
d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	25
d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	26	<dt>Auth
d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	27	<dd>a new approach to verifying authentication protocols
7303 96bc013c8987 AxClasses, Isar_examples; wenzelm parents: 7291 diff changeset	28
10163 d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	29	<dt>AxClasses
d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	30	<dd>a few basic examples of using axiomatic type classes
d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	31
15910 5df57194d064 * empty log message * nipkow parents: 15582 diff changeset	32	<dt>Complex
14024 213dcc39358f HOL-Real -> HOL-Complex kleing parents: 13852 diff changeset	33	<dd>a development of the complex numbers, the reals, and the hyper-reals,
213dcc39358f HOL-Real -> HOL-Complex kleing parents: 13852 diff changeset	34	which are used in non-standard analysis (builds the image HOL-Complex)
7303 96bc013c8987 AxClasses, Isar_examples; wenzelm parents: 7291 diff changeset	35
10163 d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	36	<dt>Hoare
d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	37	<dd>verification of imperative programs (verification conditions are
d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	38	generated automatically from pre/post conditions and loop invariants)
7691 b7e8277fa088 added BVC; wenzelm parents: 7662 diff changeset	39
15910 5df57194d064 * empty log message * nipkow parents: 15582 diff changeset	40	<dt>HoareParallel
5df57194d064 * empty log message * nipkow parents: 15582 diff changeset	41	<dd>verification of shared-variable imperative programs a la Owicki-Gries.
5df57194d064 * empty log message * nipkow parents: 15582 diff changeset	42	(verification conditions are generated automatically)
5df57194d064 * empty log message * nipkow parents: 15582 diff changeset	43
5df57194d064 * empty log message * nipkow parents: 15582 diff changeset	44	<dt>Hyperreal
5df57194d064 * empty log message * nipkow parents: 15582 diff changeset	45	<dd>Nonstandard analysis. Builds on Real and is part of Complex.
5df57194d064 * empty log message * nipkow parents: 15582 diff changeset	46
10163 d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	47	<dt>IMP
d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	48	<dd>mechanization of a large part of a semantics text by Glynn Winskel
7291 8aa66ddc0bea new entriues. nipkow parents: 7290 diff changeset	49
10163 d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	50	<dt>IMPP
d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	51	<dd>extension of IMP with local variables and mutually recursive
d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	52	procedures
2080 12eed4cec935 Fuller description of examples paulson parents: 1341 diff changeset	53
15910 5df57194d064 * empty log message * nipkow parents: 15582 diff changeset	54	<dt>Import
5df57194d064 * empty log message * nipkow parents: 15582 diff changeset	55	<dd>theories imported from other (HOL) theorem provers.
10163 d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	56
d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	57	<dt>Induct
d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	58	<dd>examples of (co)inductive definitions
3125 3f0ab2c306f7 Moved induction examples to directory Induct paulson parents: 2080 diff changeset	59
15910 5df57194d064 * empty log message * nipkow parents: 15582 diff changeset	60	<dt>IOA
5df57194d064 * empty log message * nipkow parents: 15582 diff changeset	61	<dd>a simple theory of Input/Output Automata
5df57194d064 * empty log message * nipkow parents: 15582 diff changeset	62
33026 8f35633c4922 modernized session Isar_Examples; wenzelm parents: 31795 diff changeset	63	<dt>Isar_Examples
10163 d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	64	<dd>several introductory examples using Isabelle/Isar
2080 12eed4cec935 Fuller description of examples paulson parents: 1341 diff changeset	65
10163 d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	66	<dt>Lambda
d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	67	<dd>fundamental properties of lambda-calculus (Church-Rosser and termination)
2080 12eed4cec935 Fuller description of examples paulson parents: 1341 diff changeset	68
10163 d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	69	<dt>Lattice
d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	70	<dd>lattices and order structures (in Isabelle/Isar)
7303 96bc013c8987 AxClasses, Isar_examples; wenzelm parents: 7291 diff changeset	71
15910 5df57194d064 * empty log message * nipkow parents: 15582 diff changeset	72	<dt>Library
5df57194d064 * empty log message * nipkow parents: 15582 diff changeset	73	<dd>A collection of generic theories
5df57194d064 * empty log message * nipkow parents: 15582 diff changeset	74
5df57194d064 * empty log message * nipkow parents: 15582 diff changeset	75	<dt>Matrix
5df57194d064 * empty log message * nipkow parents: 15582 diff changeset	76	<dd>two-dimensional matrices
5df57194d064 * empty log message * nipkow parents: 15582 diff changeset	77
10163 d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	78	<dt>MicroJava
d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	79	<dd>formalization of a fragment of Java, together with a corresponding
d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	80	virtual machine and a specification of its bytecode verifier and a
15910 5df57194d064 * empty log message * nipkow parents: 15582 diff changeset	81	lightweight bytecode verifier, including proofs of type-safety
7291 8aa66ddc0bea new entriues. nipkow parents: 7290 diff changeset	82
10163 d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	83	<dt>Modelcheck
d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	84	<dd>basic setup for integration of some model checkers in Isabelle/HOL
7290 f1a37c379317 updated paulson parents: 4622 diff changeset	85
15910 5df57194d064 * empty log message * nipkow parents: 15582 diff changeset	86	<dt>NanoJava
5df57194d064 * empty log message * nipkow parents: 15582 diff changeset	87	<dd>Haore Logic for a tiny fragment of Java
5df57194d064 * empty log message * nipkow parents: 15582 diff changeset	88
10163 d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	89	<dt>NumberTheory
d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	90	<dd>fundamental Theorem of Arithmetic, Chinese Remainder Theorem,
15910 5df57194d064 * empty log message * nipkow parents: 15582 diff changeset	91	Fermat/Euler Theorem, Wilson's Theorem, Quadratic Reciprocity
7662 062a782d7402 Real/HahnBanach; wenzelm parents: 7303 diff changeset	92
10163 d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	93	<dt>Prolog
d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	94	<dd>a (bare-bones) implementation of Lambda-Prolog
d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	95
15910 5df57194d064 * empty log message * nipkow parents: 15582 diff changeset	96	<dt>Real
5df57194d064 * empty log message * nipkow parents: 15582 diff changeset	97	<dd>the real numbers, part of Complex
5df57194d064 * empty log message * nipkow parents: 15582 diff changeset	98
31795 be3e1cc5005c standard naming conventions for session and theories; wenzelm parents: 15916 diff changeset	99	<dt>Hahn_Banach
15910 5df57194d064 * empty log message * nipkow parents: 15582 diff changeset	100	<dd>the Hahn-Banach theorem for real vector spaces (in Isabelle/Isar)
5df57194d064 * empty log message * nipkow parents: 15582 diff changeset	101
33028 9aa8bfb1649d modernized session SET_Protocol; wenzelm parents: 33026 diff changeset	102	<dt>SET_Protocol
15910 5df57194d064 * empty log message * nipkow parents: 15582 diff changeset	103	<dd>verification of the SET Protocol
5df57194d064 * empty log message * nipkow parents: 15582 diff changeset	104
10163 d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	105	<dt>Subst
15910 5df57194d064 * empty log message * nipkow parents: 15582 diff changeset	106	<dd>a theory of substitution and unification.
7290 f1a37c379317 updated paulson parents: 4622 diff changeset	107
10163 d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	108	<dt>TLA
d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	109	<dd>Lamport's Temporal Logic of Actions (with separate example sessions)
7291 8aa66ddc0bea new entriues. nipkow parents: 7290 diff changeset	110
10163 d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	111	<dt>UNITY
d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	112	<dd>Chandy and Misra's UNITY formalism
7290 f1a37c379317 updated paulson parents: 4622 diff changeset	113
10163 d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	114	<dt>W0
d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	115	<dd>a precursor of MiniML, without let-expressions
7291 8aa66ddc0bea new entriues. nipkow parents: 7290 diff changeset	116
10163 d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	117	<dt>ex
d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	118	<dd>miscellaneous examples
d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	119
d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	120	</dl>
1339 f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL" clasohm parents: diff changeset	121
10163 d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	122	</body>
d1972b445ece updated, improved; wenzelm parents: 9811 diff changeset	123	</html>

author	blanchet
	Mon, 14 Dec 2009 10:59:46 +0100
changeset 34083	652719832159
parent 33028	9aa8bfb1649d
child 36862	952b2b102a0a
permissions	-rw-r--r--