| Thu, 19 Aug 2021 12:31:06 +0200 |
Lukas Stevens |
add/rename some theorems about Map(pings)
|
file |
diff |
annotate
|
| Tue, 01 Jun 2021 19:46:34 +0200 |
nipkow |
More general fold function for maps
|
file |
diff |
annotate
|
| Sun, 29 Mar 2020 15:44:54 +0100 |
paulson |
more tidying up of old apply-proofs
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Sun, 17 Jun 2018 20:31:51 +0200 |
nipkow |
added simp rules
|
file |
diff |
annotate
|
| Sat, 16 Jun 2018 07:13:17 +0200 |
nipkow |
moved lemmas from AFP
|
file |
diff |
annotate
|
| Fri, 15 Jun 2018 10:45:12 +0200 |
nipkow |
Map.empty now qualified to avoid name clashes
|
file |
diff |
annotate
|
| Wed, 07 Mar 2018 19:02:22 +0100 |
wenzelm |
more abbrevs -- this makes "(=" ambiguous and thus simplifies input of "(=)" (within the context of Main HOL);
|
file |
diff |
annotate
|
| Sun, 26 Nov 2017 21:08:32 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Sat, 11 Nov 2017 18:41:08 +0000 |
haftmann |
dedicated definition for coprimality
|
file |
diff |
annotate
|
| Fri, 01 Sep 2017 09:45:56 +0200 |
bulwahn |
more facts on Map.map_of and List.zip
|
file |
diff |
annotate
|
| Sun, 27 Aug 2017 06:56:29 +0200 |
bulwahn |
more facts on Map.ran
|
file |
diff |
annotate
|
| Mon, 05 Jun 2017 15:59:41 +0200 |
haftmann |
executable domain membership checks
|
file |
diff |
annotate
|
| Sun, 11 Sep 2016 00:14:44 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Fri, 09 Sep 2016 13:39:21 +0200 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
| Wed, 10 Aug 2016 09:33:54 +0200 |
nipkow |
"split add" -> "split"
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 16:25:08 +0100 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 21:47:32 +0100 |
wenzelm |
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
|
file |
diff |
annotate
|
| Mon, 07 Dec 2015 10:38:04 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Mon, 31 Aug 2015 21:01:21 +0200 |
wenzelm |
prefer symbols;
|
file |
diff |
annotate
|
| Thu, 27 Aug 2015 21:19:48 +0200 |
haftmann |
standardized some occurences of ancient "split" alias
|
file |
diff |
annotate
|
| Tue, 04 Aug 2015 23:11:16 +0200 |
wenzelm |
eliminated clone;
|
file |
diff |
annotate
|
| Tue, 04 Aug 2015 14:29:45 +0200 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Tue, 04 Aug 2015 14:06:24 +0200 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 22:58:50 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Tue, 14 Apr 2015 11:32:01 +0200 |
Andreas Lochbihler |
add lemmas
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Sat, 12 Apr 2014 11:27:36 +0200 |
haftmann |
more operations and lemmas
|
file |
diff |
annotate
|
| Fri, 14 Feb 2014 07:53:46 +0100 |
blanchet |
merged 'Option.map' and 'Option.map_option'
|
file |
diff |
annotate
|
| Tue, 24 Sep 2013 13:35:27 +0200 |
nipkow |
added lemmas
|
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 16:25:47 +0200 |
wenzelm |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
file |
diff |
annotate
|
| Wed, 22 Feb 2012 12:30:01 +0100 |
bulwahn |
removing some unnecessary premises from Map theory
|
file |
diff |
annotate
|
| Tue, 13 Sep 2011 17:07:33 -0700 |
huffman |
tuned proofs
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
| Wed, 30 Mar 2011 11:32:52 +0200 |
bulwahn |
renewing specifications in HOL: replacing types by type_synonym
|
file |
diff |
annotate
|
| Fri, 14 Jan 2011 15:44:47 +0100 |
wenzelm |
eliminated global prems;
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 17:43:54 +0100 |
wenzelm |
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
|
file |
diff |
annotate
|
| Sun, 10 Oct 2010 22:50:25 +0200 |
krauss |
removed output syntax "'a ~=> 'b" for "'a => 'b option"
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 16:43:23 +0200 |
haftmann |
moved lemmas map_of_eqI and map_of_eq_dom to Map.thy
|
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
|
| Sat, 06 Mar 2010 15:31:31 +0100 |
haftmann |
lemma restrict_complement_singleton_eq
|
file |
diff |
annotate
|
| Sat, 06 Mar 2010 09:58:30 +0100 |
haftmann |
added dom_option_map, map_of_map_keys
|
file |
diff |
annotate
|
| Thu, 04 Mar 2010 11:22:06 +0100 |
haftmann |
lemmas set_map_of_compr, map_of_inject_set
|
file |
diff |
annotate
|
| Wed, 03 Mar 2010 20:45:48 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Wed, 03 Mar 2010 20:45:31 +0100 |
haftmann |
more uniform naming conventions
|
file |
diff |
annotate
|
| Tue, 02 Mar 2010 23:59:54 +0100 |
wenzelm |
proper (type_)notation;
|
file |
diff |
annotate
|
| Wed, 17 Feb 2010 09:48:53 +0100 |
haftmann |
added lemma map_of_map_restrict; generalized lemma dom_const
|
file |
diff |
annotate
|
| Thu, 11 Feb 2010 23:00:22 +0100 |
wenzelm |
modernized translations;
|
file |
diff |
annotate
|
| Sun, 31 Jan 2010 14:51:32 +0100 |
haftmann |
more correspondence lemmas between related operations
|
file |
diff |
annotate
|
| Sat, 16 Jan 2010 17:15:28 +0100 |
haftmann |
dropped some old primrecs and some constdefs
|
file |
diff |
annotate
|
| Thu, 12 Nov 2009 15:10:24 +0100 |
haftmann |
moved lemma map_of_zip_map to Map.thy
|
file |
diff |
annotate
|
| Mon, 27 Jul 2009 22:50:01 +0200 |
krauss |
some lemmas about maps (contributed by Peter Lammich)
|
file |
diff |
annotate
|
| Tue, 02 Jun 2009 16:23:43 +0200 |
haftmann |
added/moved lemmas by Andreas Lochbihler
|
file |
diff |
annotate
|
| Sat, 09 May 2009 07:25:22 +0200 |
nipkow |
lemmas by Andreas Lochbihler
|
file |
diff |
annotate
|
| Thu, 16 Apr 2009 14:02:12 +0200 |
haftmann |
dropped unnamed infix
|
file |
diff |
annotate
|
| Fri, 27 Mar 2009 10:05:11 +0100 |
haftmann |
normalized imports
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 10:47:20 +0100 |
nipkow |
Made Option a separate theory and renamed option_map to Option.map
|
file |
diff |
annotate
|
| Fri, 23 Jan 2009 19:51:48 +0100 |
haftmann |
lemmas dom_const, dom_if
|
file |
diff |
annotate
|
| Fri, 14 Nov 2008 08:50:08 +0100 |
haftmann |
lemmas about dom and minus / insert
|
file |
diff |
annotate
|
| Fri, 10 Oct 2008 06:45:53 +0200 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
| Thu, 27 Mar 2008 19:04:37 +0100 |
haftmann |
lemmas about map_of (zip _ _)
|
file |
diff |
annotate
|
| Fri, 25 Jan 2008 14:54:41 +0100 |
haftmann |
improved code theorem setup
|
file |
diff |
annotate
|
| Mon, 17 Dec 2007 18:01:51 +0100 |
haftmann |
whitespace typo
|
file |
diff |
annotate
|
| Wed, 28 Nov 2007 15:26:39 +0100 |
haftmann |
(reverted to unnamed infix)
|
file |
diff |
annotate
|
| Wed, 28 Nov 2007 09:01:39 +0100 |
haftmann |
dropped legacy unnamed infix
|
file |
diff |
annotate
|
| Sun, 19 Aug 2007 21:21:37 +0200 |
nipkow |
Made UN_Un simp
|
file |
diff |
annotate
|
| Fri, 20 Apr 2007 11:21:42 +0200 |
haftmann |
Isar definitions are now added explicitly to code theorem table
|
file |
diff |
annotate
|
| Fri, 02 Feb 2007 15:47:58 +0100 |
nipkow |
a few additions and deletions
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Tue, 07 Nov 2006 11:47:57 +0100 |
wenzelm |
renamed 'const_syntax' to 'notation';
|
file |
diff |
annotate
|
| Sat, 30 Sep 2006 21:39:24 +0200 |
wenzelm |
tuned specifications and proofs;
|
file |
diff |
annotate
|
| Sat, 24 Jun 2006 22:25:30 +0200 |
wenzelm |
fixed translations for _MapUpd: CONST;
|
file |
diff |
annotate
|
| Tue, 16 May 2006 21:33:01 +0200 |
wenzelm |
tuned concrete syntax -- abbreviation/const_syntax;
|
file |
diff |
annotate
|
| Sun, 09 Apr 2006 14:47:24 +0200 |
nipkow |
Made "empty" an abbreviation.
|
file |
diff |
annotate
|
| Thu, 23 Mar 2006 20:03:53 +0100 |
nipkow |
Converted translations to abbbreviations.
|
file |
diff |
annotate
|
| Wed, 04 Jan 2006 19:22:53 +0100 |
nipkow |
Reversed Larry's option/iff change.
|
file |
diff |
annotate
|
| Wed, 21 Dec 2005 12:02:57 +0100 |
paulson |
removed or modified some instances of [iff]
|
file |
diff |
annotate
|
| Fri, 07 Oct 2005 22:59:19 +0200 |
wenzelm |
replaced _K by dummy abstraction;
|
file |
diff |
annotate
|
| Thu, 29 Sep 2005 17:02:57 +0200 |
paulson |
simprules need names
|
file |
diff |
annotate
|
| Wed, 14 Sep 2005 23:55:49 +0200 |
wenzelm |
@{term [source] ...} in subsections probably more robust;
|
file |
diff |
annotate
|
| Wed, 14 Sep 2005 23:03:52 +0200 |
schirmer |
removed syntax fun_map_comp;
|
file |
diff |
annotate
|
| Mon, 11 Apr 2005 12:18:27 +0200 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Mon, 11 Apr 2005 12:14:23 +0200 |
nipkow |
tuned Map, renamed lex stuff in List.
|
file |
diff |
annotate
|
| Sun, 10 Apr 2005 17:19:03 +0200 |
nipkow |
_(_|_) is now override_on
|
file |
diff |
annotate
|
| Fri, 03 Dec 2004 15:27:47 +0100 |
paulson |
tidied
|
file |
diff |
annotate
|
| Sun, 21 Nov 2004 18:39:25 +0100 |
nipkow |
Added more lemmas
|
file |
diff |
annotate
|
| Sun, 21 Nov 2004 15:44:20 +0100 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
| Tue, 19 Oct 2004 18:18:45 +0200 |
paulson |
converted some induct_tac to induct
|
file |
diff |
annotate
|
| Wed, 18 Aug 2004 11:09:40 +0200 |
nipkow |
import -> imports
|
file |
diff |
annotate
|
| Mon, 16 Aug 2004 14:22:27 +0200 |
nipkow |
New theory header syntax.
|
file |
diff |
annotate
|
| Wed, 04 Aug 2004 19:10:45 +0200 |
nipkow |
Added a number of new thms and the new function remove1
|
file |
diff |
annotate
|
| Wed, 12 May 2004 08:14:29 +0200 |
nipkow |
renamed `> to o_m
|
file |
diff |
annotate
|
| Mon, 12 Apr 2004 19:54:09 +0200 |
oheimb |
added theorem chg_map_other
|
file |
diff |
annotate
|
| Thu, 05 Feb 2004 04:30:38 +0100 |
nipkow |
Changed variable names.
|
file |
diff |
annotate
|
| Thu, 18 Dec 2003 08:20:36 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Fri, 26 Sep 2003 10:34:57 +0200 |
paulson |
misc tidying
|
file |
diff |
annotate
|
| Sun, 14 Sep 2003 17:53:27 +0200 |
nipkow |
Added new theorems
|
file |
diff |
annotate
|
| Thu, 11 Sep 2003 22:33:12 +0200 |
nipkow |
Added a number of thms about map restriction.
|
file |
diff |
annotate
|
| Wed, 03 Sep 2003 18:20:57 +0200 |
nipkow |
Introduced new syntax for maplets x |-> y
|
file |
diff |
annotate
|
| Fri, 25 Jul 2003 17:21:22 +0200 |
nipkow |
Replaced \<leadsto> by \<rightharpoonup>
|
file |
diff |
annotate
|
| Fri, 11 Jul 2003 14:12:06 +0200 |
oheimb |
added map_image, restrict_map, some thms
|
file |
diff |
annotate
|
| Fri, 16 May 2003 16:35:36 +0200 |
webertj |
Added a few lemmas about map_le
|
file |
diff |
annotate
|
| Wed, 14 May 2003 11:15:18 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Wed, 14 May 2003 10:33:52 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Wed, 14 May 2003 10:22:09 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Wed, 30 Apr 2003 17:53:47 +0200 |
nipkow |
added a thm
|
file |
diff |
annotate
|
| Wed, 16 Apr 2003 22:21:32 +0200 |
nipkow |
header
|
file |
diff |
annotate
|
| Tue, 15 Apr 2003 12:55:31 +0200 |
kleing |
fixed document
|
file |
diff |
annotate
|
| Mon, 14 Apr 2003 18:52:13 +0200 |
nipkow |
Added thms
|
file |
diff |
annotate
|
| Mon, 14 Apr 2003 13:51:31 +0200 |
webertj |
Fixed non-escaped underscore in section headings (document generation should
|
file |
diff |
annotate
|
| Fri, 11 Apr 2003 23:11:13 +0200 |
webertj |
Map.ML integrated into Map.thy
|
file |
diff |
annotate
|
| Tue, 01 Apr 2003 17:43:10 +0200 |
nipkow |
Made empty a translation rather than a constant.
|
file |
diff |
annotate
|
| Thu, 21 Feb 2002 20:09:19 +0100 |
wenzelm |
removed theory Option;
|
file |
diff |
annotate
|
| Fri, 09 Nov 2001 00:09:47 +0100 |
wenzelm |
eliminated old "symbols" syntax, use "xsymbols" instead;
|
file |
diff |
annotate
|
| Tue, 03 Oct 2000 18:40:25 +0200 |
wenzelm |
removed "symbols" syntax for constant "override";
|
file |
diff |
annotate
|
| Wed, 27 Oct 1999 19:32:19 +0200 |
oheimb |
added various little lemmas
|
file |
diff |
annotate
|
| Wed, 12 Aug 1998 16:04:27 +0200 |
oheimb |
defined map_upd by translation via fun_upd
|
file |
diff |
annotate
|
| Fri, 24 Jul 1998 17:18:15 +0200 |
nipkow |
Map.update -> map_upd, Unpdate.update -> fun_upd
|
file |
diff |
annotate
|