Mon, 15 Sep 2014 16:11:01 +0200 blanchet 'code' is needed for extraction datatype
Mon, 15 Sep 2014 14:31:32 +0200 blanchet tuning
Mon, 15 Sep 2014 12:30:06 +0200 blanchet removed accidental '@{print}'
Mon, 15 Sep 2014 12:11:41 +0200 blanchet tuning
Mon, 15 Sep 2014 11:54:47 +0200 blanchet more hints on how to port 'size'
Mon, 15 Sep 2014 11:37:55 +0200 blanchet tuned definition of 'size' function to get nicer properties
Mon, 15 Sep 2014 11:17:44 +0200 blanchet tuning
Mon, 15 Sep 2014 11:10:09 +0200 blanchet document size difference
Mon, 15 Sep 2014 10:49:07 +0200 blanchet generate 'code' attribute only if 'code' plugin is enabled
Sun, 14 Sep 2014 22:59:30 +0200 blanchet disable datatype 'plugins' for internal types
Sat, 13 Sep 2014 18:08:45 +0200 blanchet ported Imperative HOL to new datatypes
Sat, 13 Sep 2014 18:08:38 +0200 blanchet imported patch phantoms
Fri, 12 Sep 2014 17:51:31 +0200 blanchet enabled 'Sudoku' only with 'ISABELLE_FULL_TEST' -- Sudoku is fast enough on modern hardware (within seconds on my MacBook), but it seems to fail on older test machines
Fri, 12 Sep 2014 17:30:05 +0200 blanchet new datatype is too slow on the huge datatypes (at least the mutual ones) -- use 'old_datatype' instead
Fri, 12 Sep 2014 16:42:36 +0200 blanchet run larger nominal examples only 'ISABELLE_FULL_TEST'
Fri, 12 Sep 2014 13:50:55 +0200 desharna refactor repeated terms in a single variable
Fri, 12 Sep 2014 13:50:51 +0200 desharna make 'ctr_transfer' tactic more robust
Fri, 12 Sep 2014 13:48:15 +0200 desharna make 'rel_sel' and 'map_sel' tactics more robust
Fri, 12 Sep 2014 13:27:33 +0200 fleury Changing the way the dependencies are managed.
Fri, 12 Sep 2014 13:27:32 +0200 fleury correction in the thf0 parser ("(=)" found in a Satallax proof).
Fri, 12 Sep 2014 11:17:06 +0200 blanchet merge
Fri, 12 Sep 2014 11:16:47 +0200 blanchet fixed spellings
Fri, 12 Sep 2014 07:38:15 +0200 haftmann NEWS
Thu, 11 Sep 2014 23:12:32 +0200 haftmann abstract product over monoid for lists
Thu, 11 Sep 2014 18:33:56 +0200 haftmann use proto_base_sort uniformly
Thu, 11 Sep 2014 21:11:03 +0200 blanchet fixed some spelling mistakes
Thu, 11 Sep 2014 20:01:29 +0200 blanchet tuned comment
Thu, 11 Sep 2014 19:59:46 +0200 blanchet more porting to new datatypes
Thu, 11 Sep 2014 19:45:42 +0200 blanchet tuning terminology
Thu, 11 Sep 2014 19:41:45 +0200 blanchet compile
Thu, 11 Sep 2014 19:39:48 +0200 blanchet renamed example theory for consistency
Thu, 11 Sep 2014 19:38:22 +0200 blanchet updated ROOT
Thu, 11 Sep 2014 19:35:38 +0200 blanchet tuned documentation
Thu, 11 Sep 2014 19:32:36 +0200 blanchet updated news
Thu, 11 Sep 2014 19:26:59 +0200 blanchet renamed 'BNF_Examples' to 'Datatype_Examples' (cf. 'datatypes.pdf')
Thu, 11 Sep 2014 19:20:23 +0200 blanchet move datatype benchmarks
Thu, 11 Sep 2014 19:18:23 +0200 blanchet use new datatypes for benchmarks
Thu, 11 Sep 2014 18:54:36 +0200 blanchet renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
Thu, 11 Sep 2014 18:54:36 +0200 blanchet renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
Thu, 11 Sep 2014 18:54:36 +0200 blanchet tuning
Thu, 11 Sep 2014 18:54:36 +0200 blanchet fixed situation in 'primrec' when recursive calls are apparently nested, e.g. 'f (f x y) y', with the recursion in 'y'
Thu, 11 Sep 2014 18:54:36 +0200 blanchet tuning
Thu, 11 Sep 2014 18:54:36 +0200 blanchet fixed situation in 'primrec' whereby the original value of a constructor argument of nested type was not translated correctly to a 'map fst'
Thu, 11 Sep 2014 18:54:36 +0200 blanchet speed up old Nominal by killing type variables
Thu, 11 Sep 2014 18:54:36 +0200 blanchet took out some datatype tests for Refute -- these yield timeouts on some Isatests after transition to new datatypes, for some reason (and Refute is obsolete anyway)
Thu, 11 Sep 2014 18:54:36 +0200 blanchet more docs
Thu, 11 Sep 2014 15:08:56 +0200 traytel new deads go to the end
Thu, 11 Sep 2014 11:49:47 +0200 blanchet comment
Wed, 10 Sep 2014 22:52:46 +0200 haftmann more material on lists
Wed, 10 Sep 2014 14:58:02 +0200 haftmann explicit check phase to guide type inference of class expression towards one single type variable
Wed, 10 Sep 2014 14:58:01 +0200 haftmann tuned
Wed, 10 Sep 2014 14:57:03 +0200 haftmann dropped ineffective print_translation which has never been adjusted to check/uncheck-style case patterns
Tue, 09 Sep 2014 23:54:47 +0200 blanchet tuning
Tue, 09 Sep 2014 23:54:39 +0200 blanchet proper checks -- the calls data structure may contain spurious entries
Tue, 09 Sep 2014 22:33:43 +0200 blanchet avoid exception
Tue, 09 Sep 2014 22:28:49 +0200 blanchet avoid internal fact
Tue, 09 Sep 2014 22:25:14 +0200 blanchet restored old case names
Tue, 09 Sep 2014 20:51:36 +0200 blanchet compile
Tue, 09 Sep 2014 20:51:36 +0200 blanchet avoid duplicate case names
Tue, 09 Sep 2014 20:51:36 +0200 blanchet nicer case names in the N2M case, similar to those generated by the old package (e.g. 'Cons_tree' instead of just 'Cons')
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip