Wed, 04 Mar 2009 11:49:12 +0100 merged
nipkow [Wed, 04 Mar 2009 11:49:12 +0100] rev 30247
merged
Wed, 04 Mar 2009 11:48:52 +0100 Option.thy
nipkow [Wed, 04 Mar 2009 11:48:52 +0100] rev 30246
Option.thy
Wed, 04 Mar 2009 11:44:05 +0100 consequent rewrite of index_size, size [index] to nat_of; support pseudo-primrec sepcifications with fun
haftmann [Wed, 04 Mar 2009 11:44:05 +0100] rev 30245
consequent rewrite of index_size, size [index] to nat_of; support pseudo-primrec sepcifications with fun
Wed, 04 Mar 2009 11:37:50 +0100 merged
haftmann [Wed, 04 Mar 2009 11:37:50 +0100] rev 30244
merged
Wed, 04 Mar 2009 10:52:47 +0100 explicit error message for `improper` instances lacking explicit instance parameter constants
haftmann [Wed, 04 Mar 2009 10:52:47 +0100] rev 30243
explicit error message for `improper` instances lacking explicit instance parameter constants
Wed, 04 Mar 2009 11:05:29 +0100 Merge.
blanchet [Wed, 04 Mar 2009 11:05:29 +0100] rev 30242
Merge.
Wed, 04 Mar 2009 11:05:02 +0100 Merge.
blanchet [Wed, 04 Mar 2009 11:05:02 +0100] rev 30241
Merge.
Wed, 04 Mar 2009 10:45:52 +0100 Merge.
blanchet [Wed, 04 Mar 2009 10:45:52 +0100] rev 30240
Merge.
Wed, 04 Mar 2009 10:43:39 +0100 Made Refute.norm_rhs public, so I can use it in Nitpick.
blanchet [Wed, 04 Mar 2009 10:43:39 +0100] rev 30239
Made Refute.norm_rhs public, so I can use it in Nitpick.
Sun, 01 Mar 2009 18:40:16 +0100 Added "nitpick_const_def" attribute, for overriding the definition axiom of a constant.
blanchet [Sun, 01 Mar 2009 18:40:16 +0100] rev 30238
Added "nitpick_const_def" attribute, for overriding the definition axiom of a constant.
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip