isabelle: Changelog

Mercurial Mercurial > repos > isabelle / changelog

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -30000 -10000 -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 +30000 tip

Fri, 28 Oct 2011 15:38:41 +0200 slightly more explicit/syntactic modelling of morphisms;

wenzelm [Fri, 28 Oct 2011 15:38:41 +0200] rev 45289

slightly more explicit/syntactic modelling of morphisms;

Fri, 28 Oct 2011 14:10:19 +0200 correct import path

hoelzl [Fri, 28 Oct 2011 14:10:19 +0200] rev 45288

correct import path

Fri, 28 Oct 2011 14:06:06 +0200 allow to build Probability and MV-Analysis with one ROOT.ML

hoelzl [Fri, 28 Oct 2011 14:06:06 +0200] rev 45287

allow to build Probability and MV-Analysis with one ROOT.ML

Fri, 28 Oct 2011 12:37:18 +0200 removing dead code

bulwahn [Fri, 28 Oct 2011 12:37:18 +0200] rev 45286

removing dead code

Fri, 28 Oct 2011 10:33:23 +0200 ex/Simproc_Tests.thy: remove duplicate simprocs

huffman [Fri, 28 Oct 2011 10:33:23 +0200] rev 45285

ex/Simproc_Tests.thy: remove duplicate simprocs

Fri, 28 Oct 2011 11:02:27 +0200 use simproc_setup for cancellation simprocs, to get proper name bindings

huffman [Fri, 28 Oct 2011 11:02:27 +0200] rev 45284

use simproc_setup for cancellation simprocs, to get proper name bindings

Thu, 27 Oct 2011 22:37:19 +0200 tuned;

wenzelm [Thu, 27 Oct 2011 22:37:19 +0200] rev 45283

tuned;

Thu, 27 Oct 2011 22:20:55 +0200 eliminated aliases of standard functions;

wenzelm [Thu, 27 Oct 2011 22:20:55 +0200] rev 45282

eliminated aliases of standard functions;

Thu, 27 Oct 2011 21:52:57 +0200 more standard attribute setup;

wenzelm [Thu, 27 Oct 2011 21:52:57 +0200] rev 45281

more standard attribute setup;

Thu, 27 Oct 2011 21:02:10 +0200 localized quotient data;

wenzelm [Thu, 27 Oct 2011 21:02:10 +0200] rev 45280

localized quotient data;

Thu, 27 Oct 2011 20:26:38 +0200 simplified/standardized signatures;

wenzelm [Thu, 27 Oct 2011 20:26:38 +0200] rev 45279

simplified/standardized signatures;

Thu, 27 Oct 2011 19:41:08 +0200 tuned signature;

wenzelm [Thu, 27 Oct 2011 19:41:08 +0200] rev 45278

tuned signature;

Thu, 27 Oct 2011 16:28:34 +0200 uses IMP and hence requires its tex setup

nipkow [Thu, 27 Oct 2011 16:28:34 +0200] rev 45277

uses IMP and hence requires its tex setup

Thu, 27 Oct 2011 15:59:33 +0200 merged

nipkow [Thu, 27 Oct 2011 15:59:33 +0200] rev 45276

merged

Thu, 27 Oct 2011 15:59:25 +0200 tuned text

nipkow [Thu, 27 Oct 2011 15:59:25 +0200] rev 45275

tuned text

Thu, 27 Oct 2011 13:52:31 +0200 respecting isabelle's programming style in the quotient package by simplifying qconsts_lookup function for data access; removing odd NotFound exception

bulwahn [Thu, 27 Oct 2011 13:52:31 +0200] rev 45274

respecting isabelle's programming style in the quotient package by simplifying qconsts_lookup function for data access; removing odd NotFound exception

Thu, 27 Oct 2011 13:50:55 +0200 respecting isabelle's programming style in the quotient package by simplifying map_lookup function for data access

bulwahn [Thu, 27 Oct 2011 13:50:55 +0200] rev 45273

respecting isabelle's programming style in the quotient package by simplifying map_lookup function for data access

Thu, 27 Oct 2011 13:50:54 +0200 respecting isabelle's programming style in the quotient package by simplifying quotdata_lookup function for data access

bulwahn [Thu, 27 Oct 2011 13:50:54 +0200] rev 45272

respecting isabelle's programming style in the quotient package by simplifying quotdata_lookup function for data access

Thu, 27 Oct 2011 07:48:07 +0200 merged

huffman [Thu, 27 Oct 2011 07:48:07 +0200] rev 45271

merged

Thu, 27 Oct 2011 07:46:57 +0200 fix bug in cancel_factor simprocs so they will work on goals like 'x * y < x * z' where the common term is already on the left

huffman [Thu, 27 Oct 2011 07:46:57 +0200] rev 45270

fix bug in cancel_factor simprocs so they will work on goals like 'x * y < x * z' where the common term is already on the left

Wed, 26 Oct 2011 22:51:06 +0200 more robust ML pretty printing (cf. b6c527c64789);

wenzelm [Wed, 26 Oct 2011 22:51:06 +0200] rev 45269

more robust ML pretty printing (cf. b6c527c64789);

Wed, 26 Oct 2011 22:50:40 +0200 tuned;

wenzelm [Wed, 26 Oct 2011 22:50:40 +0200] rev 45268

tuned;

Tue, 25 Oct 2011 16:37:11 +0200 renaming Cset and List_Cset in Quotient_Examples to Quotient_Set and List_Quotient_Set to avoid a name clash of theory names with the ones in HOL-Library

bulwahn [Tue, 25 Oct 2011 16:37:11 +0200] rev 45267

renaming Cset and List_Cset in Quotient_Examples to Quotient_Set and List_Quotient_Set to avoid a name clash of theory names with the ones in HOL-Library

Tue, 25 Oct 2011 16:09:02 +0200 tuned text

nipkow [Tue, 25 Oct 2011 16:09:02 +0200] rev 45266

tuned text

Tue, 25 Oct 2011 15:59:15 +0200 tuned names to avoid shadowing

nipkow [Tue, 25 Oct 2011 15:59:15 +0200] rev 45265

tuned names to avoid shadowing

Tue, 25 Oct 2011 12:00:52 +0200 merge Gcd/GCD and Lcm/LCM

huffman [Tue, 25 Oct 2011 12:00:52 +0200] rev 45264

merge Gcd/GCD and Lcm/LCM

Tue, 25 Oct 2011 08:48:36 +0200 clarify types of terms: use proper set type

boehmes [Tue, 25 Oct 2011 08:48:36 +0200] rev 45263

clarify types of terms: use proper set type

Mon, 24 Oct 2011 16:47:24 +0200 instance bool :: linorder

huffman [Mon, 24 Oct 2011 16:47:24 +0200] rev 45262

instance bool :: linorder

Mon, 24 Oct 2011 12:26:05 +0200 removing poor man's dictionary construction which were only for the ancient code generator with no support of type classes

bulwahn [Mon, 24 Oct 2011 12:26:05 +0200] rev 45261

removing poor man's dictionary construction which were only for the ancient code generator with no support of type classes

Mon, 24 Oct 2011 11:40:31 +0200 fixed typo

bulwahn [Mon, 24 Oct 2011 11:40:31 +0200] rev 45260

fixed typo

(0) -30000 -10000 -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle