src/HOL/MicroJava/Comp/CorrComp.thy
Tue, 14 Mar 2023 18:19:10 +0100 nipkow Adjusted to new map update priorities
Thu, 15 Feb 2018 12:11:00 +0100 wenzelm more symbols;
Fri, 21 Apr 2017 16:48:58 +0200 wenzelm tuned imports;
Thu, 28 May 2015 17:25:57 +1000 kleing modernized (slightly) type compiler in MicroJava
Mon, 29 Dec 2014 21:02:49 +0100 wenzelm tuned;
Tue, 09 Sep 2014 20:51:36 +0200 blanchet ported MicroJava to new datatypes
Fri, 04 Jul 2014 20:18:47 +0200 haftmann reduced name variants for assoc and commute on plus and mult
Thu, 13 Mar 2014 07:07:07 +0100 nipkow enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions
Tue, 13 Aug 2013 22:37:58 +0200 wenzelm more symbolic notation;
Mon, 05 Aug 2013 17:52:07 +0200 wenzelm tuned proofs;
Sun, 15 Jan 2012 18:55:27 +0100 wenzelm tuned proofs;
Mon, 01 Mar 2010 13:40:23 +0100 haftmann replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
Thu, 12 Nov 2009 17:21:48 +0100 hoelzl New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Tue, 07 Oct 2008 16:07:50 +0200 haftmann arbitrary is undefined
less more (0) -15 tip