isabelle: File revisions

src/HOL/MicroJava/J/JTypeSafe.thy

2015-10-13	haftmann	2015-10-13	prod_case as canonical name for product type eliminator	file \| diff \| annotate
2015-10-07	wenzelm	2015-10-07	isabelle update_cartouches;	file \| diff \| annotate
2015-07-18	wenzelm	2015-07-18	prefer tactics with explicit context;	file \| diff \| annotate
2015-03-27	wenzelm	2015-03-27	tuned signature;	file \| diff \| annotate
2015-03-25	wenzelm	2015-03-25	prefer local fixes;	file \| diff \| annotate
2015-03-24	wenzelm	2015-03-24	clarified case_tac fixes and context;	file \| diff \| annotate
2015-02-10	wenzelm	2015-02-10	proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;	file \| diff \| annotate
2014-11-10	wenzelm	2014-11-10	proper context for assume_tac (atac remains as fall-back without context);	file \| diff \| annotate
2014-11-02	wenzelm	2014-11-02	modernized header;	file \| diff \| annotate
2014-11-01	wenzelm	2014-11-01	eliminated spurious semicolons;	file \| diff \| annotate
2014-09-09	blanchet	2014-09-09	ported MicroJava to new datatypes	file \| diff \| annotate
2014-06-11	Thomas Sewell	2014-06-11	Hypsubst preserves equality hypotheses Fixes included for various theories affected by this change.	file \| diff \| annotate
2013-12-14	wenzelm	2013-12-14	proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;	file \| diff \| annotate
2013-04-27	wenzelm	2013-04-27	uniform Proof.context for hyp_subst_tac;	file \| diff \| annotate
2013-04-18	wenzelm	2013-04-18	simplifier uses proper Proof.context instead of historic type simpset;	file \| diff \| annotate
2013-04-10	wenzelm	2013-04-10	added ML antiquotation @{theory_context};	file \| diff \| annotate
2013-02-28	wenzelm	2013-02-28	marginalized historic strip_tac;	file \| diff \| annotate
2011-10-12	wenzelm	2011-10-12	modernized structure Induct_Tacs;	file \| diff \| annotate
2011-01-16	wenzelm	2011-01-16	tuned headers;	file \| diff \| annotate
2010-09-06	wenzelm	2010-09-06	more antiquotations;	file \| diff \| annotate
2009-11-24	haftmann	2009-11-24	backported parts of abstract byte code verifier from AFP/Jinja	file \| diff \| annotate
2009-08-13	paulson	2009-08-13	Removal of redundant settings of unification trace and search bounds.	file \| diff \| annotate
2009-07-23	wenzelm	2009-07-23	renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;	file \| diff \| annotate
2008-06-14	wenzelm	2008-06-14	simplified InductTacs.case_tac/induct_tac;	file \| diff \| annotate
2008-06-10	wenzelm	2008-06-10	tuned proofs;	file \| diff \| annotate
2008-06-09	wenzelm	2008-06-09	DatatypePackage.case_tac;	file \| diff \| annotate
2007-08-07	wenzelm	2007-08-07	turned Unify flags into configuration options (global only);	file \| diff \| annotate
2007-07-21	wenzelm	2007-07-21	tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);	file \| diff \| annotate
2007-07-11	berghofe	2007-07-11	- Renamed inductive2 to inductive - Renamed some theorems about transitive closure for predicates	file \| diff \| annotate
2007-02-07	berghofe	2007-02-07	Adapted to new inductive definition package.	file \| diff \| annotate
2005-06-17	haftmann	2005-06-17	migrated theory headers to new format	file \| diff \| annotate
2003-08-08	streckem	2003-08-08	Changed lemmas .._type_sound	file \| diff \| annotate
2003-05-26	streckem	2003-05-26	Introduced distinction wf_prog vs. ws_prog	file \| diff \| annotate
2003-05-14	nipkow	2003-05-14	* empty log message *	file \| diff \| annotate
2002-10-23	streckem	2002-10-23	Added compiler	file \| diff \| annotate
2002-02-26	kleing	2002-02-26	introduces SystemClasses and BVExample	file \| diff \| annotate
2002-02-21	kleing	2002-02-21	new document	file \| diff \| annotate
2002-02-14	nipkow	2002-02-14	nodups -> distinct	file \| diff \| annotate
2001-12-16	kleing	2001-12-16	exception merge, cleanup, tuned	file \| diff \| annotate
2001-10-01	streckem	2001-10-01	Removed some unfoldings of defs after declaring wf_java_prog as syntax	file \| diff \| annotate
2001-02-05	oheimb	2001-02-05	improved document (added headers etc)	file \| diff \| annotate
2001-02-01	oheimb	2001-02-01	converted to Isar, simplifying recursion on class hierarchy	file \| diff \| annotate
1999-11-11	nipkow	1999-11-11	* empty log message *	file \| diff \| annotate

isabelle

RSS Atom