isabelle: File revisions

src/HOL/Library/positivstellensatz.ML

2013-05-17	wenzelm	2013-05-17	tuned signature;	file \| diff \| annotate
2013-04-18	wenzelm	2013-04-18	simplifier uses proper Proof.context instead of historic type simpset;	file \| diff \| annotate
2012-02-22	huffman	2012-02-22	tuned whitespace	file \| diff \| annotate
2012-02-15	wenzelm	2012-02-15	renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;	file \| diff \| annotate
2011-11-27	wenzelm	2011-11-27	more antiquotations;	file \| diff \| annotate
2011-08-22	huffman	2011-08-22	avoid warnings	file \| diff \| annotate
2011-08-08	wenzelm	2011-08-08	misc tuning -- eliminated old-fashioned rep_thm;	file \| diff \| annotate
2010-05-07	krauss	2010-05-07	spelling	file \| diff \| annotate
2010-09-02	haftmann	2010-09-02	Table.map replaces Table.map'	file \| diff \| annotate
2010-08-27	wenzelm	2010-08-27	disposed some old debugging tools;	file \| diff \| annotate
2010-08-27	haftmann	2010-08-27	formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj	file \| diff \| annotate
2010-08-19	haftmann	2010-08-19	tuned quotes	file \| diff \| annotate
2010-08-19	haftmann	2010-08-19	use antiquotations for remaining unqualified constants in HOL	file \| diff \| annotate
2010-06-28	haftmann	2010-06-28	explicit is better than implicit	file \| diff \| annotate
2010-05-25	wenzelm	2010-05-25	eliminated various catch-all exception patterns, guessing at the concrete exeptions that are intended here;	file \| diff \| annotate
2010-05-15	wenzelm	2010-05-15	less pervasive names from structure Thm;	file \| diff \| annotate
2010-05-07	haftmann	2010-05-07	renamed Normalizer to the more specific Semiring_Normalizer	file \| diff \| annotate
2010-05-07	haftmann	2010-05-07	split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces	file \| diff \| annotate
2010-05-06	haftmann	2010-05-06	former free-floating field_comp_conv now in structure Normalizer	file \| diff \| annotate
2010-05-06	haftmann	2010-05-06	dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML	file \| diff \| annotate
2010-02-27	wenzelm	2010-02-27	modernized structure Term_Ord;	file \| diff \| annotate
2010-02-05	haftmann	2010-02-05	more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS	file \| diff \| annotate
2009-11-05	wenzelm	2009-11-05	tuned header; use plain simultaneous lemma statements -- Pure's &&& should hardly ever occur in user space;	file \| diff \| annotate
2009-10-22	haftmann	2009-10-22	map_range (and map_index) combinator	file \| diff \| annotate
2009-10-21	haftmann	2009-10-21	curried union as canonical list operation	file \| diff \| annotate
2009-10-21	haftmann	2009-10-21	merged	file \| diff \| annotate
2009-10-21	haftmann	2009-10-21	dropped redundant gen_ prefix	file \| diff \| annotate
2009-10-21	wenzelm	2009-10-21	standardized basic operations on type option;	file \| diff \| annotate
2009-10-19	wenzelm	2009-10-19	uniform use of Integer.add/mult/sum/prod;	file \| diff \| annotate
2009-10-01	wenzelm	2009-10-01	moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;	file \| diff \| annotate
2009-09-30	Philipp Meyer	2009-09-30	tuned FuncFun and FuncUtil structure in positivstellensatz.ML	file \| diff \| annotate
2009-09-22	Philipp Meyer	2009-09-22	removed opening of structures	file \| diff \| annotate
2009-09-29	wenzelm	2009-09-29	explicit indication of Unsynchronized.ref;	file \| diff \| annotate
2009-09-22	Philipp Meyer	2009-09-22	used standard fold function and type aliases	file \| diff \| annotate
2009-09-21	Philipp Meyer	2009-09-21	sos method generates and uses proof certificates	file \| diff \| annotate
2009-08-26	boehmes	2009-08-26	added further conversions and conversionals	file \| diff \| annotate
2009-07-09	wenzelm	2009-07-09	renamed functor TableFun to Table, and GraphFun to Graph;	file \| diff \| annotate
2009-05-12	chaieb	2009-05-12	A generic arithmetic prover based on Positivstellensatz certificates --- also implements Fourrier-Motzkin elimination as a special case Fourrier-Motzkin elimination	file \| diff \| annotate

isabelle

RSS Atom