isabelle: src/Provers/README@38f96394c099 (annotated)

4623 e6ada440a383 updated; wenzelm parents: 4289 diff changeset	1	Provers: generic theorem proving tools
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	2
a5a9c433f639 Initial revision clasohm parents: diff changeset	3	This directory contains ML sources of generic theorem proving tools.
a5a9c433f639 Initial revision clasohm parents: diff changeset	4	Typically, they can be applied to various logics, provided rules of a
3279 815ef5848324 tuned all READMEs; wenzelm parents: 195 diff changeset	5	certain form are derivable. Some of these are documented in the
195 1315ce07f515 added mention of simplifier, splitter, hypsubst lcp parents: 0 diff changeset	6	Reference Manual.
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	7
4623 e6ada440a383 updated; wenzelm parents: 4289 diff changeset	8	blast.ML generic tableau prover with proof reconstruction
4654 dbeae12ada20 added clasimp.ML; wenzelm parents: 4623 diff changeset	9	clasimp.ML combination of classical reasoner and simplifier
4623 e6ada440a383 updated; wenzelm parents: 4289 diff changeset	10	classical.ML theorem prover for classical logics
e6ada440a383 updated; wenzelm parents: 4289 diff changeset	11	hypsubst.ML tactic to substitute in the hypotheses
e6ada440a383 updated; wenzelm parents: 4289 diff changeset	12	ind.ML a simple induction package
e6ada440a383 updated; wenzelm parents: 4289 diff changeset	13	quantifier1.ML simplification procedures for "1 point rules"
e6ada440a383 updated; wenzelm parents: 4289 diff changeset	14	simp.ML powerful but slow simplifier
e6ada440a383 updated; wenzelm parents: 4289 diff changeset	15	simplifier.ML fast simplifier
5680 4f526bcd3a68 split_paired_all.ML: turn surjective pairing into split rule; wenzelm parents: 4654 diff changeset	16	split_paired_all.ML turn surjective pairing into split rule
4623 e6ada440a383 updated; wenzelm parents: 4289 diff changeset	17	splitter.ML performs case splits for simplifier.ML
e6ada440a383 updated; wenzelm parents: 4289 diff changeset	18	typedsimp.ML basic simplifier for explicitly typed logics
4289 5c1bfefd39b7 tuned; wenzelm parents: 3279 diff changeset	19
5c1bfefd39b7 tuned; wenzelm parents: 3279 diff changeset	20	directory Arith:
4623 e6ada440a383 updated; wenzelm parents: 4289 diff changeset	21	cancel_factor.ML cancel common constant factor
e6ada440a383 updated; wenzelm parents: 4289 diff changeset	22	cancel_sums.ML cancel common summands
e6ada440a383 updated; wenzelm parents: 4289 diff changeset	23	nat_transitive.ML simple package for inequalities over nat

author	paulson
	Fri, 18 Feb 2000 15:35:29 +0100
changeset 8255	38f96394c099
parent 5897	b3548f939dd2
child 8870	e900a58cafe4
permissions	-rw-r--r--