Thu, 02 Feb 2012 10:12:30 +0100 |
bulwahn |
adding a minimally refined equality on sets for code generation
|
file |
diff |
annotate
|
Tue, 31 Jan 2012 15:39:45 +0100 |
bulwahn |
adding code equation for setsum
|
file |
diff |
annotate
|
Mon, 23 Jan 2012 17:29:19 +0100 |
huffman |
generalize type of List.listrel
|
file |
diff |
annotate
|
Mon, 23 Jan 2012 14:07:36 +0100 |
bulwahn |
adding code generation for some list relations
|
file |
diff |
annotate
|
Tue, 10 Jan 2012 18:12:03 +0100 |
berghofe |
pred_subset/equals_eq are now standard pred_set_conv rules
|
file |
diff |
annotate
|
Sat, 07 Jan 2012 20:44:23 +0100 |
haftmann |
massaging of code setup for sets
|
file |
diff |
annotate
|
Sat, 07 Jan 2012 11:45:53 +0100 |
haftmann |
corrected slip
|
file |
diff |
annotate
|
Sat, 07 Jan 2012 09:32:01 +0100 |
haftmann |
restore convenient code_abbrev declarations (particulary important if List.set is not the formal constructor for sets)
|
file |
diff |
annotate
|
Fri, 06 Jan 2012 22:16:01 +0100 |
haftmann |
moved lemmas about List.set and set operations to List theory
|
file |
diff |
annotate
|
Fri, 06 Jan 2012 20:39:50 +0100 |
haftmann |
farewell to theory More_List
|
file |
diff |
annotate
|
Fri, 06 Jan 2012 17:44:42 +0100 |
wenzelm |
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
|
file |
diff |
annotate
|
Fri, 06 Jan 2012 10:19:49 +0100 |
haftmann |
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
|
file |
diff |
annotate
|
Thu, 05 Jan 2012 18:18:39 +0100 |
wenzelm |
improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
|
file |
diff |
annotate
|
Thu, 29 Dec 2011 13:42:21 +0100 |
haftmann |
qualified Finite_Set.fold
|
file |
diff |
annotate
|
Thu, 29 Dec 2011 10:47:55 +0100 |
haftmann |
attribute code_abbrev superseedes code_unfold_post; tuned text
|
file |
diff |
annotate
|
Tue, 27 Dec 2011 09:15:26 +0100 |
haftmann |
dropped fact whose names clash with corresponding facts on canonical fold
|
file |
diff |
annotate
|
Sat, 24 Dec 2011 15:53:10 +0100 |
haftmann |
dropped obsolete lemma member_set
|
file |
diff |
annotate
|
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
|