| Sun, 31 Aug 2014 09:10:42 +0200 |
haftmann |
separated listsum material
|
file |
diff |
annotate
|
| Mon, 25 Aug 2014 16:06:41 +0200 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
| Thu, 07 Aug 2014 12:17:41 +0200 |
blanchet |
no need for 'set_simps' now that 'datatype_new' generates the desired 'set' property
|
file |
diff |
annotate
|
| Mon, 21 Jul 2014 17:51:29 +0200 |
Andreas Lochbihler |
add parametricity lemmas
|
file |
diff |
annotate
|
| Sat, 19 Jul 2014 18:30:43 +0200 |
haftmann |
reverse induction over nonempty lists
|
file |
diff |
annotate
|
| Wed, 09 Jul 2014 11:48:21 +0200 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
| Sat, 05 Jul 2014 11:01:53 +0200 |
haftmann |
prefer ac_simps collections over separate name bindings for add and mult
|
file |
diff |
annotate
|
| Fri, 04 Jul 2014 20:18:47 +0200 |
haftmann |
reduced name variants for assoc and commute on plus and mult
|
file |
diff |
annotate
|
| Sat, 28 Jun 2014 09:16:42 +0200 |
haftmann |
fact consolidation
|
file |
diff |
annotate
|
| Tue, 24 Jun 2014 15:05:58 +0200 |
Andreas Lochbihler |
add lemma
|
file |
diff |
annotate
|
| Thu, 12 Jun 2014 18:47:27 +0200 |
nipkow |
merged
|
file |
diff |
annotate
|
| Thu, 12 Jun 2014 18:47:16 +0200 |
nipkow |
added [simp]
|
file |
diff |
annotate
|
| Thu, 12 Jun 2014 17:02:03 +0200 |
blanchet |
reintroduced vital 'Thm.transfer'
|
file |
diff |
annotate
|
| Thu, 12 Jun 2014 01:00:49 +0200 |
blanchet |
reduces Sledgehammer dependencies
|
file |
diff |
annotate
|
| Tue, 10 Jun 2014 21:15:57 +0200 |
blanchet |
changed syntax of map: and rel: arguments to BNF-based datatypes
|
file |
diff |
annotate
|
| Tue, 10 Jun 2014 12:16:22 +0200 |
blanchet |
use 'where' clause for selector default value syntax
|
file |
diff |
annotate
|
| Mon, 09 Jun 2014 16:08:30 +0200 |
nipkow |
added List.union
|
file |
diff |
annotate
|
| Fri, 30 May 2014 12:27:51 +0200 |
blanchet |
tuned whitespace, to make datatype definitions slightly less intimidating
|
file |
diff |
annotate
|
| Mon, 26 May 2014 16:32:55 +0200 |
blanchet |
got rid of '=:' squiggly
|
file |
diff |
annotate
|
| Wed, 14 May 2014 11:33:38 +0200 |
nipkow |
added lemma
|
file |
diff |
annotate
|
| Tue, 29 Apr 2014 16:02:02 +0200 |
wenzelm |
prefer plain ASCII / latex over not-so-universal Unicode;
|
file |
diff |
annotate
|
| Wed, 23 Apr 2014 10:23:27 +0200 |
blanchet |
move size hooks together, with new one preceding old one and sharing same theory data
|
file |
diff |
annotate
|
| Sat, 12 Apr 2014 11:27:36 +0200 |
haftmann |
more operations and lemmas
|
file |
diff |
annotate
|
| Thu, 10 Apr 2014 17:48:54 +0200 |
kuncar |
make list_all an abbreviation of pred_list - prevent duplication
|
file |
diff |
annotate
|
| Thu, 10 Apr 2014 17:48:32 +0200 |
kuncar |
simplify and fix theories thanks to 356a5efdb278
|
file |
diff |
annotate
|
| Thu, 10 Apr 2014 17:48:15 +0200 |
kuncar |
abstract Domainp in relator_domain rules => more natural statement of the rule
|
file |
diff |
annotate
|
| Thu, 10 Apr 2014 17:48:15 +0200 |
kuncar |
more appropriate name (Lifting.invariant -> eq_onp)
|
file |
diff |
annotate
|
| Thu, 10 Apr 2014 17:48:14 +0200 |
kuncar |
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 11:42:32 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Wed, 19 Mar 2014 18:47:22 +0100 |
haftmann |
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
|
file |
diff |
annotate
|
| Sun, 16 Mar 2014 18:09:04 +0100 |
haftmann |
normalising simp rules for compound operators
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 13:18:13 +0100 |
blanchet |
killed a few 'metis' calls
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 15:40:33 +0100 |
blanchet |
renamed 'fun_rel' to 'rel_fun'
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 15:29:18 +0100 |
blanchet |
renamed 'prod_rel' to 'rel_prod'
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 14:57:14 +0100 |
blanchet |
renamed 'set_rel' to 'rel_set'
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 13:36:48 +0100 |
blanchet |
renamed 'map_pair' to 'map_prod'
|
file |
diff |
annotate
|
| Fri, 28 Feb 2014 17:54:52 +0100 |
traytel |
load Metis a little later
|
file |
diff |
annotate
|
| Fri, 28 Feb 2014 18:09:37 +0100 |
nipkow |
added function "List.extract"
|
file |
diff |
annotate
|
| Fri, 21 Feb 2014 00:09:56 +0100 |
blanchet |
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
|
file |
diff |
annotate
|
| Wed, 19 Feb 2014 16:32:37 +0100 |
blanchet |
merged 'List.set' with BNF-generated 'set'
|
file |
diff |
annotate
|
| Tue, 18 Feb 2014 23:03:49 +0100 |
kuncar |
delete or move now not necessary reflexivity rules due to 1726f46d2aa8
|
file |
diff |
annotate
|
| Mon, 17 Feb 2014 13:31:42 +0100 |
blanchet |
renamed 'datatype_new_compat' to 'datatype_compat'
|
file |
diff |
annotate
|
| Sun, 16 Feb 2014 21:33:28 +0100 |
blanchet |
folded 'rel_option' into 'option_rel'
|
file |
diff |
annotate
|
| Sun, 16 Feb 2014 21:33:28 +0100 |
blanchet |
folded 'list_all2' with the relator generated by 'datatype_new'
|
file |
diff |
annotate
|
| Fri, 14 Feb 2014 07:53:46 +0100 |
blanchet |
hide 'rel' name -- this one is waiting to be merged with 'list_all2'
|
file |
diff |
annotate
|
| Fri, 14 Feb 2014 07:53:46 +0100 |
blanchet |
renamed 'enriched_type' to more informative 'functor' (following the renaming of enriched type constructors to bounded natural functors)
|
file |
diff |
annotate
|
| Fri, 14 Feb 2014 07:53:46 +0100 |
blanchet |
merged 'Option.map' and 'Option.map_option'
|
file |
diff |
annotate
|
| Fri, 14 Feb 2014 07:53:45 +0100 |
blanchet |
merged 'List.map' and 'List.list.map'
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 17:35:59 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:37:06 +0100 |
blanchet |
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
renamed 'nat_{case,rec}' to '{case,rec}_nat'
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
compatibility names
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
use new selector support to define 'the', 'hd', 'tl'
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
transformed 'option' and 'list' into new-style datatypes (but register them as old-style as well)
|
file |
diff |
annotate
|
| Sat, 25 Jan 2014 23:50:49 +0100 |
haftmann |
avoid (now superfluous) indirect passing of constant names
|
file |
diff |
annotate
|
| Sat, 25 Jan 2014 23:50:49 +0100 |
haftmann |
prefer explicit code symbol type over ad-hoc name mangling
|
file |
diff |
annotate
|
| Fri, 24 Jan 2014 11:51:45 +0100 |
blanchet |
killed 'More_BNFs' by moving its various bits where they (now) belong
|
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
|
| Tue, 31 Dec 2013 22:18:31 +0100 |
haftmann |
more abstract declaration of code attributes
|
file |
diff |
annotate
|
| Fri, 27 Dec 2013 14:35:14 +0100 |
haftmann |
prefer target-style syntaxx for sublocale
|
file |
diff |
annotate
|
| Wed, 25 Dec 2013 17:39:06 +0100 |
haftmann |
prefer more canonical names for lemmas on min/max
|
file |
diff |
annotate
|
| Wed, 27 Nov 2013 11:08:55 +0100 |
Andreas Lochbihler |
remove junk
|
file |
diff |
annotate
|
| Wed, 27 Nov 2013 10:43:51 +0100 |
Andreas Lochbihler |
merged
|
file |
diff |
annotate
|
| Wed, 20 Nov 2013 10:59:12 +0100 |
Andreas Lochbihler |
add predicate version of lexicographic order on lists
|
file |
diff |
annotate
|
| Thu, 21 Nov 2013 21:33:34 +0100 |
blanchet |
rationalize imports
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 17:07:52 +0100 |
hoelzl |
merged
|
file |
diff |
annotate
|
| Mon, 18 Nov 2013 17:14:01 +0100 |
hoelzl |
add lemmas Suc_funpow and id_funpow to simpset; add lemma map_add_upt
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 10:05:53 +0100 |
haftmann |
eliminiated neg_numeral in favour of - (numeral _)
|
file |
diff |
annotate
|
| Tue, 12 Nov 2013 13:47:24 +0100 |
blanchet |
port list comprehension simproc to 'Ctr_Sugar' abstraction
|
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:20 +0200 |
blanchet |
killed most "no_atp", to make Sledgehammer more complete
|
file |
diff |
annotate
|
| Fri, 27 Sep 2013 15:38:23 +0200 |
nipkow |
added code eqns for bounded LEAST operator
|
file |
diff |
annotate
|
| Thu, 26 Sep 2013 13:37:33 +0200 |
lammich |
Added symmetric code_unfold-lemmas for null and is_none
|
file |
diff |
annotate
|
| Wed, 18 Sep 2013 18:11:32 +0200 |
traytel |
added two functions to List (one contributed by Manuel Eberl)
|
file |
diff |
annotate
|
| Wed, 18 Sep 2013 12:16:10 +0200 |
nipkow |
added and tuned lemmas
|
file |
diff |
annotate
|
| Thu, 05 Sep 2013 11:10:51 +0200 |
traytel |
list_to_set_comprehension: don't crash in case distinctions on datatypes with even number of constructors
|
file |
diff |
annotate
|
| Tue, 03 Sep 2013 01:12:40 +0200 |
wenzelm |
tuned proofs -- clarified flow of facts wrt. calculation;
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 17:45:22 +0200 |
wenzelm |
merged
|
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
|
| Tue, 13 Aug 2013 15:59:22 +0200 |
kuncar |
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
|
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
|
| Sat, 15 Jun 2013 17:19:23 +0200 |
haftmann |
lifting for primitive definitions;
|
file |
diff |
annotate
|
| Sat, 15 Jun 2013 17:19:23 +0200 |
haftmann |
selection operator smallest_prime_beyond
|
file |
diff |
annotate
|
| Sat, 25 May 2013 18:30:38 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Sat, 25 May 2013 15:37:53 +0200 |
wenzelm |
syntax translations always depend on context;
|
file |
diff |
annotate
|
| Sat, 25 May 2013 15:44:29 +0200 |
haftmann |
weaker precendence of syntax for big intersection and union on sets
|
file |
diff |
annotate
|
| Fri, 24 May 2013 17:00:46 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 23 May 2013 14:22:49 +0200 |
noschinl |
more lemmas for sorted_list_of_set
|
file |
diff |
annotate
|
| Mon, 06 May 2013 02:48:18 +0200 |
nipkow |
tail recursive version of map, for code generation, optionally
|
file |
diff |
annotate
|
| Tue, 23 Apr 2013 11:14:51 +0200 |
haftmann |
tuned: unnamed contexts, interpretation and sublocale in locale target;
|
file |
diff |
annotate
|
| Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| Fri, 05 Apr 2013 22:08:42 +0200 |
traytel |
allow redundant cases in the list comprehension translation
|
file |
diff |
annotate
|
| Tue, 22 Jan 2013 14:33:45 +0100 |
traytel |
separate data used for case translation from the datatype package
|
file |
diff |
annotate
|
| Tue, 22 Jan 2013 13:32:41 +0100 |
berghofe |
case translations performed in a separate check phase (with adjustments by traytel)
|
file |
diff |
annotate
|
| Wed, 27 Mar 2013 10:55:05 +0100 |
haftmann |
centralized various multiset operations in theory multiset;
|
file |
diff |
annotate
|
| Tue, 26 Mar 2013 20:49:57 +0100 |
haftmann |
explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts
|
file |
diff |
annotate
|
| Sat, 23 Mar 2013 20:50:39 +0100 |
haftmann |
fundamental revision of big operators on sets
|
file |
diff |
annotate
|
| Thu, 28 Feb 2013 17:14:55 +0100 |
wenzelm |
provide common HOLogic.conj_conv and HOLogic.eq_conv;
|
file |
diff |
annotate
|
| Thu, 28 Feb 2013 16:54:52 +0100 |
wenzelm |
just one HOLogic.Trueprop_conv, with regular exception CTERM;
|
file |
diff |
annotate
|
| Mon, 25 Feb 2013 12:17:50 +0100 |
wenzelm |
prefer stateless 'ML_val' for tests;
|
file |
diff |
annotate
|
| Sun, 17 Feb 2013 21:29:30 +0100 |
haftmann |
Sieve of Eratosthenes
|
file |
diff |
annotate
|
| Sun, 17 Feb 2013 11:34:40 +0100 |
haftmann |
simplified construction of upto_aux
|
file |
diff |
annotate
|
| Sat, 16 Feb 2013 15:27:10 +0100 |
nipkow |
tail recursive code for function "upto"
|
file |
diff |
annotate
|
| Fri, 15 Feb 2013 11:47:33 +0100 |
haftmann |
systematic conversions between nat and nibble/char;
|
file |
diff |
annotate
|
| Thu, 14 Feb 2013 12:24:42 +0100 |
haftmann |
abandoned theory Plain
|
file |
diff |
annotate
|
| Wed, 13 Feb 2013 13:38:52 +0100 |
haftmann |
combinator List.those;
|
file |
diff |
annotate
|
| Fri, 14 Dec 2012 19:51:20 +0100 |
nipkow |
unified layout of defs
|
file |
diff |
annotate
|
| Fri, 07 Dec 2012 16:25:33 +0100 |
wenzelm |
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time) -- relevant for any application using it, e.g. small paper sessions;
|
file |
diff |
annotate
|
| Tue, 20 Nov 2012 18:59:35 +0100 |
hoelzl |
add Countable_Set theory
|
file |
diff |
annotate
|
| Thu, 08 Nov 2012 11:59:48 +0100 |
bulwahn |
adjusting proofs as the set_comprehension_pointfree simproc breaks some existing proofs
|
file |
diff |
annotate
|
| Sun, 21 Oct 2012 17:04:13 +0200 |
webertj |
merged
|
file |
diff |
annotate
|
| Fri, 19 Oct 2012 15:12:52 +0200 |
webertj |
Renamed {left,right}_distrib to distrib_{right,left}.
|
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
|
| Wed, 10 Oct 2012 15:16:44 +0200 |
Andreas Lochbihler |
tail-recursive implementation for length
|
file |
diff |
annotate
|
| Tue, 09 Oct 2012 16:57:58 +0200 |
kuncar |
rename Set.project to Set.filter - more appropriate name
|
file |
diff |
annotate
|
| Mon, 08 Oct 2012 12:03:49 +0200 |
haftmann |
consolidated names of theorems on composition;
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 22:55:41 +0200 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
| Thu, 16 Aug 2012 14:07:32 +0200 |
haftmann |
prefer eta-expanded code equations for fold, to accomodate tail recursion optimisation in Scala
|
file |
diff |
annotate
|
| Tue, 31 Jul 2012 13:55:39 +0200 |
kuncar |
more set operations expressed by Finite_Set.fold
|
file |
diff |
annotate
|
| Mon, 30 Apr 2012 12:14:53 +0200 |
bulwahn |
making sorted_list_of_set executable
|
file |
diff |
annotate
|