Mercurial Mercurial > repos > isabelle / changelog
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 +30000 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Mon, 20 Sep 1999 12:01:41 +0200 Fixed bug in add_primrec which caused non-informative error message.
changeset
berghofe [Mon, 20 Sep 1999 12:01:41 +0200] rev 7544
Fixed bug in add_primrec which caused non-informative error message.
Mon, 20 Sep 1999 10:46:16 +0200 renamed Always_Int to Always_Int_I
changeset
paulson [Mon, 20 Sep 1999 10:46:16 +0200] rev 7543
renamed Always_Int to Always_Int_I
Mon, 20 Sep 1999 10:45:30 +0200 new theorem mono_Follows_apply
changeset
paulson [Mon, 20 Sep 1999 10:45:30 +0200] rev 7542
new theorem mono_Follows_apply
Mon, 20 Sep 1999 10:42:09 +0200 new theorem Always_INT_distrib; therefore renamed Always_Int
changeset
paulson [Mon, 20 Sep 1999 10:42:09 +0200] rev 7541
new theorem Always_INT_distrib; therefore renamed Always_Int to Always_Int_I
Mon, 20 Sep 1999 10:40:40 +0200 working Safety proof for the system at last
changeset
paulson [Mon, 20 Sep 1999 10:40:40 +0200] rev 7540
working Safety proof for the system at last
Mon, 20 Sep 1999 10:40:08 +0200 now uses Pattern.aeconv, not aconv, to test equality between the terms
changeset
paulson [Mon, 20 Sep 1999 10:40:08 +0200] rev 7539
now uses Pattern.aeconv, not aconv, to test equality between the terms abstracted over; otherwise it is incomplete. Other changes are cosmetic
Fri, 17 Sep 1999 10:31:38 +0200 new rule PLam_ensures
changeset
paulson [Fri, 17 Sep 1999 10:31:38 +0200] rev 7538
new rule PLam_ensures
Fri, 10 Sep 1999 18:40:06 +0200 working snapshot
changeset
paulson [Fri, 10 Sep 1999 18:40:06 +0200] rev 7537
working snapshot
Fri, 10 Sep 1999 18:37:04 +0200 new theorem image_image_eq_UN
changeset
paulson [Fri, 10 Sep 1999 18:37:04 +0200] rev 7536
new theorem image_image_eq_UN
Fri, 10 Sep 1999 17:28:51 +0200 The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
changeset
wenzelm [Fri, 10 Sep 1999 17:28:51 +0200] rev 7535
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar) (by Gertrud Bauer, TU Munich);
Thu, 09 Sep 1999 19:01:37 +0200 added no_prems;
changeset
wenzelm [Thu, 09 Sep 1999 19:01:37 +0200] rev 7534
added no_prems;
Thu, 09 Sep 1999 14:30:08 +0200 minor change to smp_tac
changeset
oheimb [Thu, 09 Sep 1999 14:30:08 +0200] rev 7533
minor change to smp_tac
Thu, 09 Sep 1999 13:24:26 +0200 fixed url;
changeset
wenzelm [Thu, 09 Sep 1999 13:24:26 +0200] rev 7532
fixed url;
Thu, 09 Sep 1999 12:26:45 +0200 AddXDs [bspec];
changeset
wenzelm [Thu, 09 Sep 1999 12:26:45 +0200] rev 7531
AddXDs [bspec];
Thu, 09 Sep 1999 12:25:44 +0200 tuned;
changeset
wenzelm [Thu, 09 Sep 1999 12:25:44 +0200] rev 7530
tuned;
Thu, 09 Sep 1999 12:25:30 +0200 AddXIs [disjI1, disjI2];
changeset
wenzelm [Thu, 09 Sep 1999 12:25:30 +0200] rev 7529
AddXIs [disjI1, disjI2];
Thu, 09 Sep 1999 12:25:01 +0200 removed obsolete comment;
changeset
wenzelm [Thu, 09 Sep 1999 12:25:01 +0200] rev 7528
removed obsolete comment;
Wed, 08 Sep 1999 23:49:39 +0200 lemma less_add;
changeset
wenzelm [Wed, 08 Sep 1999 23:49:39 +0200] rev 7527
lemma less_add;
Wed, 08 Sep 1999 18:10:39 +0200 (un)fold: ignore facts;
changeset
wenzelm [Wed, 08 Sep 1999 18:10:39 +0200] rev 7526
(un)fold: ignore facts;
Wed, 08 Sep 1999 16:44:11 +0200 more rational theorem names (?)
changeset
paulson [Wed, 08 Sep 1999 16:44:11 +0200] rev 7525
more rational theorem names (?)
Wed, 08 Sep 1999 16:43:26 +0200 tidied
changeset
paulson [Wed, 08 Sep 1999 16:43:26 +0200] rev 7524
tidied
Wed, 08 Sep 1999 15:50:11 +0200 more rational theorem names (?)
changeset
paulson [Wed, 08 Sep 1999 15:50:11 +0200] rev 7523
more rational theorem names (?)
Wed, 08 Sep 1999 15:45:36 +0200 ensures_tac now handles leadsTo as well as LeadsTo
changeset
paulson [Wed, 08 Sep 1999 15:45:36 +0200] rev 7522
ensures_tac now handles leadsTo as well as LeadsTo
Wed, 08 Sep 1999 15:44:56 +0200 new theorem single_Diff_lessThan
changeset
paulson [Wed, 08 Sep 1999 15:44:56 +0200] rev 7521
new theorem single_Diff_lessThan
Wed, 08 Sep 1999 15:44:11 +0200 now uses the identity function
changeset
paulson [Wed, 08 Sep 1999 15:44:11 +0200] rev 7520
now uses the identity function
Wed, 08 Sep 1999 15:41:58 +0200 simplification of relations involving 0, Suc and natural-number numerals
changeset
paulson [Wed, 08 Sep 1999 15:41:58 +0200] rev 7519
simplification of relations involving 0, Suc and natural-number numerals
Wed, 08 Sep 1999 15:41:30 +0200 generalized the theorem zless_zero_nat to zless_nat_eq_int_zless, and
changeset
paulson [Wed, 08 Sep 1999 15:41:30 +0200] rev 7518
generalized the theorem zless_zero_nat to zless_nat_eq_int_zless, and reorganized
Wed, 08 Sep 1999 15:40:39 +0200 generalized the theorem bin_add_BIT_Min to bin_add_Min_right
changeset
paulson [Wed, 08 Sep 1999 15:40:39 +0200] rev 7517
generalized the theorem bin_add_BIT_Min to bin_add_Min_right
Wed, 08 Sep 1999 15:39:52 +0200 moved identity theorems to Fun.ML
changeset
paulson [Wed, 08 Sep 1999 15:39:52 +0200] rev 7516
moved identity theorems to Fun.ML
Wed, 08 Sep 1999 15:38:54 +0200 comments
changeset
paulson [Wed, 08 Sep 1999 15:38:54 +0200] rev 7515
comments
(0) -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 +30000 tip
isabelle