| Mon, 26 Mar 2018 16:14:16 +0200 |
Manuel Eberl |
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
|
file |
diff |
annotate
|
| Mon, 12 Mar 2018 20:52:53 +0100 |
Manuel Eberl |
Changes to complete distributive lattices due to Viorel Preoteasa
|
file |
diff |
annotate
|
| Thu, 15 Feb 2018 12:11:00 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Sun, 26 Nov 2017 21:08:32 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Mon, 09 Oct 2017 19:10:49 +0200 |
haftmann |
clarified uniqueness criterion for euclidean rings
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:22 +0200 |
haftmann |
euclidean rings need no normalization
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:21 +0200 |
haftmann |
abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel
|
file |
diff |
annotate
|
| Mon, 29 May 2017 09:14:15 +0200 |
eberlm |
reorganised material on sublists
|
file |
diff |
annotate
|
| Sat, 17 Dec 2016 15:22:14 +0100 |
haftmann |
more fine-grained type class hierarchy for div and mod
|
file |
diff |
annotate
|
| Tue, 18 Oct 2016 18:48:53 +0200 |
haftmann |
suitable logical type class for abs, sgn
|
file |
diff |
annotate
|
| Mon, 26 Sep 2016 07:56:54 +0200 |
haftmann |
syntactic type class for operation mod named after mod;
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 16:25:08 +0100 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:56 +0100 |
haftmann |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
file |
diff |
annotate
|
| Mon, 07 Dec 2015 10:38:04 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Sun, 13 Sep 2015 22:56:52 +0200 |
wenzelm |
tuned proofs -- less legacy;
|
file |
diff |
annotate
|
| Tue, 01 Sep 2015 22:32:58 +0200 |
wenzelm |
eliminated \<Colon>;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 22:58:50 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Fri, 12 Jun 2015 08:53:23 +0200 |
haftmann |
uniform _ div _ as infix syntax for ring division
|
file |
diff |
annotate
|
| Mon, 01 Jun 2015 18:59:21 +0200 |
haftmann |
separate class for division operator, with particular syntax added in more specific classes
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 21:54:32 +0200 |
haftmann |
given up separate type classes demanding `inverse 0 = 0`
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Mon, 20 Oct 2014 07:45:58 +0200 |
haftmann |
augmented and tuned facts on even/odd and division
|
file |
diff |
annotate
|
| Mon, 13 Oct 2014 18:45:48 +0200 |
wenzelm |
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
|
file |
diff |
annotate
|
| Fri, 10 Oct 2014 19:55:32 +0200 |
haftmann |
specialized specification: avoid trivial instances
|
file |
diff |
annotate
|
| Tue, 16 Sep 2014 19:23:37 +0200 |
blanchet |
added 'extraction' plugins -- this might help 'HOL-Proofs'
|
file |
diff |
annotate
|
| Sun, 14 Sep 2014 22:59:30 +0200 |
blanchet |
disable datatype 'plugins' for internal types
|
file |
diff |
annotate
|
| Thu, 11 Sep 2014 19:32:36 +0200 |
blanchet |
updated news
|
file |
diff |
annotate
|
| Wed, 03 Sep 2014 00:06:24 +0200 |
blanchet |
use 'datatype_new' in 'Main'
|
file |
diff |
annotate
|
| Sun, 31 Aug 2014 09:10:42 +0200 |
haftmann |
separated listsum material
|
file |
diff |
annotate
|
| Wed, 13 Aug 2014 17:17:51 +0200 |
Andreas Lochbihler |
add algebraic type class instances for Enum.finite* types
|
file |
diff |
annotate
|
| Fri, 08 Aug 2014 17:36:08 +0200 |
Andreas Lochbihler |
add complete_lattice instances for Enum.finite_* types such that quickcheck deals with lattice class operations
|
file |
diff |
annotate
|
| Thu, 12 Jun 2014 18:47:16 +0200 |
nipkow |
added [simp]
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 23:07:23 +0100 |
blanchet |
moved 'bacc' back to 'Enum' (cf. 744934b818c7) -- reduces baggage loaded by 'Hilbert_Choice'
|
file |
diff |
annotate
|
| Wed, 01 Jan 2014 01:05:48 +0100 |
haftmann |
fundamental treatment of undefined vs. universally partial replaces code_abort
|
file |
diff |
annotate
|
| Sun, 10 Nov 2013 15:05:06 +0100 |
haftmann |
qualifed popular user space names
|
file |
diff |
annotate
|
| Fri, 18 Oct 2013 10:43:21 +0200 |
blanchet |
killed more "no_atp"s
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 16:25:47 +0200 |
wenzelm |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
file |
diff |
annotate
|
| Sun, 23 Jun 2013 21:16:07 +0200 |
haftmann |
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
|
file |
diff |
annotate
|
| Sun, 16 Dec 2012 18:07:29 +0100 |
bulwahn |
providing a custom code equation for vimage to overwrite the vimage definition that would be rewritten by set_comprehension_pointfree simproc in the code preprocessor to an non-terminating code equation
|
file |
diff |
annotate
|
| Mon, 22 Oct 2012 22:24:34 +0200 |
haftmann |
incorporated constant chars into instantiation proof for enum;
|
file |
diff |
annotate
|
| Sat, 20 Oct 2012 10:00:21 +0200 |
haftmann |
tailored enum specification towards simple instantiation;
|
file |
diff |
annotate
|
| Sat, 20 Oct 2012 10:00:21 +0200 |
haftmann |
refined internal structure of Enum.thy
|
file |
diff |
annotate
|
| Sat, 20 Oct 2012 09:12:16 +0200 |
haftmann |
moved quite generic material from theory Enum to more appropriate places
|
file |
diff |
annotate
|
| Mon, 25 Jun 2012 16:03:21 +0200 |
bulwahn |
some special code equations for Id with class constraint enum after adding the set comprehension simproc to the code preprocessing
|
file |
diff |
annotate
|
| Fri, 30 Mar 2012 17:25:34 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Fri, 30 Mar 2012 17:22:17 +0200 |
wenzelm |
tuned proofs, less guesswork;
|
file |
diff |
annotate
|
| Fri, 30 Mar 2012 14:00:18 +0200 |
huffman |
rephrase lemma card_Pow using '2' instead of 'Suc (Suc 0)'
|
file |
diff |
annotate
|
| Mon, 30 Jan 2012 13:55:24 +0100 |
bulwahn |
adding code equations for max_extp and mlex
|
file |
diff |
annotate
|
| Mon, 30 Jan 2012 13:55:22 +0100 |
bulwahn |
adding code equation for rtranclp in Enum
|
file |
diff |
annotate
|
| Mon, 30 Jan 2012 13:55:21 +0100 |
bulwahn |
adding code equation for max_ext
|
file |
diff |
annotate
|
| Mon, 30 Jan 2012 13:55:20 +0100 |
bulwahn |
adding code equation for tranclp
|
file |
diff |
annotate
|
| Sat, 28 Jan 2012 12:05:26 +0100 |
bulwahn |
an executable version of accessible part (only for finite types yet)
|
file |
diff |
annotate
|
| Thu, 26 Jan 2012 12:03:35 +0100 |
bulwahn |
evaluation of THE with a non-singleton set raises a Match exception during the evaluation to yield a potential counterexample in quickcheck.
|
file |
diff |
annotate
|
| Wed, 25 Jan 2012 09:32:23 +0100 |
bulwahn |
adding code equation for Collect on finite types
|
file |
diff |
annotate
|
| Sat, 24 Dec 2011 15:53:08 +0100 |
haftmann |
enum type class instance for `set`; dropped misfitting code lemma for trancl
|
file |
diff |
annotate
|
| Fri, 14 Oct 2011 18:55:59 +0200 |
haftmann |
moved sublists to More_List.thy
|
file |
diff |
annotate
|
| Thu, 13 Oct 2011 23:35:15 +0200 |
haftmann |
avoid very specific code equation for card; corrected spelling
|
file |
diff |
annotate
|
| Thu, 13 Oct 2011 23:27:46 +0200 |
haftmann |
bouned transitive closure
|
file |
diff |
annotate
|