Fri, 19 Sep 2014 13:27:04 +0200 tuning
blanchet [Fri, 19 Sep 2014 13:27:04 +0200] rev 58387
tuning
Fri, 19 Sep 2014 10:40:56 +0200 typo
traytel [Fri, 19 Sep 2014 10:40:56 +0200] rev 58386
typo
Fri, 19 Sep 2014 10:00:34 +0200 regression tests for n2m
traytel [Fri, 19 Sep 2014 10:00:34 +0200] rev 58385
regression tests for n2m
Fri, 19 Sep 2014 08:26:03 +0200 merged
Andreas Lochbihler [Fri, 19 Sep 2014 08:26:03 +0200] rev 58384
merged
Thu, 18 Sep 2014 15:23:23 +0200 add lemma
Andreas Lochbihler [Thu, 18 Sep 2014 15:23:23 +0200] rev 58383
add lemma
Thu, 18 Sep 2014 19:01:50 +0200 tuned imports
blanchet [Thu, 18 Sep 2014 19:01:50 +0200] rev 58382
tuned imports
Thu, 18 Sep 2014 18:49:58 +0200 removed debugging junk
blanchet [Thu, 18 Sep 2014 18:49:58 +0200] rev 58381
removed debugging junk
Thu, 18 Sep 2014 17:54:56 +0200 help AFP entry 'Free-Groups' to compile
blanchet [Thu, 18 Sep 2014 17:54:56 +0200] rev 58380
help AFP entry 'Free-Groups' to compile
Thu, 18 Sep 2014 16:57:10 +0200 reintroduced an instantiation of 'size' for 'numerals'
blanchet [Thu, 18 Sep 2014 16:57:10 +0200] rev 58379
reintroduced an instantiation of 'size' for 'numerals'
Thu, 18 Sep 2014 16:47:40 +0200 use selector
blanchet [Thu, 18 Sep 2014 16:47:40 +0200] rev 58378
use selector
Thu, 18 Sep 2014 16:47:40 +0200 moved old 'size' generator together with 'old_datatype'
blanchet [Thu, 18 Sep 2014 16:47:40 +0200] rev 58377
moved old 'size' generator together with 'old_datatype'
Thu, 18 Sep 2014 16:47:40 +0200 moved datatype realizer to 'old_datatype' and colleagues
blanchet [Thu, 18 Sep 2014 16:47:40 +0200] rev 58376
moved datatype realizer to 'old_datatype' and colleagues
Thu, 18 Sep 2014 16:47:40 +0200 careful with op = in n2m (actually by Dmitriy Traytel)
blanchet [Thu, 18 Sep 2014 16:47:40 +0200] rev 58375
careful with op = in n2m (actually by Dmitriy Traytel)
Thu, 18 Sep 2014 16:47:40 +0200 fixed attribute name in docs (thanks to Andreas Lochbihler)
blanchet [Thu, 18 Sep 2014 16:47:40 +0200] rev 58374
fixed attribute name in docs (thanks to Andreas Lochbihler)
Thu, 18 Sep 2014 16:47:40 +0200 updated NEWS
blanchet [Thu, 18 Sep 2014 16:47:40 +0200] rev 58373
updated NEWS
Thu, 18 Sep 2014 16:47:40 +0200 moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer)
blanchet [Thu, 18 Sep 2014 16:47:40 +0200] rev 58372
moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer) * * * made example compile again
Thu, 18 Sep 2014 16:47:40 +0200 increased 'HOL-Proofs' timeout
blanchet [Thu, 18 Sep 2014 16:47:40 +0200] rev 58371
increased 'HOL-Proofs' timeout
Thu, 18 Sep 2014 16:47:40 +0200 made 'mk_pointfree' work again in local theories
blanchet [Thu, 18 Sep 2014 16:47:40 +0200] rev 58370
made 'mk_pointfree' work again in local theories
Thu, 18 Sep 2014 16:47:40 +0200 fixed authorship
blanchet [Thu, 18 Sep 2014 16:47:40 +0200] rev 58369
fixed authorship
Thu, 18 Sep 2014 15:07:43 +0200 product over monoids for lists
haftmann [Thu, 18 Sep 2014 15:07:43 +0200] rev 58368
product over monoids for lists
Thu, 18 Sep 2014 00:03:46 +0200 renamed SMT certificate files, following 'SMT2' -> 'SMT' renaming
blanchet [Thu, 18 Sep 2014 00:03:46 +0200] rev 58367
renamed SMT certificate files, following 'SMT2' -> 'SMT' renaming
Thu, 18 Sep 2014 00:02:45 +0200 more meaningful record tests
blanchet [Thu, 18 Sep 2014 00:02:45 +0200] rev 58366
more meaningful record tests
Thu, 18 Sep 2014 00:01:27 +0200 updated SMT certificates
blanchet [Thu, 18 Sep 2014 00:01:27 +0200] rev 58365
updated SMT certificates
Wed, 17 Sep 2014 23:45:57 +0200 tuning
blanchet [Wed, 17 Sep 2014 23:45:57 +0200] rev 58364
tuning
Wed, 17 Sep 2014 23:45:28 +0200 take out selectors for records -- for derived records, these don't quite have the right type
blanchet [Wed, 17 Sep 2014 23:45:28 +0200] rev 58363
take out selectors for records -- for derived records, these don't quite have the right type
Wed, 17 Sep 2014 21:35:58 +0200 register Isabelle selectors as SMT selectors when possible
blanchet [Wed, 17 Sep 2014 21:35:58 +0200] rev 58362
register Isabelle selectors as SMT selectors when possible
Wed, 17 Sep 2014 17:32:27 +0200 added codatatype support for CVC4
blanchet [Wed, 17 Sep 2014 17:32:27 +0200] rev 58361
added codatatype support for CVC4
Wed, 17 Sep 2014 16:53:39 +0200 added interface for CVC4 extensions
blanchet [Wed, 17 Sep 2014 16:53:39 +0200] rev 58360
added interface for CVC4 extensions
Wed, 17 Sep 2014 16:20:13 +0200 avoid 'subst_tac' when possible (it is suspected of not helping 'HOL-Proofs')
blanchet [Wed, 17 Sep 2014 16:20:13 +0200] rev 58359
avoid 'subst_tac' when possible (it is suspected of not helping 'HOL-Proofs')
Wed, 17 Sep 2014 12:09:33 +0200 tweaked compatibility layer
blanchet [Wed, 17 Sep 2014 12:09:33 +0200] rev 58358
tweaked compatibility layer
(0) -30000 -10000 -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 tip