Fri, 16 May 2014 16:40:02 +0200 added lemmas for -1
noschinl [Fri, 16 May 2014 16:40:02 +0200] rev 56979
added lemmas for -1
Fri, 16 May 2014 12:56:39 +0200 proper handling of 'ctor_dtor' for mutual corecursive cases where not all type variables are present in all low-level constructors (cf. 'coind_wit1' etc. in 'Misc_Codatatypes.thy')
blanchet [Fri, 16 May 2014 12:56:39 +0200] rev 56978
proper handling of 'ctor_dtor' for mutual corecursive cases where not all type variables are present in all low-level constructors (cf. 'coind_wit1' etc. in 'Misc_Codatatypes.thy')
Fri, 16 May 2014 09:19:15 +0200 new syntax for card, normalized spacing for #
nipkow [Fri, 16 May 2014 09:19:15 +0200] rev 56977
new syntax for card, normalized spacing for #
Thu, 15 May 2014 16:46:29 +0200 clarified stylized status of sandwich algebra
haftmann [Thu, 15 May 2014 16:46:29 +0200] rev 56976
clarified stylized status of sandwich algebra
Thu, 15 May 2014 16:38:33 +0200 dropped dead code
haftmann [Thu, 15 May 2014 16:38:33 +0200] rev 56975
dropped dead code
Thu, 15 May 2014 16:38:32 +0200 accurate separation of static and dynamic context
haftmann [Thu, 15 May 2014 16:38:32 +0200] rev 56974
accurate separation of static and dynamic context
Thu, 15 May 2014 16:38:31 +0200 syntactic means to prevent accidental mixup of static and dynamic context
haftmann [Thu, 15 May 2014 16:38:31 +0200] rev 56973
syntactic means to prevent accidental mixup of static and dynamic context
Thu, 15 May 2014 16:38:31 +0200 proper separation of static and dynamic context
haftmann [Thu, 15 May 2014 16:38:31 +0200] rev 56972
proper separation of static and dynamic context
Thu, 15 May 2014 16:38:30 +0200 optimization for trivial cases
haftmann [Thu, 15 May 2014 16:38:30 +0200] rev 56971
optimization for trivial cases
Thu, 15 May 2014 16:38:29 +0200 modernized setup
haftmann [Thu, 15 May 2014 16:38:29 +0200] rev 56970
modernized setup
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip