| Mon, 19 Dec 2011 14:41:08 +0100 |
noschinl |
add lemmas
|
file |
diff |
annotate
|
| Thu, 15 Dec 2011 18:08:40 +0100 |
wenzelm |
clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
|
file |
diff |
annotate
|
| Tue, 13 Dec 2011 22:44:16 +0100 |
noschinl |
added lemmas
|
file |
diff |
annotate
|
| Fri, 09 Dec 2011 13:42:16 +0100 |
huffman |
add induction rule for list_all2
|
file |
diff |
annotate
|
| Thu, 08 Dec 2011 13:53:27 +0100 |
bulwahn |
removing special code generator setup for hd and last function because this causes problems with quickcheck narrowing as the Haskell Prelude functions throw errors that cannot be caught instead of PatternFail exceptions
|
file |
diff |
annotate
|
| Thu, 01 Dec 2011 15:41:58 +0100 |
hoelzl |
cardinality of sets of lists
|
file |
diff |
annotate
|
| Sun, 20 Nov 2011 21:07:10 +0100 |
wenzelm |
eliminated obsolete "standard";
|
file |
diff |
annotate
|
| Wed, 19 Oct 2011 08:37:27 +0200 |
bulwahn |
removing old code generator setup for lists
|
file |
diff |
annotate
|
| Mon, 03 Oct 2011 14:43:12 +0200 |
bulwahn |
adding lemma to List library for executable equation of the (refl) transitive closure
|
file |
diff |
annotate
|
| Wed, 14 Sep 2011 10:08:52 -0400 |
hoelzl |
renamed Complete_Lattices lemmas, removed legacy names
|
file |
diff |
annotate
|
| Tue, 13 Sep 2011 17:07:33 -0700 |
huffman |
tuned proofs
|
file |
diff |
annotate
|
| Tue, 13 Sep 2011 12:14:29 +0200 |
bulwahn |
added lemma motivated by a more specific lemma in the AFP-KBPs theories
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
| Thu, 01 Sep 2011 13:18:27 +0200 |
blanchet |
added two lemmas about "distinct" to help Sledgehammer
|
file |
diff |
annotate
|
| Tue, 30 Aug 2011 20:10:48 +0200 |
bulwahn |
adding list_size_append (thanks to Rene Thiemann)
|
file |
diff |
annotate
|
| Tue, 30 Aug 2011 20:10:47 +0200 |
bulwahn |
strengthening list_size_pointwise (thanks to Rene Thiemann)
|
file |
diff |
annotate
|
| Fri, 26 Aug 2011 11:22:47 +0200 |
nipkow |
added lemma
|
file |
diff |
annotate
|
| Tue, 02 Aug 2011 10:36:50 +0200 |
krauss |
moved recdef package to HOL/Library/Old_Recdef.thy
|
file |
diff |
annotate
|
| Wed, 29 Jun 2011 17:35:46 +0200 |
wenzelm |
modernized some simproc setup;
|
file |
diff |
annotate
|
| Mon, 27 Jun 2011 17:04:04 +0200 |
krauss |
new Datatype.info_of_constr with strict behaviour wrt. to overloaded constructors -- side effect: function package correctly identifies 0::int as a non-constructor;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 16:34:49 +0200 |
wenzelm |
discontinued Name.variant to emphasize that this is old-style / indirect;
|
file |
diff |
annotate
|
| Fri, 20 May 2011 11:44:16 +0200 |
haftmann |
names of fold_set locales resemble name of characteristic property more closely
|
file |
diff |
annotate
|
| Sat, 14 May 2011 18:26:25 +0200 |
haftmann |
use pointfree characterisation for fold_set locale
|
file |
diff |
annotate
|
| Mon, 09 May 2011 16:11:20 +0200 |
noschinl |
add a lemma about commutative append to List.thy
|
file |
diff |
annotate
|
| Mon, 09 May 2011 12:26:25 +0200 |
noschinl |
removed assumption from lemma List.take_add
|
file |
diff |
annotate
|
| Tue, 19 Apr 2011 23:57:28 +0200 |
wenzelm |
eliminated Codegen.mode in favour of explicit argument;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 15:25:25 +0200 |
wenzelm |
prefer local name spaces;
|
file |
diff |
annotate
|
| Wed, 06 Apr 2011 23:04:00 +0200 |
wenzelm |
separate structure Term_Position;
|
file |
diff |
annotate
|
| Wed, 30 Mar 2011 20:19:21 +0200 |
wenzelm |
actually check list comprehension examples;
|
file |
diff |
annotate
|
| Mon, 28 Mar 2011 23:49:53 +0200 |
wenzelm |
list comprehension: strip positions where the translation cannot handle them right now;
|
file |
diff |
annotate
|
| Tue, 22 Mar 2011 20:44:47 +0100 |
wenzelm |
more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
|
file |
diff |
annotate
|
| Tue, 15 Mar 2011 22:04:02 +0100 |
nipkow |
added lemma
|
file |
diff |
annotate
|
| Fri, 25 Feb 2011 14:25:41 +0100 |
nipkow |
added simp lemma nth_Cons_pos to List
|
file |
diff |
annotate
|
| Thu, 03 Feb 2011 18:57:42 +0100 |
wenzelm |
explicit is better than implicit;
|
file |
diff |
annotate
|
| Tue, 11 Jan 2011 14:12:37 +0100 |
haftmann |
"enriched_type" replaces less specific "type_lifting"
|
file |
diff |
annotate
|
| Fri, 07 Jan 2011 18:10:35 +0100 |
bulwahn |
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
|
file |
diff |
annotate
|
| Tue, 21 Dec 2010 17:52:23 +0100 |
haftmann |
tuned type_lifting declarations
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 17:43:54 +0100 |
wenzelm |
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
|
file |
diff |
annotate
|
| Wed, 08 Dec 2010 13:34:50 +0100 |
haftmann |
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 09:19:10 +0100 |
haftmann |
replace `type_mapper` by the more adequate `type_lifting`
|
file |
diff |
annotate
|
| Sun, 28 Nov 2010 15:20:51 +0100 |
nipkow |
gave more standard finite set rules simp and intro attribute
|
file |
diff |
annotate
|
| Mon, 22 Nov 2010 11:34:58 +0100 |
bulwahn |
adding code equations for EX1 on finite types
|
file |
diff |
annotate
|
| Thu, 18 Nov 2010 17:01:16 +0100 |
haftmann |
mapper for list type; map_pair replaces prod_fun
|
file |
diff |
annotate
|
| Wed, 17 Nov 2010 21:35:23 +0100 |
nipkow |
code eqn for slice was missing; redefined splice with fun
|
file |
diff |
annotate
|
| Fri, 05 Nov 2010 08:16:34 +0100 |
bulwahn |
added two lemmas about injectivity of concat to the list theory
|
file |
diff |
annotate
|
| Tue, 02 Nov 2010 16:31:57 +0100 |
haftmann |
lemmas sorted_map_same, sorted_same
|
file |
diff |
annotate
|
| Thu, 28 Oct 2010 17:54:09 +0200 |
nipkow |
added lemmas about listrel(1)
|
file |
diff |
annotate
|
| Wed, 27 Oct 2010 16:40:31 +0200 |
haftmann |
sorting: avoid _key suffix if lemma applies both to simple and generalized variant; generalized insort_insert to insort_insert_key; additional lemmas
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 16:39:21 +0200 |
haftmann |
include ATP in theory List -- avoid theory edge by-passing the prominent list theory
|
file |
diff |
annotate
|
| Mon, 25 Oct 2010 13:34:58 +0200 |
haftmann |
dropped (almost) redundant distinct.induct rule; distinct_simps again named distinct.simps
|
file |
diff |
annotate
|
| Sun, 24 Oct 2010 20:19:00 +0200 |
nipkow |
nat_number -> eval_nat_numeral
|
file |
diff |
annotate
|
| Wed, 06 Oct 2010 17:44:21 +0200 |
blanchet |
merged
|
file |
diff |
annotate
|
| Mon, 04 Oct 2010 22:45:09 +0200 |
blanchet |
move Metis into Plain
|
file |
diff |
annotate
|
| Mon, 04 Oct 2010 12:22:58 +0200 |
haftmann |
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
|
file |
diff |
annotate
|
| Tue, 28 Sep 2010 15:21:45 +0200 |
haftmann |
localized listsum
|
file |
diff |
annotate
|
| Mon, 27 Sep 2010 14:13:22 +0200 |
haftmann |
lemma remdups_map_remdups
|
file |
diff |
annotate
|
| Wed, 22 Sep 2010 16:52:09 +0200 |
nipkow |
more lists lemmas
|
file |
diff |
annotate
|
| Tue, 21 Sep 2010 02:03:40 +0200 |
nipkow |
new lemma
|
file |
diff |
annotate
|
| Fri, 17 Sep 2010 20:53:50 +0200 |
haftmann |
generalized lemma insort_remove1 to insort_key_remove1
|
file |
diff |
annotate
|