isabelle: File revisions

etc/isar-keywords.el

2013-04-26	blanchet	2013-04-26	updated keywords	file \| diff \| annotate
2013-04-10	wenzelm	2013-04-10	updated keywords;	file \| diff \| annotate
2013-03-30	wenzelm	2013-03-30	added 'print_defn_rules' command; tuned;	file \| diff \| annotate
2013-03-08	wenzelm	2013-03-08	updated keywords (cf. 84d01fd733cf);	file \| diff \| annotate
2013-02-28	wenzelm	2013-02-28	discontinued obsolete 'axioms' command;	file \| diff \| annotate
2013-02-27	wenzelm	2013-02-27	discontinued redundant 'use' command;	file \| diff \| annotate
2013-02-27	wenzelm	2013-02-27	discontinued obsolete 'uses' within theory header;	file \| diff \| annotate
2013-02-25	wenzelm	2013-02-25	reconsider 'export_code' as "thy_decl" command due to its global side-effect on the file-system;	file \| diff \| annotate
2013-02-25	wenzelm	2013-02-25	reconsider 'pretty_setmargin' as "control" command (instead of "diag") -- it is stateful and Proof General legacy;	file \| diff \| annotate
2012-11-30	wenzelm	2012-11-30	added 'print_inductives' command;	file \| diff \| annotate
2012-11-17	wenzelm	2012-11-17	updated keywords;	file \| diff \| annotate
2012-09-28	wenzelm	2012-09-28	updated keywords using proper "isabelle update_keywords";	file \| diff \| annotate
2012-09-28	blanchet	2012-09-28	killed temporary "data_raw" and "codata_raw" now that the examples have been ported to "data" and "codata"	file \| diff \| annotate
2012-09-28	blanchet	2012-09-28	compatibility option to use "rep_datatype"	file \| diff \| annotate
2012-09-26	wenzelm	2012-09-26	updated keywords;	file \| diff \| annotate
2012-09-21	blanchet	2012-09-21	renamed "Codatatype" directory "BNF" (and corresponding session) -- this opens the door to no-nonsense session names like "HOL-BNF-LFP"	file \| diff \| annotate
2012-09-11	wenzelm	2012-09-11	updated keywords;	file \| diff \| annotate
2012-09-04	blanchet	2012-09-04	started work on sugared "(co)data" commands	file \| diff \| annotate
2012-09-03	blanchet	2012-09-03	renamed three BNF/(co)datatype-related commands	file \| diff \| annotate
2012-08-30	blanchet	2012-08-30	more work on BNF sugar -- up to derivation of nchotomy	file \| diff \| annotate
2012-08-30	blanchet	2012-08-30	killed obsolete "bnf_of_typ" command	file \| diff \| annotate
2012-08-28	wenzelm	2012-08-28	more permanent update of keywords (cf. 3517d6f50b12);	file \| diff \| annotate
2012-08-28	blanchet	2012-08-28	updated keywords	file \| diff \| annotate
2012-08-23	wenzelm	2012-08-23	added specific 'spark_open_vcg' and 'spark_open_siv' with formal management of corresponding source files;	file \| diff \| annotate
2012-08-20	wenzelm	2012-08-20	some support for inlining file content into outer syntax token language;	file \| diff \| annotate
2012-08-07	wenzelm	2012-08-07	prefer static Build.outer_syntax in Isabelle/Scala session -- discontinued incremental protocol; just one cumulative Keyword.status at end of batch session;	file \| diff \| annotate
2012-04-04	huffman	2012-04-04	update keywords file	file \| diff \| annotate
2012-04-03	kuncar	2012-04-03	new package Lifting - initial commit	file \| diff \| annotate
2012-04-01	krauss	2012-04-01	merged, manually resolving conflicts due to session renaming (cf. 6488c5efec49)	file \| diff \| annotate
2012-04-01	wenzelm	2012-04-01	more keywords;	file \| diff \| annotate
2012-03-23	kuncar	2012-03-23	update etc/isar-keywords.el	file \| diff \| annotate
2012-03-21	wenzelm	2012-03-21	more explicit Toplevel.open_target/close_target; replaced 'context_includes' by 'context' 'includes'; tuned command descriptions;	file \| diff \| annotate
2012-03-21	wenzelm	2012-03-21	basic support for nested contexts including bundles; include multiple bundles; renamed "affirm" back to "assert" (cf. c4492c6bf450 which was motivated by obsolete Alice/ML); tuned signatures;	file \| diff \| annotate
2012-03-20	wenzelm	2012-03-20	basic support for bundled declarations;	file \| diff \| annotate
2012-03-16	wenzelm	2012-03-16	eliminated odd 'finalconsts' / Theory.add_finals;	file \| diff \| annotate
2012-03-15	wenzelm	2012-03-15	more precise TPTP keywords and dependencies;	file \| diff \| annotate
2012-03-15	wenzelm	2012-03-15	some support for outer syntax keyword declarations within theory header; more uniform Thy_Header.header as argument for begin_theory etc.;	file \| diff \| annotate
2012-02-24	blanchet	2012-02-24	renamed 'try_methods' to 'try0'	file \| diff \| annotate
2012-02-22	bulwahn	2012-02-22	adding new command "find_unused_assms"	file \| diff \| annotate
2011-12-20	bulwahn	2011-12-20	added keywords	file \| diff \| annotate
2011-10-19	wenzelm	2011-10-19	updated keywords;	file \| diff \| annotate
2011-10-13	wenzelm	2011-10-13	discontinued obsolete 'types' command;	file \| diff \| annotate
2011-09-23	berghofe	2011-09-23	Include keywords print_coercions and print_coercion_maps	file \| diff \| annotate
2011-08-16	wenzelm	2011-08-16	include HOL-Library keywords for the sake of recdef;	file \| diff \| annotate
2011-05-27	blanchet	2011-05-27	added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods	file \| diff \| annotate
2011-04-15	berghofe	2011-04-15	Added command for associating user-defined types with SPARK types.	file \| diff \| annotate
2011-01-15	berghofe	2011-01-15	Include HOL-SPARK keywords	file \| diff \| annotate
2011-01-12	wenzelm	2011-01-12	updated keywords;	file \| diff \| annotate
2011-01-06	ballarin	2011-01-06	Diagnostic command to show locale dependencies.	file \| diff \| annotate
2010-12-17	wenzelm	2010-12-17	Command 'type_synonym' (with single argument) supersedes 'types' (legacy feature);	file \| diff \| annotate
2010-12-17	wenzelm	2010-12-17	replaced command 'nonterminals' by slightly modernized version 'nonterminal';	file \| diff \| annotate
2010-12-06	haftmann	2010-12-06	replace `type_mapper` by the more adequate `type_lifting`	file \| diff \| annotate
2010-12-05	wenzelm	2010-12-05	command 'notepad' replaces former 'example_proof';	file \| diff \| annotate
2010-12-04	wenzelm	2010-12-04	formal notepad without any result;	file \| diff \| annotate
2010-11-28	wenzelm	2010-11-28	added 'syntax_declaration' command;	file \| diff \| annotate
2010-11-17	haftmann	2010-11-17	updated keywords	file \| diff \| annotate
2010-11-06	wenzelm	2010-11-06	updated keywords;	file \| diff \| annotate
2010-11-05	wenzelm	2010-11-05	updated keywords;	file \| diff \| annotate
2010-10-27	krauss	2010-10-27	regenerated keyword file	file \| diff \| annotate
2010-10-25	blanchet	2010-10-25	merge	file \| diff \| annotate

isabelle

RSS Atom