src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
Wed, 10 Jan 2018 15:25:09 +0100 nipkow ran isabelle update_op on all sources
Tue, 19 Dec 2017 13:58:12 +0100 wenzelm isabelle update_cartouches -c -t;
Fri, 18 Aug 2017 20:47:47 +0200 wenzelm session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
Mon, 17 Jul 2017 16:49:19 +0200 eberlm Printing natural numbers as numerals in evaluation
Thu, 08 Dec 2016 15:21:18 +0100 bulwahn filter non-matching prems to not fail in proof procedure; include test case (related to c8a93680b80d)
Thu, 26 May 2016 17:51:22 +0200 wenzelm isabelle update_cartouches -c -t;
Sun, 10 Jan 2016 20:21:30 +0100 Lukas Bulwahn filter non-matching prems rather than fail in proof procedure in rare cases; include derived example motivating change and some similar other ones
Wed, 24 Jun 2015 21:26:03 +0200 wenzelm clarified 'case' command;
Thu, 11 Sep 2014 19:32:36 +0200 blanchet updated news
Tue, 09 Sep 2014 20:51:36 +0200 blanchet use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
Fri, 09 May 2014 08:13:37 +0200 haftmann hardcoded nbe and sml into value command
Thu, 24 Apr 2014 00:23:38 +0200 blanchet avoid name shadowing
Thu, 06 Mar 2014 13:36:48 +0100 blanchet renamed 'map_pair' to 'map_prod'
Fri, 15 Feb 2013 08:31:31 +0100 haftmann less customary term_of conversions;
Fri, 15 Feb 2013 08:31:31 +0100 haftmann two target language numeral types: integer and natural, as replacement for code_numeral;
less more (0) -15 tip