isabelle: File revisions

src/HOL/IsaMakefile

2009-02-09	chaieb	2009-02-09	added Determinants to Library	file \| diff \| annotate
2009-02-09	chaieb	2009-02-09	added Euclidean_Space and Glbs to Library	file \| diff \| annotate
2009-02-09	chaieb	2009-02-09	Added HOL/Library/Finite_Cartesian_Product.thy to Library	file \| diff \| annotate
2009-02-06	haftmann	2009-02-06	session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there	file \| diff \| annotate
2009-02-06	chaieb	2009-02-06	fixed dependencies : Theory Dense_Linear_Order moved to Library	file \| diff \| annotate
2009-02-05	haftmann	2009-02-05	merged	file \| diff \| annotate
2009-02-05	haftmann	2009-02-05	moved Random.thy to Library	file \| diff \| annotate
2009-02-05	hoelzl	2009-02-05	Add approximation method	file \| diff \| annotate
2009-02-05	hoelzl	2009-02-05	Added new Float theory and moved old Library/Float.thy to ComputeFloat	file \| diff \| annotate
2009-02-03	haftmann	2009-02-03	merged Big0	file \| diff \| annotate
2009-02-03	haftmann	2009-02-03	established session HOL-Reflection	file \| diff \| annotate
2009-02-16	wenzelm	2009-02-16	removed obsolete axclass manual and examples;	file \| diff \| annotate
2009-02-02	haftmann	2009-02-02	added Mapping.thy to Library	file \| diff \| annotate
2009-01-30	krauss	2009-01-30	fixed case	file \| diff \| annotate
2009-01-30	chaieb	2009-01-30	Added Formal_Power_Series_Examples to HOL-ex image	file \| diff \| annotate
2009-01-29	chaieb	2009-01-29	Inserted Formal_Power_Series.thy under Library	file \| diff \| annotate
2009-01-28	haftmann	2009-01-28	Reflection.thy now in HOL/Library	file \| diff \| annotate
2009-01-26	haftmann	2009-01-26	entry point for Word library now named Word	file \| diff \| annotate
2009-01-17	haftmann	2009-01-17	no document for HOL-Base	file \| diff \| annotate
2009-01-16	haftmann	2009-01-16	added HOL-Base image	file \| diff \| annotate
2009-01-12	huffman	2009-01-12	add Polynomial.thy to makefile	file \| diff \| annotate
2009-01-08	haftmann	2009-01-08	split of Imperative_HOL theories from HOL-Library	file \| diff \| annotate
2008-12-29	haftmann	2008-12-29	adapted HOL source structure to distribution layout	file \| diff \| annotate
2008-12-27	krauss	2008-12-27	renamed LexOrds.thy to Termination.thy; examples for sizechange method	file \| diff \| annotate
2008-12-16	krauss	2008-12-16	method "sizechange" proves termination of functions; added more infrastructure for termination proofs	file \| diff \| annotate
2008-12-15	nipkow	2008-12-15	merged	file \| diff \| annotate
2008-12-11	nipkow	2008-12-11	Testfile for Stefan's code generator	file \| diff \| annotate
2008-12-15	haftmann	2008-12-15	moved value.ML to src/Tools	file \| diff \| annotate
2008-12-10	nipkow	2008-12-10	moved ContNotDenum into Library	file \| diff \| annotate
2008-12-03	haftmann	2008-12-03	made repository layout more coherent with logical distribution structure; stripped some $Id$s	file \| diff \| annotate
2008-11-29	nipkow	2008-11-29	new file float_syntax.ML	file \| diff \| annotate
2008-11-17	wenzelm	2008-11-17	removed Induct/Mutil.thy -- the file has been moved to AFP;	file \| diff \| annotate
2008-11-15	wenzelm	2008-11-15	clean: added HOL-Main;	file \| diff \| annotate
2008-11-13	haftmann	2008-11-13	moved assert to Heap_Monad.thy	file \| diff \| annotate
2008-10-21	berghofe	2008-10-21	Added nominal_inductive2.ML	file \| diff \| annotate
2008-10-17	wenzelm	2008-10-17	reactivated HOL-Matrix; minor cleanup;	file \| diff \| annotate
2008-10-16	ballarin	2008-10-16	Removed ex/Locales.thy.	file \| diff \| annotate
2008-10-14	wenzelm	2008-10-14	renamed AtpThread to AtpWrapper;	file \| diff \| annotate
2008-10-04	wenzelm	2008-10-04	replaced ISATOOL by ISABELLE_TOOL;	file \| diff \| annotate
2008-10-03	wenzelm	2008-10-03	version of sledgehammer using threads instead of processes, misc cleanup; (by Fabian Immler);	file \| diff \| annotate
2008-10-03	wenzelm	2008-10-03	removed old/unused setup of raw ATP oracles;	file \| diff \| annotate
2008-09-29	haftmann	2008-09-29	separate HOL-Main image	file \| diff \| annotate
2008-09-28	wenzelm	2008-09-28	HOL no longer depends on HOL-Plain;	file \| diff \| annotate
2008-09-27	wenzelm	2008-09-27	HOL_USEDIR_OPTIONS no longer applies to HOL-Plain (main HOL is rebuilt from Pure);	file \| diff \| annotate
2008-09-22	berghofe	2008-09-22	Added coherent logic prover.	file \| diff \| annotate
2008-09-22	haftmann	2008-09-22	different session branches for HOL-Plain vs. Plain	file \| diff \| annotate
2008-09-16	haftmann	2008-09-16	moved term_of syntax to separate theory	file \| diff \| annotate
2008-09-16	haftmann	2008-09-16	generic value command	file \| diff \| annotate
2008-09-03	nipkow	2008-09-03	removed ex/Puzzle	file \| diff \| annotate
2008-09-02	nipkow	2008-09-02	Replaced Library/NatPair by Nat_Int_Bij.	file \| diff \| annotate
2008-08-28	haftmann	2008-08-28	restructured and split code serializer module	file \| diff \| annotate
2008-08-27	haftmann	2008-08-27	added HOL/ex/Numeral.thy	file \| diff \| annotate
2008-08-05	krauss	2008-08-05	fix HOL/ex/LexOrds.thy; add to regression	file \| diff \| annotate
2008-08-01	ballarin	2008-08-01	Generalised polynomial lemmas from cring to ring.	file \| diff \| annotate
2008-07-30	ballarin	2008-07-30	New locales for orders and lattices where the equivalence relation is not restricted to equality.	file \| diff \| annotate
2008-07-29	ballarin	2008-07-29	New theory on divisibility; Restructured presentation.	file \| diff \| annotate
2008-07-29	haftmann	2008-07-29	corrected Pure dependency	file \| diff \| annotate
2008-07-25	haftmann	2008-07-25	tuned	file \| diff \| annotate
2008-07-21	haftmann	2008-07-21	(adjusted)	file \| diff \| annotate
2008-07-16	berghofe	2008-07-16	Added Standardization theory to nominal examples.	file \| diff \| annotate

isabelle

RSS Atom