Thu, 16 Feb 2012 09:51:34 +0100 simplifying proof
bulwahn [Thu, 16 Feb 2012 09:51:34 +0100] rev 46501
simplifying proof
Thu, 16 Feb 2012 09:18:23 +0100 removing unnecessary premises in theorems of List theory
bulwahn [Thu, 16 Feb 2012 09:18:23 +0100] rev 46500
removing unnecessary premises in theorems of List theory
Thu, 16 Feb 2012 09:18:21 +0100 tuning mutabelle script
bulwahn [Thu, 16 Feb 2012 09:18:21 +0100] rev 46499
tuning mutabelle script
Thu, 16 Feb 2012 09:18:20 +0100 adding documentation for abort_potential option in quickcheck
bulwahn [Thu, 16 Feb 2012 09:18:20 +0100] rev 46498
adding documentation for abort_potential option in quickcheck
Wed, 15 Feb 2012 23:19:30 +0100 renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm [Wed, 15 Feb 2012 23:19:30 +0100] rev 46497
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
Wed, 15 Feb 2012 22:44:31 +0100 discontinued Drule.term_rule, which tends to cause confusion due to builtin cterm_of (NB: the standard morphisms already provide a separate term component);
wenzelm [Wed, 15 Feb 2012 22:44:31 +0100] rev 46496
discontinued Drule.term_rule, which tends to cause confusion due to builtin cterm_of (NB: the standard morphisms already provide a separate term component);
Wed, 15 Feb 2012 21:38:28 +0100 uniform Isar source formatting for this file;
wenzelm [Wed, 15 Feb 2012 21:38:28 +0100] rev 46495
uniform Isar source formatting for this file;
Wed, 15 Feb 2012 21:29:23 +0100 clarified outer syntax "constdecl", which is only local to some rail diagrams;
wenzelm [Wed, 15 Feb 2012 21:29:23 +0100] rev 46494
clarified outer syntax "constdecl", which is only local to some rail diagrams;
Wed, 15 Feb 2012 21:08:27 +0100 discontinued obsolete "prems" fact;
wenzelm [Wed, 15 Feb 2012 21:08:27 +0100] rev 46493
discontinued obsolete "prems" fact;
Wed, 15 Feb 2012 20:56:30 +0100 eliminated slightly odd / obsolete DETERM_UNTIL, DETERM_UNTIL_SOLVED (cf. 941afb897532, ea0668a1c0ba);
wenzelm [Wed, 15 Feb 2012 20:56:30 +0100] rev 46492
eliminated slightly odd / obsolete DETERM_UNTIL, DETERM_UNTIL_SOLVED (cf. 941afb897532, ea0668a1c0ba);
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip