isabelle: Changelog

Mercurial Mercurial > repos > isabelle / changelog

Thu, 13 Apr 1995 11:43:01 +0200 Redefined OUnion in a definitional manner

changeset

lcp [Thu, 13 Apr 1995 11:43:01 +0200] rev 1039

Redefined OUnion in a definitional manner

Thu, 13 Apr 1995 11:41:34 +0200 Redefined OUnion in a definitional manner, and proved the

changeset

lcp [Thu, 13 Apr 1995 11:41:34 +0200] rev 1038

Redefined OUnion in a definitional manner, and proved the rules again. Deleted the rules OUnionI/E as they were not needed. Proved OUN_cong. Extended OrdQuant_ss with oex_cong and defined Ord_atomize to extract rewrite rules from ALL x<i... assumptions.

Thu, 13 Apr 1995 11:40:07 +0200 Deleted lt_oadd_disj1

changeset

lcp [Thu, 13 Apr 1995 11:40:07 +0200] rev 1037

Deleted lt_oadd_disj1

Thu, 13 Apr 1995 11:38:48 +0200 Recoded function atomize so that new ways of creating

changeset

lcp [Thu, 13 Apr 1995 11:38:48 +0200] rev 1036

Recoded function atomize so that new ways of creating simplification rules can be added easily.

Thu, 13 Apr 1995 11:37:39 +0200 Proved Int_Diff_eq.

changeset

lcp [Thu, 13 Apr 1995 11:37:39 +0200] rev 1035

Proved Int_Diff_eq.