noschinl [Fri, 16 May 2014 16:40:02 +0200] rev 56979
added lemmas for -1
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')
nipkow [Fri, 16 May 2014 09:19:15 +0200] rev 56977
new syntax for card, normalized spacing for #
haftmann [Thu, 15 May 2014 16:46:29 +0200] rev 56976
clarified stylized status of sandwich algebra
haftmann [Thu, 15 May 2014 16:38:33 +0200] rev 56975
dropped dead code
haftmann [Thu, 15 May 2014 16:38:32 +0200] rev 56974
accurate separation 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
haftmann [Thu, 15 May 2014 16:38:31 +0200] rev 56972
proper separation of static and dynamic context
haftmann [Thu, 15 May 2014 16:38:30 +0200] rev 56971
optimization for trivial cases
haftmann [Thu, 15 May 2014 16:38:29 +0200] rev 56970
modernized setup
haftmann [Thu, 15 May 2014 16:38:29 +0200] rev 56969
dropped obsolete hand-waving adjustion of type variables: safely done in preprocessor
haftmann [Thu, 15 May 2014 16:38:28 +0200] rev 56968
unified approach toward conversions and simple term rewriting in preprocessor by means of sandwiches
haftmann [Thu, 15 May 2014 16:38:17 +0200] rev 56967
normalize type variables of evaluation term by conversion
blanchet [Thu, 15 May 2014 20:48:14 +0200] rev 56966
more aggressive nested size handling in the absence of 'size_o_map' theorems (+ unrelated pattern matching fix)
blanchet [Thu, 15 May 2014 20:48:13 +0200] rev 56965
new approach to silence proof methods, to avoid weird theory/context mismatches
haftmann [Thu, 15 May 2014 18:18:50 +0200] rev 56964
type