isabelle: Changelog

blanchet [Mon, 12 Aug 2013 23:36:43 +0200] rev 52992

fixed "sorry"d proofs

blanchet [Mon, 12 Aug 2013 23:21:06 +0200] rev 52991

repaired proofs (after change to xxx_case_def)

traytel [Mon, 12 Aug 2013 22:38:39 +0200] rev 52990

temporary sorry's for temporarily nonterminating (due to 2b430bbb5a1a) proofs

blanchet [Mon, 12 Aug 2013 21:30:37 +0200] rev 52989

qualify intermediate typedefs

blanchet [Mon, 12 Aug 2013 21:30:36 +0200] rev 52988

avoid double qualification for case constants

blanchet [Mon, 12 Aug 2013 21:30:35 +0200] rev 52987

qualify more generated names with optional type name component

traytel [Mon, 12 Aug 2013 20:04:03 +0200] rev 52986

eliminated bogus assumption from theorem (that was instantiated with refl and resulted in flexflex pairs)

traytel [Mon, 12 Aug 2013 15:36:55 +0200] rev 52985

generalized library function

wenzelm [Mon, 12 Aug 2013 18:03:47 +0200] rev 52984

updated keywords;

wenzelm [Mon, 12 Aug 2013 18:02:01 +0200] rev 52983

merged

isabelle