| Tue, 03 Sep 2013 01:12:40 +0200 |
wenzelm |
tuned proofs -- clarified flow of facts wrt. calculation;
|
file |
diff |
annotate
|
| Thu, 25 Jul 2013 08:57:16 +0200 |
haftmann |
factored syntactic type classes for bot and top (by Alessandro Coglio)
|
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, 02 Jun 2013 20:44:55 +0200 |
haftmann |
type class for confined subtraction
|
file |
diff |
annotate
|
| Wed, 20 Feb 2013 12:04:42 +0100 |
hoelzl |
split dense into inner_dense_order and no_top/no_bot
|
file |
diff |
annotate
|
| Sun, 24 Feb 2013 20:29:13 +0100 |
haftmann |
turned example into library for comparing growth of functions
|
file |
diff |
annotate
|
| Sun, 17 Feb 2013 21:29:30 +0100 |
haftmann |
Sieve of Eratosthenes
|
file |
diff |
annotate
|
| Fri, 19 Oct 2012 15:12:52 +0200 |
webertj |
Renamed {left,right}_distrib to distrib_{right,left}.
|
file |
diff |
annotate
|
| Fri, 12 Oct 2012 18:58:20 +0200 |
wenzelm |
discontinued obsolete typedef (open) syntax;
|
file |
diff |
annotate
|
| Sat, 06 Oct 2012 11:08:52 +0200 |
haftmann |
alternative simplification of ^^ to the righthand side;
|
file |
diff |
annotate
|
| Sat, 15 Sep 2012 20:14:29 +0200 |
haftmann |
typeclass formalising bounded subtraction
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 22:55:41 +0200 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
| Fri, 27 Jul 2012 17:59:18 +0200 |
huffman |
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
|
file |
diff |
annotate
|
| Fri, 27 Jul 2012 17:57:31 +0200 |
huffman |
give Nat_Arith simprocs proper name bindings by using simproc_setup
|
file |
diff |
annotate
|
| Thu, 24 May 2012 17:25:53 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Mon, 16 Apr 2012 11:24:57 +0200 |
huffman |
tuned some proofs;
|
file |
diff |
annotate
|
| Sun, 01 Apr 2012 16:09:58 +0200 |
huffman |
removed Nat_Numeral.thy, moving all theorems elsewhere
|
file |
diff |
annotate
|
| Fri, 30 Mar 2012 08:11:52 +0200 |
huffman |
move lemmas from Nat_Numeral.thy to Nat.thy
|
file |
diff |
annotate
|
| Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
| Sat, 28 Jan 2012 10:35:52 +0100 |
bulwahn |
adding yet another induction rule on natural numbers
|
file |
diff |
annotate
|
| Sat, 28 Jan 2012 10:22:46 +0100 |
bulwahn |
moving declarations back to the section they seem to belong to (cf. afffe1f72143)
|
file |
diff |
annotate
|
| Thu, 29 Dec 2011 10:47:55 +0100 |
haftmann |
attribute code_abbrev superseedes code_unfold_post
|
file |
diff |
annotate
|
| Sat, 24 Dec 2011 15:53:09 +0100 |
haftmann |
generalized type signature to permit overloading on `set`
|
file |
diff |
annotate
|
| Mon, 19 Dec 2011 14:41:08 +0100 |
noschinl |
add lemmas
|
file |
diff |
annotate
|
| Mon, 19 Dec 2011 14:41:08 +0100 |
noschinl |
weaken preconditions on lemmas
|
file |
diff |
annotate
|
| Tue, 13 Dec 2011 16:14:41 +0100 |
nipkow |
lemmas about Kleene iteration
|
file |
diff |
annotate
|
| Wed, 30 Nov 2011 18:07:14 +0100 |
wenzelm |
prefer typedef without alternative name;
|
file |
diff |
annotate
|
| Fri, 21 Oct 2011 11:17:14 +0200 |
bulwahn |
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
| Thu, 08 Sep 2011 18:47:23 -0700 |
huffman |
remove lemmas nat_add_min_{left,right} in favor of generic lemmas min_add_distrib_{left,right}
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 23:07:16 +0200 |
haftmann |
lemmas about +, *, min, max on nat
|
file |
diff |
annotate
|
| Sat, 20 Aug 2011 01:39:27 +0200 |
haftmann |
more uniform formatting of specifications
|
file |
diff |
annotate
|
| Thu, 18 Aug 2011 13:55:26 +0200 |
haftmann |
observe distinction between sets and predicates more properly
|
file |
diff |
annotate
|
| Wed, 29 Jun 2011 18:12:34 +0200 |
wenzelm |
modernized some simproc setup;
|
file |
diff |
annotate
|
| Thu, 30 Sep 2010 08:50:45 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 11:13:15 +0200 |
nipkow |
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 |
nipkow |
expand_fun_eq -> ext_iff
|
file |
diff |
annotate
|
| Fri, 20 Aug 2010 17:46:56 +0200 |
haftmann |
more concise characterization of of_nat operation and class semiring_char_0
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 10:48:37 +0200 |
haftmann |
dropped superfluous [code del]s
|
file |
diff |
annotate
|
| Mon, 14 Jun 2010 16:00:46 +0200 |
haftmann |
added lemma funpow_mult
|
file |
diff |
annotate
|
| Tue, 08 Jun 2010 16:37:19 +0200 |
haftmann |
qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
|
file |
diff |
annotate
|
| Mon, 17 May 2010 18:59:59 -0700 |
huffman |
declare add_nonneg_nonneg [simp]; remove now-redundant lemmas realpow_two_le_order(2)
|
file |
diff |
annotate
|
| Fri, 16 Apr 2010 21:28:09 +0200 |
wenzelm |
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 12:58:52 +0100 |
blanchet |
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 07:42:46 -0800 |
huffman |
add lemmas Nats_cases and Nats_induct
|
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
|
| Thu, 18 Feb 2010 14:21:44 -0800 |
huffman |
get rid of many duplicate simp rule warnings
|
file |
diff |
annotate
|
| Fri, 12 Feb 2010 14:28:01 +0100 |
haftmann |
tuned import order
|
file |
diff |
annotate
|
| Tue, 09 Feb 2010 11:47:47 +0100 |
haftmann |
hide fact names clashing with fact names from Group.thy
|
file |
diff |
annotate
|
| Mon, 08 Feb 2010 17:12:27 +0100 |
haftmann |
hide fact Nat.add_0_right; make add_0_right from Groups priority
|
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
|
| Wed, 30 Dec 2009 01:08:33 +0100 |
krauss |
more regular axiom of infinity, with no (indirect) reference to overloaded constants
|
file |
diff |
annotate
|
| Fri, 13 Nov 2009 14:14:04 +0100 |
nipkow |
renamed lemmas "anti_sym" -> "antisym"
|
file |
diff |
annotate
|
| Fri, 30 Oct 2009 18:32:40 +0100 |
haftmann |
tuned code setup
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 17:44:03 +0100 |
haftmann |
moved lemmas for dvd on nat to theories Nat and Power
|
file |
diff |
annotate
|
| Wed, 30 Sep 2009 08:21:53 +0200 |
haftmann |
tuned whitespace
|
file |
diff |
annotate
|
| Mon, 31 Aug 2009 14:09:42 +0200 |
nipkow |
tuned the simp rules for Int involving insert and intervals.
|
file |
diff |
annotate
|
| Fri, 28 Aug 2009 19:15:59 +0200 |
nipkow |
tuned proofs
|
file |
diff |
annotate
|
| Tue, 14 Jul 2009 10:54:04 +0200 |
haftmann |
code attributes use common underscore convention
|
file |
diff |
annotate
|
| Thu, 18 Jun 2009 19:54:21 +0200 |
krauss |
generalized less_Suc_induct
|
file |
diff |
annotate
|