| Mon, 26 Mar 2012 18:54:41 +0200 |
Functions and lemmas by Christian Sternagel
|
file | diff | annotate |
| Sun, 25 Mar 2012 20:15:39 +0200 |
merged fork with new numeral representation (see NEWS)
|
file | diff | annotate |
| Tue, 13 Mar 2012 13:31:26 +0100 |
tuned proofs -- eliminated pointless chaining of facts after 'interpret';
|
file | diff | annotate |
| Mon, 12 Mar 2012 21:41:11 +0100 |
tuned proofs
|
file | diff | annotate |
| Mon, 27 Feb 2012 09:01:49 +0100 |
converting "set [...]" to "{...}" in evaluation results
|
file | diff | annotate |
| Sat, 25 Feb 2012 09:07:37 +0100 |
one general list_all2_update_cong instead of two special ones
|
file | diff | annotate |
| Fri, 24 Feb 2012 22:46:44 +0100 |
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
|
file | diff | annotate |
| Fri, 24 Feb 2012 09:40:02 +0100 |
given up disfruitful branch
|
file | diff | annotate |
| Thu, 23 Feb 2012 21:25:59 +0100 |
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
|
file | diff | annotate |
| Thu, 16 Feb 2012 09:18:23 +0100 |
removing unnecessary premises in theorems of List theory
|
file | diff | annotate |
| Fri, 10 Feb 2012 09:47:59 +0100 |
more specification of the quotient package in IsarRef
|
file | diff | annotate |
| Wed, 08 Feb 2012 01:49:33 +0100 |
use 'primrec' to define "rotate1", for uniformity (and to help first-order tools that rely on "Spec_Rules")
|
file | diff | annotate |
| Wed, 08 Feb 2012 00:55:06 +0100 |
removed fact that confuses SPASS -- better rely on "rev_rev_ident", which is stronger and more ATP friendly
|
file | diff | annotate |
| Sun, 05 Feb 2012 10:43:52 +0100 |
adding code equation for Relation.image; adding map_project as correspondence to map_filter on lists
|
file | diff | annotate |
| Sun, 05 Feb 2012 08:24:39 +0100 |
another try to improve code generation of set equality (cf. da32cf32c0c7)
|
file | diff | annotate |
| Thu, 02 Feb 2012 10:12:30 +0100 |
adding a minimally refined equality on sets for code generation
|
file | diff | annotate |
| Tue, 31 Jan 2012 15:39:45 +0100 |
adding code equation for setsum
|
file | diff | annotate |
| Mon, 23 Jan 2012 17:29:19 +0100 |
generalize type of List.listrel
|
file | diff | annotate |
| Mon, 23 Jan 2012 14:07:36 +0100 |
adding code generation for some list relations
|
file | diff | annotate |
| Tue, 10 Jan 2012 18:12:03 +0100 |
pred_subset/equals_eq are now standard pred_set_conv rules
|
file | diff | annotate |
| Sat, 07 Jan 2012 20:44:23 +0100 |
massaging of code setup for sets
|
file | diff | annotate |
| Sat, 07 Jan 2012 11:45:53 +0100 |
corrected slip
|
file | diff | annotate |
| Sat, 07 Jan 2012 09:32:01 +0100 |
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 |
moved lemmas about List.set and set operations to List theory
|
file | diff | annotate |
| Fri, 06 Jan 2012 20:39:50 +0100 |
farewell to theory More_List
|
file | diff | annotate |
| Fri, 06 Jan 2012 17:44:42 +0100 |
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 |
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 |
improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
|
file | diff | annotate |
| Thu, 29 Dec 2011 13:42:21 +0100 |
qualified Finite_Set.fold
|
file | diff | annotate |
| Thu, 29 Dec 2011 10:47:55 +0100 |
attribute code_abbrev superseedes code_unfold_post; tuned text
|
file | diff | annotate |
| Tue, 27 Dec 2011 09:15:26 +0100 |
dropped fact whose names clash with corresponding facts on canonical fold
|
file | diff | annotate |
| Sat, 24 Dec 2011 15:53:10 +0100 |
dropped obsolete lemma member_set
|
file | diff | annotate |
| Mon, 19 Dec 2011 14:41:08 +0100 |
add lemmas
|
file | diff | annotate |
| Thu, 15 Dec 2011 18:08:40 +0100 |
clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
|
file | diff | annotate |
| Tue, 13 Dec 2011 22:44:16 +0100 |
added lemmas
|
file | diff | annotate |
| Fri, 09 Dec 2011 13:42:16 +0100 |
add induction rule for list_all2
|
file | diff | annotate |
| Thu, 08 Dec 2011 13:53:27 +0100 |
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 |
cardinality of sets of lists
|
file | diff | annotate |
| Sun, 20 Nov 2011 21:07:10 +0100 |
eliminated obsolete "standard";
|
file | diff | annotate |
| Wed, 19 Oct 2011 08:37:27 +0200 |
removing old code generator setup for lists
|
file | diff | annotate |
| Mon, 03 Oct 2011 14:43:12 +0200 |
adding lemma to List library for executable equation of the (refl) transitive closure
|
file | diff | annotate |
| Wed, 14 Sep 2011 10:08:52 -0400 |
renamed Complete_Lattices lemmas, removed legacy names
|
file | diff | annotate |
| Tue, 13 Sep 2011 17:07:33 -0700 |
tuned proofs
|
file | diff | annotate |
| Tue, 13 Sep 2011 12:14:29 +0200 |
added lemma motivated by a more specific lemma in the AFP-KBPs theories
|
file | diff | annotate |
| Mon, 12 Sep 2011 07:55:43 +0200 |
new fastforce replacing fastsimp - less confusing name
|
file | diff | annotate |
| Thu, 01 Sep 2011 13:18:27 +0200 |
added two lemmas about "distinct" to help Sledgehammer
|
file | diff | annotate |
| Tue, 30 Aug 2011 20:10:48 +0200 |
adding list_size_append (thanks to Rene Thiemann)
|
file | diff | annotate |
| Tue, 30 Aug 2011 20:10:47 +0200 |
strengthening list_size_pointwise (thanks to Rene Thiemann)
|
file | diff | annotate |
| Fri, 26 Aug 2011 11:22:47 +0200 |
added lemma
|
file | diff | annotate |
| Tue, 02 Aug 2011 10:36:50 +0200 |
moved recdef package to HOL/Library/Old_Recdef.thy
|
file | diff | annotate |
| Wed, 29 Jun 2011 17:35:46 +0200 |
modernized some simproc setup;
|
file | diff | annotate |
| Mon, 27 Jun 2011 17:04:04 +0200 |
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 |
discontinued Name.variant to emphasize that this is old-style / indirect;
|
file | diff | annotate |
| Fri, 20 May 2011 11:44:16 +0200 |
names of fold_set locales resemble name of characteristic property more closely
|
file | diff | annotate |
| Sat, 14 May 2011 18:26:25 +0200 |
use pointfree characterisation for fold_set locale
|
file | diff | annotate |
| Mon, 09 May 2011 16:11:20 +0200 |
add a lemma about commutative append to List.thy
|
file | diff | annotate |
| Mon, 09 May 2011 12:26:25 +0200 |
removed assumption from lemma List.take_add
|
file | diff | annotate |
| Tue, 19 Apr 2011 23:57:28 +0200 |
eliminated Codegen.mode in favour of explicit argument;
|
file | diff | annotate |
| Sat, 16 Apr 2011 16:15:37 +0200 |
modernized structure Proof_Context;
|
file | diff | annotate |
| Sat, 16 Apr 2011 15:25:25 +0200 |
prefer local name spaces;
|
file | diff | annotate |