wenzelm [Thu, 19 Aug 2010 18:19:21 +0200] rev 38560
added generated file;
wenzelm [Thu, 19 Aug 2010 17:41:52 +0200] rev 38559
merged
haftmann [Thu, 19 Aug 2010 16:08:59 +0200] rev 38558
tuned quotes
haftmann [Thu, 19 Aug 2010 16:08:54 +0200] rev 38557
more antiquotations
haftmann [Thu, 19 Aug 2010 16:08:53 +0200] rev 38556
deglobalized named HOL constants
haftmann [Thu, 19 Aug 2010 16:03:07 +0200] rev 38555
deglobalized named HOL constants
haftmann [Thu, 19 Aug 2010 16:03:01 +0200] rev 38554
corrected some long-overseen misperceptions in recdef
haftmann [Thu, 19 Aug 2010 12:11:57 +0200] rev 38553
use HOLogic.boolT and @{typ bool} more pervasively
haftmann [Thu, 19 Aug 2010 11:19:24 +0200] rev 38552
tuned
haftmann [Thu, 19 Aug 2010 11:19:24 +0200] rev 38551
some more antiquotations
haftmann [Thu, 19 Aug 2010 11:13:07 +0200] rev 38550
tuned
haftmann [Thu, 19 Aug 2010 11:02:14 +0200] rev 38549
use antiquotations for remaining unqualified constants in HOL
haftmann [Thu, 19 Aug 2010 10:27:12 +0200] rev 38548
tuned
haftmann [Thu, 19 Aug 2010 10:27:02 +0200] rev 38547
tuned declaration order
haftmann [Wed, 18 Aug 2010 17:03:09 +0200] rev 38546
merged
haftmann [Wed, 18 Aug 2010 17:01:12 +0200] rev 38545
NEWS
haftmann [Wed, 18 Aug 2010 16:59:37 +0200] rev 38544
re-added instantiation of type class random for records
haftmann [Wed, 18 Aug 2010 16:59:37 +0200] rev 38543
tuned signature and code
haftmann [Wed, 18 Aug 2010 16:59:36 +0200] rev 38542
adjusted to restored naming convention of logical record types
haftmann [Wed, 18 Aug 2010 16:59:36 +0200] rev 38541
robustified proof
haftmann [Wed, 18 Aug 2010 16:59:36 +0200] rev 38540
adjusted to changed naming convention of logical record types
haftmann [Wed, 18 Aug 2010 16:59:35 +0200] rev 38539
removed separate quickcheck_record module
haftmann [Wed, 18 Aug 2010 15:01:57 +0200] rev 38538
liberal instantiation of class eq; tuned naming scheme
haftmann [Wed, 18 Aug 2010 15:01:57 +0200] rev 38537
more helpful NEWS entry
haftmann [Tue, 17 Aug 2010 16:44:24 +0200] rev 38536
dropped SML typedef_codegen: does not fit to code equations for record operations any longer
haftmann [Tue, 17 Aug 2010 16:44:21 +0200] rev 38535
preemptive NEWS
haftmann [Tue, 17 Aug 2010 16:35:23 +0200] rev 38534
tuned code
haftmann [Tue, 17 Aug 2010 16:27:58 +0200] rev 38533
use extension constant as formal constructor of logical record type
haftmann [Tue, 17 Aug 2010 16:27:58 +0200] rev 38532
deleted typecopy package
haftmann [Tue, 17 Aug 2010 15:29:41 +0200] rev 38531
authentic syntax allows simplification of type names
haftmann [Tue, 17 Aug 2010 15:19:37 +0200] rev 38530
dropped make_/dest_ naming convention
haftmann [Tue, 17 Aug 2010 15:17:44 +0200] rev 38529
formally integrated typecopy layer into record package
haftmann [Tue, 17 Aug 2010 15:13:16 +0200] rev 38528
eliminated typecopy interpretation
haftmann [Wed, 18 Aug 2010 14:55:10 +0200] rev 38527
moved spurious auxiliary lemma here
haftmann [Wed, 18 Aug 2010 14:55:10 +0200] rev 38526
tuned proof
haftmann [Wed, 18 Aug 2010 14:55:09 +0200] rev 38525
qualified constants Let and If
haftmann [Wed, 18 Aug 2010 14:55:09 +0200] rev 38524
NEWS
haftmann [Wed, 18 Aug 2010 12:27:39 +0200] rev 38523
merged
haftmann [Wed, 18 Aug 2010 12:26:48 +0200] rev 38522
deglobalization
blanchet [Wed, 18 Aug 2010 12:26:15 +0200] rev 38521
merged
blanchet [Wed, 18 Aug 2010 12:05:44 +0200] rev 38520
merged
blanchet [Wed, 18 Aug 2010 12:04:00 +0200] rev 38519
rename enum values
blanchet [Wed, 18 Aug 2010 12:03:44 +0200] rev 38518
handle bound name conflicts gracefully in FOF translation
blanchet [Wed, 18 Aug 2010 11:14:33 +0200] rev 38517
with Kodkodi 1.2.15, Java 1.5 is fine
blanchet [Wed, 18 Aug 2010 10:42:04 +0200] rev 38516
gracefully handle the case where the JVM is too old in Nitpick
blanchet [Wed, 18 Aug 2010 09:38:50 +0200] rev 38515
improve SPASS clause numbering hack
haftmann [Wed, 18 Aug 2010 12:19:27 +0200] rev 38514
deglobalization
haftmann [Wed, 18 Aug 2010 12:08:21 +0200] rev 38513
more antiquotations