src/HOL/MicroJava/BV/Correct.thy
Fri, 20 Sep 2024 19:51:08 +0200 wenzelm standardize mixfix annotations via "isabelle update -a -u mixfix_cartouches" --- to simplify systematic editing;
Wed, 07 Oct 2015 23:28:49 +0200 wenzelm isabelle update_cartouches;
Thu, 23 Jul 2015 22:13:42 +0200 wenzelm more symbols by default, without xsymbols mode;
Mon, 29 Dec 2014 21:02:49 +0100 wenzelm tuned;
Sun, 02 Nov 2014 17:58:35 +0100 wenzelm modernized header;
Sat, 01 Nov 2014 14:20:38 +0100 wenzelm eliminated spurious semicolons;
Sun, 16 Feb 2014 21:33:28 +0100 blanchet folded 'list_all2' with the relator generated by 'datatype_new'
Tue, 13 Aug 2013 11:13:26 +0200 wenzelm tuned proofs;
Mon, 12 Sep 2011 07:55:43 +0200 nipkow new fastforce replacing fastsimp - less confusing name
Mon, 01 Mar 2010 13:42:31 +0100 haftmann merged
Mon, 01 Mar 2010 13:40:23 +0100 haftmann replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
Wed, 24 Feb 2010 22:09:50 +0100 wenzelm modernized syntax declarations, and make them actually work with authentic syntax;
Tue, 24 Nov 2009 14:37:23 +0100 haftmann backported parts of abstract byte code verifier from AFP/Jinja
Thu, 27 Mar 2008 17:21:41 +0100 wenzelm fixed theory imports;
Wed, 07 Feb 2007 17:44:07 +0100 berghofe Adapted to new inductive definition package.
less more (0) -15 tip