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

author	blanchet
	Wed, 26 Sep 2012 10:41:36 +0200
changeset 49596	c3536db7e938
parent 36862	952b2b102a0a
permissions	-rw-r--r--