src/HOL/TLA/Memory/MemoryImplementation.thy
2011-10-12 ago modernized structure Induct_Tacs;
2011-06-29 ago simplified/unified Simplifier.mk_solver;
2011-05-15 ago simplified/unified method_setup/attribute_setup;
2011-05-13 ago proper method_setup "split_idle";
2011-05-12 ago modernized dead code;
2011-05-12 ago eliminated old-style MI_fast_css -- replaced by fast_solver with config option;
2011-05-12 ago eliminated obsolete MI_css -- use current context directly;
2011-03-20 ago modernized specifications;
2011-01-16 ago tuned headers;
2010-09-06 ago more antiquotations;
2010-05-12 ago modernized specifications;
2009-07-23 ago renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
2008-06-14 ago proper context for tactics derived from res_inst_tac;
2008-06-10 ago case_split_tac (works without context);
2008-06-09 ago DatatypePackage.case_tac;
2008-03-19 ago more antiquotations;
2007-08-07 ago tuned ML setup;
2006-12-02 ago TLA: converted legacy ML scripts;
2005-09-07 ago converted to Isar theory format;
2001-10-05 ago tuned;
2000-08-03 ago tuned version by Stephan Merz (unbatchified etc.);
1999-02-08 ago updated (Stephan Merz);
1997-10-08 ago A formalization of TLA in HOL -- by Stephan Merz;