| Sat, 14 Sep 2013 18:24:12 +0200 |
tuned proof
|
file | diff | annotate |
| Sun, 25 Aug 2013 23:20:25 +0200 |
tuned proofs;
|
file | diff | annotate |
| Sun, 25 Aug 2013 17:17:48 +0200 |
tuned proofs -- fewer warnings;
|
file | diff | annotate |
| Fri, 19 Oct 2012 15:12:52 +0200 |
Renamed {left,right}_distrib to distrib_{right,left}.
|
file | diff | annotate |
| Tue, 09 Oct 2012 22:24:24 +0200 |
removed redundant lemma, cf. class zero_neq_one in HOL/Rings.thy;
|
file | diff | annotate |
| Tue, 28 Feb 2012 20:20:09 +0100 |
tuned proofs;
|
file | diff | annotate |
| Wed, 12 Oct 2011 20:16:48 +0200 |
tuned proofs -- eliminated vacuous "induct arbitrary: ..." situations;
|
file | diff | annotate |
| Mon, 13 Sep 2010 11:13:15 +0200 |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file | diff | annotate |
| Tue, 07 Sep 2010 10:05:19 +0200 |
expand_fun_eq -> ext_iff
|
file | diff | annotate |
| Mon, 19 Jul 2010 16:09:44 +0200 |
diff_minus subsumes diff_def
|
file | diff | annotate |
| Mon, 12 Jul 2010 08:58:13 +0200 |
dropped superfluous [code del]s
|
file | diff | annotate |
| Mon, 28 Jun 2010 15:32:17 +0200 |
explicit is better than implicit
|
file | diff | annotate |
| Fri, 05 Feb 2010 14:33:50 +0100 |
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
|
file | diff | annotate |
| Sat, 17 Oct 2009 14:43:18 +0200 |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file | diff | annotate |
| Mon, 31 Aug 2009 14:09:42 +0200 |
tuned the simp rules for Int involving insert and intervals.
|
file | diff | annotate |
| Wed, 29 Apr 2009 14:20:26 +0200 |
farewell to class recpower
|
file | diff | annotate |
| Fri, 27 Mar 2009 10:05:11 +0100 |
normalized imports
|
file | diff | annotate |
| Thu, 12 Mar 2009 08:57:03 -0700 |
remove trailing spaces
|
file | diff | annotate |
| Thu, 12 Feb 2009 18:14:43 +0100 |
Moved FTA into Lib and cleaned it up a little.
|
file | diff | annotate |
| Wed, 28 Jan 2009 16:29:16 +0100 |
Replaced group_ and ring_simps by algebra_simps;
|
file | diff | annotate |
| Fri, 16 Jan 2009 08:28:53 +0100 |
moved Univ_Poly to Library
|
file | diff | annotate | base |
| Mon, 17 Nov 2008 17:00:55 +0100 |
tuned unfold_locales invocation
|
file | diff | annotate |
| Fri, 10 Oct 2008 06:45:53 +0200 |
`code func` now just `code`
|
file | diff | annotate |
| Mon, 07 Jul 2008 08:47:17 +0200 |
absolute imports of HOL/*.thy theories
|
file | diff | annotate |
| Wed, 02 Jul 2008 07:11:57 +0200 |
cleaned up some code generator configuration
|
file | diff | annotate |
| Thu, 26 Jun 2008 10:07:01 +0200 |
established Plain theory and image
|
file | diff | annotate |
| Mon, 17 Mar 2008 22:34:27 +0100 |
avoid rebinding of existing facts;
|
file | diff | annotate |
| Mon, 03 Mar 2008 15:37:16 +0100 |
tuned
|
file | diff | annotate |
| Mon, 25 Feb 2008 11:27:27 +0100 |
A library for univariate polynomials -- generalizes old Hyperreal/Poly.thy from reals to locales
|
file | diff | annotate |