Tue, 19 Nov 2013 10:05:53 +0100 |
haftmann |
eliminiated neg_numeral in favour of - (numeral _)
|
file |
diff |
annotate
|
Fri, 01 Nov 2013 18:51:14 +0100 |
haftmann |
more simplification rules on unary and binary minus
|
file |
diff |
annotate
|
Fri, 23 Aug 2013 17:01:12 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Thu, 07 Mar 2013 17:50:26 +0100 |
wenzelm |
tuned proofs -- more structure, less warnings;
|
file |
diff |
annotate
|
Mon, 25 Feb 2013 12:17:50 +0100 |
wenzelm |
prefer stateless 'ML_val' for tests;
|
file |
diff |
annotate
|
Fri, 15 Feb 2013 08:31:31 +0100 |
haftmann |
two target language numeral types: integer and natural, as replacement for code_numeral;
|
file |
diff |
annotate
|
Wed, 28 Nov 2012 15:59:18 +0100 |
wenzelm |
eliminated slightly odd identifiers;
|
file |
diff |
annotate
|
Tue, 27 Nov 2012 13:22:29 +0100 |
wenzelm |
eliminated some improper identifiers;
|
file |
diff |
annotate
|
Fri, 19 Oct 2012 15:12:52 +0200 |
webertj |
Renamed {left,right}_distrib to distrib_{right,left}.
|
file |
diff |
annotate
|
Mon, 03 Sep 2012 09:15:40 +0200 |
wenzelm |
some parallel ML;
|
file |
diff |
annotate
|
Wed, 22 Aug 2012 22:55:41 +0200 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
Thu, 12 Apr 2012 18:39:19 +0200 |
wenzelm |
more standard method setup;
|
file |
diff |
annotate
|
Tue, 27 Mar 2012 14:49:56 +0200 |
huffman |
remove redundant lemmas
|
file |
diff |
annotate
|
Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
Sat, 25 Feb 2012 09:07:39 +0100 |
bulwahn |
removing unnecessary assumptions in RealDef;
|
file |
diff |
annotate
|
Fri, 06 Jan 2012 10:19:48 +0100 |
haftmann |
prefer concat over foldl append []
|
file |
diff |
annotate
|
Fri, 02 Dec 2011 14:54:25 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
Wed, 10 Aug 2011 20:53:43 +0200 |
wenzelm |
old term operations are legacy;
|
file |
diff |
annotate
|
Tue, 02 Aug 2011 10:36:50 +0200 |
krauss |
moved recdef package to HOL/Library/Old_Recdef.thy
|
file |
diff |
annotate
|
Thu, 03 Mar 2011 21:43:06 +0100 |
wenzelm |
tuned proofs -- eliminated prems;
|
file |
diff |
annotate
|
Thu, 03 Mar 2011 15:19:20 +0100 |
wenzelm |
removed spurious 'unused_thms' (cf. 1a65b780bd56);
|
file |
diff |
annotate
|
Fri, 25 Feb 2011 20:07:48 +0100 |
nipkow |
Some cleaning up
|
file |
diff |
annotate
|
Thu, 24 Feb 2011 21:54:28 +0100 |
krauss |
recdef -> fun(ction)
|
file |
diff |
annotate
|
Thu, 24 Feb 2011 17:38:05 +0100 |
krauss |
eliminated clones of List.upto
|
file |
diff |
annotate
|
Mon, 21 Feb 2011 23:47:19 +0100 |
wenzelm |
tuned proofs -- eliminated prems;
|
file |
diff |
annotate
|
Fri, 07 Jan 2011 18:10:42 +0100 |
bulwahn |
adopting proofs due to new list comprehension to set comprehension simproc
|
file |
diff |
annotate
|
Wed, 29 Dec 2010 17:34:41 +0100 |
wenzelm |
explicit file specifications -- avoid secondary load path;
|
file |
diff |
annotate
|
Fri, 27 Aug 2010 10:56:46 +0200 |
haftmann |
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
|
file |
diff |
annotate
|
Thu, 26 Aug 2010 20:51:17 +0200 |
haftmann |
formerly unnamed infix impliciation now named HOL.implies
|
file |
diff |
annotate
|
Thu, 19 Aug 2010 16:08:59 +0200 |
haftmann |
tuned quotes
|
file |
diff |
annotate
|
Thu, 19 Aug 2010 11:02:14 +0200 |
haftmann |
use antiquotations for remaining unqualified constants in HOL
|
file |
diff |
annotate
|
Mon, 19 Jul 2010 16:09:44 +0200 |
haftmann |
diff_minus subsumes diff_def
|
file |
diff |
annotate
|
Wed, 12 May 2010 12:31:51 +0200 |
haftmann |
tuned test problems
|
file |
diff |
annotate
|
Sun, 09 May 2010 22:51:11 -0700 |
huffman |
avoid using real-specific versions of generic lemmas
|
file |
diff |
annotate
|
Thu, 29 Apr 2010 15:00:40 +0200 |
haftmann |
code_reflect: specify module name directly after keyword
|
file |
diff |
annotate
|
Wed, 28 Apr 2010 21:41:05 +0200 |
haftmann |
use code_reflect
|
file |
diff |
annotate
|
Mon, 01 Mar 2010 13:40:23 +0100 |
haftmann |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
file |
diff |
annotate
|
Fri, 05 Feb 2010 14:33:50 +0100 |
haftmann |
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
|
file |
diff |
annotate
|
Thu, 12 Nov 2009 17:21:48 +0100 |
hoelzl |
New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
|
file |
diff |
annotate
|
Thu, 22 Oct 2009 13:48:06 +0200 |
haftmann |
map_range (and map_index) combinator
|
file |
diff |
annotate
|
Sat, 17 Oct 2009 14:43:18 +0200 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
Tue, 07 Jul 2009 17:39:51 +0200 |
nipkow |
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
|
file |
diff |
annotate
|
Sat, 20 Jun 2009 13:34:54 +0200 |
nipkow |
added lemmas; tuned
|
file |
diff |
annotate
|
Wed, 17 Jun 2009 16:55:01 -0700 |
huffman |
new GCD library, courtesy of Jeremy Avigad
|
file |
diff |
annotate
|
Sun, 22 Mar 2009 19:36:04 +0100 |
nipkow |
1. New cancellation simprocs for common factors in inequations
|
file |
diff |
annotate
|
Wed, 11 Mar 2009 10:58:18 +0100 |
hoelzl |
Updated paths in Decision_Procs comments and NEWS
|
file |
diff |
annotate
|
Wed, 04 Mar 2009 11:05:29 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
Wed, 04 Mar 2009 10:45:52 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
Thu, 26 Feb 2009 06:33:48 -0800 |
huffman |
add type annotation
|
file |
diff |
annotate
|
Wed, 25 Feb 2009 11:29:59 -0800 |
huffman |
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
|
file |
diff |
annotate
|
Sat, 21 Feb 2009 20:52:30 +0100 |
nipkow |
Removed subsumed lemmas
|
file |
diff |
annotate
|
Fri, 06 Feb 2009 15:15:32 +0100 |
haftmann |
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
|
file |
diff |
annotate
| base
|