isabelle: File revisions

Mercurial isabelle / file revisions

NEWS

3 months ago	blanchet	2012-02-04	made option available to users (mostly for experiments)	file \| diff \| annotate
3 months ago	nipkow	2012-01-31	NEWS	file \| diff \| annotate
3 months ago	blanchet	2012-01-30	docs and news	file \| diff \| annotate
3 months ago	bulwahn	2012-01-30	NEWS	file \| diff \| annotate
4 months ago	blanchet	2012-01-19	renamed "sound" option to "strict"	file \| diff \| annotate
4 months ago	bulwahn	2012-01-17	refreshing NEWS	file \| diff \| annotate
4 months ago	wenzelm	2012-01-16	position constraints for numerals enable PIDE markup;	file \| diff \| annotate
4 months ago	bulwahn	2012-01-10	NEWS	file \| diff \| annotate
4 months ago	wenzelm	2012-01-09	misc tuning and reformatting;	file \| diff \| annotate
4 months ago	haftmann	2012-01-06	consolidated various theorem names relating to Finite_Set.fold and List.fold combinators	file \| diff \| annotate
4 months ago	haftmann	2012-01-06	more explicit NEWS	file \| diff \| annotate
4 months ago	haftmann	2012-01-06	incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r); tuned quotes	file \| diff \| annotate
4 months ago	wenzelm	2012-01-05	discontinued Syntax.positions -- atomic parse trees are always annotated;	file \| diff \| annotate
4 months ago	wenzelm	2012-01-05	improved case syntax: more careful treatment of position constraints, which enables PIDE markup; tuned;	file \| diff \| annotate
4 months ago	haftmann	2011-12-29	attribute code_abbrev superseedes code_unfold_post	file \| diff \| annotate
4 months ago	huffman	2011-12-28	fix typos	file \| diff \| annotate
4 months ago	huffman	2011-12-28	remove some duplicate lemmas	file \| diff \| annotate
4 months ago	haftmann	2011-12-27	be explicit about Finite_Set.fold	file \| diff \| annotate
4 months ago	haftmann	2011-12-26	NEWS: unavoidable fact renames	file \| diff \| annotate
5 months ago	haftmann	2011-12-24	NEWS: `set` is now a proper type constructor	file \| diff \| annotate
5 months ago	huffman	2011-12-23	remove redundant lemma word_sub_def	file \| diff \| annotate
5 months ago	bulwahn	2011-12-21	NEWS	file \| diff \| annotate
5 months ago	bulwahn	2011-12-14	NEWS	file \| diff \| annotate
5 months ago	wenzelm	2011-12-13	'datatype' specifications allow explicit sort constraints; tuned signatures;	file \| diff \| annotate
5 months ago	huffman	2011-12-10	prove class instances without extra lemmas	file \| diff \| annotate
5 months ago	huffman	2011-12-09	remove redundant lemma word_diff_minus	file \| diff \| annotate
5 months ago	noschinl	2011-12-09	more systematic lemma name	file \| diff \| annotate
5 months ago	bulwahn	2011-12-05	NEWS	file \| diff \| annotate
5 months ago	huffman	2011-12-04	remove Library/Diagonalize.thy, because Library/Nat_Bijection.thy includes all the same functionality	file \| diff \| annotate
5 months ago	blanchet	2011-12-01	added "minimize" option for more control over automatic minimization	file \| diff \| annotate
5 months ago	blanchet	2011-12-01	renamed "slicing" to "slice"	file \| diff \| annotate
5 months ago	wenzelm	2011-12-01	renamed inner syntax categories "num" to "num_token" and "xnum" to "xnum_token";	file \| diff \| annotate
6 months ago	wenzelm	2011-11-24	modernized some old-style infix operations, which were left over from the time of ML proof scripts;	file \| diff \| annotate
6 months ago	wenzelm	2011-11-23	modernized some old-style infix operations, which were left over from the time of ML proof scripts;	file \| diff \| annotate
6 months ago	wenzelm	2011-11-21	NEWS;	file \| diff \| annotate
6 months ago	wenzelm	2011-11-20	'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;	file \| diff \| annotate
6 months ago	wenzelm	2011-11-19	NEWS;	file \| diff \| annotate
6 months ago	wenzelm	2011-11-19	added ML antiquotation @{attributes};	file \| diff \| annotate
6 months ago	huffman	2011-11-17	HOL-Word: removed more duplicate theorems	file \| diff \| annotate
6 months ago	huffman	2011-11-17	HOL-Word: removed many duplicate theorems (see NEWS)	file \| diff \| annotate
6 months ago	blanchet	2011-11-16	document "lam_trans" option	file \| diff \| annotate
6 months ago	wenzelm	2011-11-09	sort assignment before simultaneous term_check, not isolated parse_term; prefer Syntax.read_typ over Syntax.parse_typ, to include check phase for sort assignment; simplified Syntax_Phases.decode_sort/decode_typ; discontinued unused Proof_Context.check_tvar;	file \| diff \| annotate
6 months ago	blanchet	2011-11-07	avoid infinite recursion in peephole optimizer function -- this had a debilitating effect on rationals and reals	file \| diff \| annotate
6 months ago	wenzelm	2011-11-07	clarified attribute "mono_set": pure declaration, proper export in ML;	file \| diff \| annotate
6 months ago	wenzelm	2011-11-07	misc tuning;	file \| diff \| annotate
6 months ago	wenzelm	2011-10-29	uniform treatment of syntax declaration wrt. aux. context (NB: notation avoids duplicate mixfix internally);	file \| diff \| annotate
6 months ago	wenzelm	2011-10-28	refined Local_Theory.declaration {syntax = false, pervasive} semantics: update is applied to auxiliary context as well;	file \| diff \| annotate
7 months ago	bulwahn	2011-10-21	NEWS	file \| diff \| annotate
7 months ago	haftmann	2011-10-19	NEWS	file \| diff \| annotate
7 months ago	wenzelm	2011-10-19	inlined @{thms} (ML compile-time) allows to get rid of legacy zadd_ac as well (cf. 49e305100097);	file \| diff \| annotate
7 months ago	bulwahn	2011-10-19	NEWS	file \| diff \| annotate
7 months ago	noschinl	2011-10-17	(old) NEWS	file \| diff \| annotate
7 months ago	haftmann	2011-10-14	NEWS	file \| diff \| annotate
7 months ago	wenzelm	2011-10-13	discontinued obsolete 'types' command;	file \| diff \| annotate
7 months ago	wenzelm	2011-10-12	discontinued obsolete alias structure ProofContext;	file \| diff \| annotate
7 months ago	huffman	2011-10-09	Int.thy: discontinued some legacy theorems	file \| diff \| annotate
8 months ago	wenzelm	2011-09-26	back to post-release mode;	file \| diff \| annotate
8 months ago	wenzelm	2011-09-26	tuned;	file \| diff \| annotate
8 months ago	wenzelm	2011-09-26	misc tuning for release;	file \| diff \| annotate
8 months ago	huffman	2011-09-22	discontinued legacy theorem names from RealDef.thy	file \| diff \| annotate

(0) -1000 -300 -100 -60 tip

isabelle

RSS Atom