isabelle: Changelog

pass auto-proved exhaustiveness properties to tactic; rightly use "%_. False" instead of undefined for unspecified conditions; get rid of ugly "if True then ... else Code.abort" in auto-generated code equations;

Wed, 18 Dec 2013 17:27:17 +0100 merge

changeset

blanchet [Wed, 18 Dec 2013 17:27:17 +0100] rev 54805

merge

Wed, 18 Dec 2013 17:26:31 +0100 changed pirate port

changeset

blanchet [Wed, 18 Dec 2013 17:26:31 +0100] rev 54804

changed pirate port

Wed, 18 Dec 2013 17:00:14 +0100 fixed variable confusion introduced by 'tuning' change 565f9af86d67

changeset

blanchet [Wed, 18 Dec 2013 17:00:14 +0100] rev 54803

fixed variable confusion introduced by 'tuning' change 565f9af86d67

Wed, 18 Dec 2013 16:50:14 +0100 made SML/NJ happier

changeset

blanchet [Wed, 18 Dec 2013 16:50:14 +0100] rev 54802

made SML/NJ happier

Wed, 18 Dec 2013 16:50:14 +0100 try 'auto' first -- more likely to succeed

changeset

blanchet [Wed, 18 Dec 2013 16:50:14 +0100] rev 54801

try 'auto' first -- more likely to succeed

Wed, 18 Dec 2013 16:50:14 +0100 new port

changeset

blanchet [Wed, 18 Dec 2013 16:50:14 +0100] rev 54800

new port

Wed, 18 Dec 2013 16:50:14 +0100 tuning

changeset

blanchet [Wed, 18 Dec 2013 16:50:14 +0100] rev 54799

tuning

Wed, 18 Dec 2013 16:50:14 +0100 generate type classes for tfrees

changeset

blanchet [Wed, 18 Dec 2013 16:50:14 +0100] rev 54798

generate type classes for tfrees

Wed, 18 Dec 2013 11:53:40 +0100 modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property

changeset

hoelzl [Wed, 18 Dec 2013 11:53:40 +0100] rev 54797

modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property

Tue, 17 Dec 2013 22:34:26 +0100 avoid clashes of fact names

changeset

haftmann [Tue, 17 Dec 2013 22:34:26 +0100] rev 54796

avoid clashes of fact names

Tue, 17 Dec 2013 20:21:22 +0100 initalize locale with idents from background theory rather than empty idents: must treat idents and registrations synchronously to provide consistent setup for interpretation in locale contexts

changeset

haftmann [Tue, 17 Dec 2013 20:21:22 +0100] rev 54795

initalize locale with idents from background theory rather than empty idents: must treat idents and registrations synchronously to provide consistent setup for interpretation in locale contexts

Tue, 17 Dec 2013 15:56:57 +0100 reduced cardinals dependencies of (co)datatypes

changeset

traytel [Tue, 17 Dec 2013 15:56:57 +0100] rev 54794

reduced cardinals dependencies of (co)datatypes

Tue, 17 Dec 2013 15:44:10 +0100 tighter bnf bounds for (co)datatypes

changeset

traytel [Tue, 17 Dec 2013 15:44:10 +0100] rev 54793

tighter bnf bounds for (co)datatypes

Tue, 17 Dec 2013 15:15:59 +0100 tuned

changeset

traytel [Tue, 17 Dec 2013 15:15:59 +0100] rev 54792

tuned