Mercurial Mercurial > repos > isabelle / changelog
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -10000 -3000 -1000 -300 -100 -50 -24 +24 +50 +100 +300 +1000 +3000 +10000 +30000 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Tue, 22 Feb 2005 10:54:30 +0100 more setsum tuning
changeset
nipkow [Tue, 22 Feb 2005 10:54:30 +0100] rev 15543
more setsum tuning
Mon, 21 Feb 2005 19:23:46 +0100 more fine tuniung
changeset
nipkow [Mon, 21 Feb 2005 19:23:46 +0100] rev 15542
more fine tuniung
Mon, 21 Feb 2005 18:04:28 +0100 fixed proof
changeset
nipkow [Mon, 21 Feb 2005 18:04:28 +0100] rev 15541
fixed proof
Mon, 21 Feb 2005 15:57:45 +0100 removed superfluous setsum_constant
changeset
nipkow [Mon, 21 Feb 2005 15:57:45 +0100] rev 15540
removed superfluous setsum_constant
Mon, 21 Feb 2005 15:04:10 +0100 comprehensive cleanup, replacing sumr by setsum
changeset
nipkow [Mon, 21 Feb 2005 15:04:10 +0100] rev 15539
comprehensive cleanup, replacing sumr by setsum
Sat, 19 Feb 2005 18:44:34 +0100 lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
changeset
dixon [Sat, 19 Feb 2005 18:44:34 +0100] rev 15538
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
Fri, 18 Feb 2005 15:20:27 +0100 continued eliminating sumr
changeset
nipkow [Fri, 18 Feb 2005 15:20:27 +0100] rev 15537
continued eliminating sumr
Fri, 18 Feb 2005 11:48:53 +0100 starting to get rid of sumr
changeset
nipkow [Fri, 18 Feb 2005 11:48:53 +0100] rev 15536
starting to get rid of sumr
Fri, 18 Feb 2005 11:48:42 +0100 tuning
changeset
nipkow [Fri, 18 Feb 2005 11:48:42 +0100] rev 15535
tuning
Wed, 16 Feb 2005 19:00:49 +0100 *** empty log message ***
changeset
nipkow [Wed, 16 Feb 2005 19:00:49 +0100] rev 15534
*** empty log message ***
Tue, 15 Feb 2005 16:56:15 +0100 refine now provides specific cases "goal1" ... "goaln" for addressing
changeset
berghofe [Tue, 15 Feb 2005 16:56:15 +0100] rev 15533
refine now provides specific cases "goal1" ... "goaln" for addressing subgoals of a proof state.
Mon, 14 Feb 2005 10:24:58 +0100 simplified a proof
changeset
paulson [Mon, 14 Feb 2005 10:24:58 +0100] rev 15532
simplified a proof
Sun, 13 Feb 2005 17:15:14 +0100 Deleted Library.option type.
changeset
skalberg [Sun, 13 Feb 2005 17:15:14 +0100] rev 15531
Deleted Library.option type.
Fri, 11 Feb 2005 18:51:00 +0100 Fully qualified refl and trans to avoid confusion with theorems
changeset
berghofe [Fri, 11 Feb 2005 18:51:00 +0100] rev 15530
Fully qualified refl and trans to avoid confusion with theorems in Lattice_Locales.partial_order.
Fri, 11 Feb 2005 17:11:24 +0100 Optimized present_tokens to produce fewer newlines when hiding proofs.
changeset
berghofe [Fri, 11 Feb 2005 17:11:24 +0100] rev 15529
Optimized present_tokens to produce fewer newlines when hiding proofs.
Fri, 11 Feb 2005 10:03:41 +0100 New reference Toplevel.debug for verbose printing of exns.
changeset
ballarin [Fri, 11 Feb 2005 10:03:41 +0100] rev 15528
New reference Toplevel.debug for verbose printing of exns.
Fri, 11 Feb 2005 04:36:22 +0100 update from Larry
changeset
kleing [Fri, 11 Feb 2005 04:36:22 +0100] rev 15527
update from Larry
Thu, 10 Feb 2005 19:14:35 +0100 some stuff is now redundant.
changeset
nipkow [Thu, 10 Feb 2005 19:14:35 +0100] rev 15526
some stuff is now redundant.
Thu, 10 Feb 2005 18:51:54 +0100 HOL.order -> Orderings.order due to restructering
changeset
nipkow [Thu, 10 Feb 2005 18:51:54 +0100] rev 15525
HOL.order -> Orderings.order due to restructering
Thu, 10 Feb 2005 18:51:12 +0100 Moved oderings from HOL into the new Orderings.thy
changeset
nipkow [Thu, 10 Feb 2005 18:51:12 +0100] rev 15524
Moved oderings from HOL into the new Orderings.thy
Thu, 10 Feb 2005 17:09:15 +0100 Added paper by M. Takahashi.
changeset
berghofe [Thu, 10 Feb 2005 17:09:15 +0100] rev 15523
Added paper by M. Takahashi.
Thu, 10 Feb 2005 17:08:45 +0100 Added proof of eta-postponement theorem (using parallel eta-reduction).
changeset
berghofe [Thu, 10 Feb 2005 17:08:45 +0100] rev 15522
Added proof of eta-postponement theorem (using parallel eta-reduction).
Thu, 10 Feb 2005 16:03:18 +0100 non-inductive fold1Set proofs
changeset
paulson [Thu, 10 Feb 2005 16:03:18 +0100] rev 15521
non-inductive fold1Set proofs
Thu, 10 Feb 2005 13:01:46 +0100 simplified a key lemma for foldSet
changeset
paulson [Thu, 10 Feb 2005 13:01:46 +0100] rev 15520
simplified a key lemma for foldSet
(0) -10000 -3000 -1000 -300 -100 -50 -24 +24 +50 +100 +300 +1000 +3000 +10000 +30000 tip
isabelle