isabelle: File revisions

src/Pure/Isar/isar_cmd.ML

2006-11-28	wenzelm	2006-11-28	dest_term: strip_imp_concl;	file \| diff \| annotate
2006-11-23	wenzelm	2006-11-23	prefer Proof.context over Context.generic;	file \| diff \| annotate
2006-11-21	wenzelm	2006-11-21	moved theorem kinds from PureThy to Thm;	file \| diff \| annotate
2006-11-14	wenzelm	2006-11-14	incorporated IsarThy into IsarCmd;	file \| diff \| annotate
2006-10-12	wenzelm	2006-10-12	renamed print_lthms to print_facts, do not insist on proof state; renamed Toplevel.enter_forward_proof to Toplevel.enter_proof_body;	file \| diff \| annotate
2006-10-11	wenzelm	2006-10-11	removed 'undo_end', recovered 'cannot_undo';	file \| diff \| annotate
2006-10-11	wenzelm	2006-10-11	undo_end/kill: handle local theory; Toplevel: generic_theory;	file \| diff \| annotate
2006-10-09	wenzelm	2006-10-09	Secure.commit;	file \| diff \| annotate
2006-09-30	wenzelm	2006-09-30	added undo_end;	file \| diff \| annotate
2006-09-19	wenzelm	2006-09-19	'print_theory': bang option for full verbosity;	file \| diff \| annotate
2006-09-18	wenzelm	2006-09-18	added class_deps;	file \| diff \| annotate
2006-04-13	wenzelm	2006-04-13	ProofDisplay.print_theorems/theory;	file \| diff \| annotate
2006-04-09	wenzelm	2006-04-09	print_term etc.: actually observe print mode in final output;	file \| diff \| annotate
2006-03-14	wenzelm	2006-03-14	added print_stmts;	file \| diff \| annotate
2006-02-15	wenzelm	2006-02-15	simplified presentation commands;	file \| diff \| annotate
2006-01-27	wenzelm	2006-01-27	Locale.init;	file \| diff \| annotate
2006-01-10	wenzelm	2006-01-10	print rules: generic context;	file \| diff \| annotate
2006-01-05	wenzelm	2006-01-05	tuned print_theorems_theory;	file \| diff \| annotate
2005-11-09	wenzelm	2005-11-09	Element.context;	file \| diff \| annotate
2005-11-02	wenzelm	2005-11-02	Isar.loop;	file \| diff \| annotate
2005-10-18	wenzelm	2005-10-18	back: Toplevel.actual/skip_proof; use simplified Toplevel.proof etc.;	file \| diff \| annotate
2005-09-13	wenzelm	2005-09-13	Proof.get_thmss;	file \| diff \| annotate
2005-09-05	wenzelm	2005-09-05	add_chapter/section/subsection/subsubsection/text: optional locale specification;	file \| diff \| annotate
2005-09-02	ballarin	2005-09-02	print_locale omits facts by default	file \| diff \| annotate
2005-08-31	wenzelm	2005-08-31	present_text: Toplevel.no_body_context prevents use of wrong context in interaction;	file \| diff \| annotate
2005-08-24	ballarin	2005-08-24	Printing of interpretations: option to show witness theorems;	file \| diff \| annotate
2005-08-16	wenzelm	2005-08-16	back: removed ill-defined '!' option; print_theorems: print facts in proof mode; print_prfs: proper context version -- ProofContext.pretty_proof_of;	file \| diff \| annotate
2005-07-13	wenzelm	2005-07-13	Toplevel.actual_proof;	file \| diff \| annotate
2005-06-20	wenzelm	2005-06-20	print_theorems: proper use of PureThy.print_theorems_diff;	file \| diff \| annotate
2005-06-05	wenzelm	2005-06-05	File.shell_path;	file \| diff \| annotate
2005-06-02	wenzelm	2005-06-02	tuned comment;	file \| diff \| annotate
2005-05-23	wenzelm	2005-05-23	use: not a theory command!	file \| diff \| annotate
2005-05-22	wenzelm	2005-05-22	string FindTheorems.criterion;	file \| diff \| annotate
2005-05-22	wenzelm	2005-05-22	added print_simpset; renamed print_thms_containing to find_theorems; removed print_intros (superceded by find_theorems intro);	file \| diff \| annotate
2005-05-17	wenzelm	2005-05-17	tuned;	file \| diff \| annotate
2005-05-16	kleing	2005-05-16	searching for thms by combination of criteria (intro, elim, dest, name, term pattern)	file \| diff \| annotate
2005-04-21	berghofe	2005-04-21	Adapted use command to new behaviour of Toplevel.node_trans	file \| diff \| annotate
2005-04-13	wenzelm	2005-04-13	* MESSAGE REFERS TO PREVIOUS VERSION * Attrib.src; ISABELLE_DOC_FORMAT;	file \| diff \| annotate
2005-04-13	wenzelm	2005-04-13	* empty log message *	file \| diff \| annotate
2005-03-24	ballarin	2005-03-24	Further work on interpretation commands. New command `interpret' for interpretation in proof contexts.	file \| diff \| annotate
2005-03-09	ballarin	2005-03-09	First version of global registration command.	file \| diff \| annotate
2005-02-13	skalberg	2005-02-13	Deleted Library.option type.	file \| diff \| annotate
2005-01-24	berghofe	2005-01-24	Specific theorems in a named list of theorems can now be referred to via indices (type thmref).	file \| diff \| annotate
2004-10-11	berghofe	2004-10-11	Some changes to allow skipping of proof scripts.	file \| diff \| annotate
2004-10-01	paulson	2004-10-01	display-drafts now uses pdf!	file \| diff \| annotate
2004-09-27	ballarin	2004-09-27	Modified locales: improved implementation of "includes".	file \| diff \| annotate
2004-08-12	ballarin	2004-08-12	Disallowed "includes" in locale declarations.	file \| diff \| annotate
2004-06-21	kleing	2004-06-21	Merged in license change from Isabelle2004	file \| diff \| annotate
2004-06-15	wenzelm	2004-06-15	path instead of string;	file \| diff \| annotate
2004-06-13	wenzelm	2004-06-13	added display_drafts and print_drafts commands;	file \| diff \| annotate
2003-02-03	berghofe	2003-02-03	Moved print_intros from proof_general.ML to Isar/isar_cmd.ML	file \| diff \| annotate
2002-07-02	wenzelm	2002-07-02	thms_containing: optional limit argument;	file \| diff \| annotate
2002-07-02	wenzelm	2002-07-02	ProofContext.print_thms_containing;	file \| diff \| annotate
2002-02-26	wenzelm	2002-02-26	markup commands: proper theory/proof transactions!	file \| diff \| annotate
2002-02-25	wenzelm	2002-02-25	markup commands (from isar_thy.ML) with proper check of antiquotations;	file \| diff \| annotate
2002-02-12	wenzelm	2002-02-12	got rid of explicit marginal comments (now stripped earlier from input);	file \| diff \| annotate
2002-01-15	wenzelm	2002-01-15	print_locale: allow full body specification;	file \| diff \| annotate
2001-12-05	wenzelm	2001-12-05	added print_rules;	file \| diff \| annotate
2001-11-24	wenzelm	2001-11-24	print_locale: expr;	file \| diff \| annotate
2001-11-09	berghofe	2001-11-09	Commands prf and full_prf can now also be used to display proof term of current proof state.	file \| diff \| annotate

isabelle

RSS Atom