#
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
cc47ae18 |
|
17-Jun-2018 |
nipkow <none@none> |
added simp rules
|
#
c84f26fc |
|
15-Jun-2018 |
nipkow <none@none> |
moved lemmas from AFP
|
#
dd214cba |
|
15-Jun-2018 |
nipkow <none@none> |
Map.empty now qualified to avoid name clashes
|
#
5538296a |
|
07-Mar-2018 |
wenzelm <none@none> |
more abbrevs -- this makes "(=" ambiguous and thus simplifies input of "(=)" (within the context of Main HOL);
|
#
c7cc1919 |
|
26-Nov-2017 |
wenzelm <none@none> |
more symbols;
|
#
85b3e948 |
|
11-Nov-2017 |
haftmann <none@none> |
dedicated definition for coprimality --HG-- extra : rebase_source : 891168c98ce62efae6b7e72c7d3365fea12b33ae
|
#
90e3ae3c |
|
01-Sep-2017 |
bulwahn <none@none> |
more facts on Map.map_of and List.zip --HG-- extra : rebase_source : aabab8a4de88b4f4ff69c542f7e9d1c239fc1a0f
|
#
4f6b421b |
|
26-Aug-2017 |
bulwahn <none@none> |
more facts on Map.ran --HG-- extra : rebase_source : d61a2c0821deb956f90db3fb9c2dac2670a5c3da
|
#
3c4faa3a |
|
05-Jun-2017 |
haftmann <none@none> |
executable domain membership checks --HG-- extra : rebase_source : 77e2c6439ac87c558348313cdbfac8f7d3e81d95
|
#
9147221e |
|
10-Sep-2016 |
wenzelm <none@none> |
tuned proofs;
|
#
d96745dd |
|
09-Sep-2016 |
nipkow <none@none> |
added lemmas
|
#
2df4ddef |
|
10-Aug-2016 |
nipkow <none@none> |
"split add" -> "split"
|
#
35f7dccd |
|
23-Feb-2016 |
nipkow <none@none> |
more canonical names
|
#
0bfb73b6 |
|
28-Dec-2015 |
wenzelm <none@none> |
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
|
#
0df376fc |
|
07-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
883895af |
|
31-Aug-2015 |
wenzelm <none@none> |
prefer symbols;
|
#
df44ab4c |
|
27-Aug-2015 |
haftmann <none@none> |
standardized some occurences of ancient "split" alias --HG-- extra : rebase_source : 706ba501d5c0596a2bde6e46d42aa8464a91ede5
|
#
85802007 |
|
04-Aug-2015 |
wenzelm <none@none> |
eliminated clone;
|
#
751f8d90 |
|
04-Aug-2015 |
wenzelm <none@none> |
more symbols; more spaces;
|
#
eee57403 |
|
04-Aug-2015 |
wenzelm <none@none> |
more symbols;
|
#
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
#
b4ae9938 |
|
14-Apr-2015 |
Andreas Lochbihler <none@none> |
add lemmas
|
#
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
#
d766ca99 |
|
12-Apr-2014 |
haftmann <none@none> |
more operations and lemmas --HG-- extra : rebase_source : 8f5be7e0cdc09c667e66c2cda2c667d4da6e5f73
|
#
447c00c8 |
|
13-Feb-2014 |
blanchet <none@none> |
merged 'Option.map' and 'Option.map_option'
|
#
e5a198cc |
|
24-Sep-2013 |
nipkow <none@none> |
added lemmas
|
#
7237bdd9 |
|
02-Sep-2013 |
wenzelm <none@none> |
tuned proofs -- clarified flow of facts wrt. calculation;
|
#
06329277 |
|
13-Aug-2013 |
wenzelm <none@none> |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
#
422810da |
|
21-Feb-2012 |
bulwahn <none@none> |
removing some unnecessary premises from Map theory
|
#
15635718 |
|
13-Sep-2011 |
huffman <none@none> |
tuned proofs
|
#
ad9e459c |
|
11-Sep-2011 |
nipkow <none@none> |
new fastforce replacing fastsimp - less confusing name
|
#
0d0a8a60 |
|
30-Mar-2011 |
bulwahn <none@none> |
renewing specifications in HOL: replacing types by type_synonym
|
#
6fb8be2b |
|
14-Jan-2011 |
wenzelm <none@none> |
eliminated global prems; tuned proofs;
|
#
adfe6cf9 |
|
17-Dec-2010 |
wenzelm <none@none> |
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
|
#
33206df1 |
|
10-Oct-2010 |
krauss <none@none> |
removed output syntax "'a ~=> 'b" for "'a => 'b option"
|
#
aa5e12fe |
|
13-Sep-2010 |
haftmann <none@none> |
moved lemmas map_of_eqI and map_of_eq_dom to Map.thy
|
#
5b59da77 |
|
13-Sep-2010 |
nipkow <none@none> |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
#
bb8268b1 |
|
07-Sep-2010 |
nipkow <none@none> |
expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
|
#
db8d7171 |
|
06-Mar-2010 |
haftmann <none@none> |
lemma restrict_complement_singleton_eq
|
#
776f0fc5 |
|
06-Mar-2010 |
haftmann <none@none> |
added dom_option_map, map_of_map_keys
|
#
4fd58a44 |
|
04-Mar-2010 |
haftmann <none@none> |
lemmas set_map_of_compr, map_of_inject_set
|
#
e5edb092 |
|
03-Mar-2010 |
haftmann <none@none> |
more uniform naming conventions
|
#
db258df9 |
|
02-Mar-2010 |
wenzelm <none@none> |
proper (type_)notation;
|
#
3f83a35e |
|
17-Feb-2010 |
haftmann <none@none> |
added lemma map_of_map_restrict; generalized lemma dom_const
|
#
4f52a6da |
|
11-Feb-2010 |
wenzelm <none@none> |
modernized translations; formal markup of @{syntax_const} and @{const_syntax}; minor tuning;
|
#
daa35d88 |
|
31-Jan-2010 |
haftmann <none@none> |
more correspondence lemmas between related operations
|
#
74426e02 |
|
16-Jan-2010 |
haftmann <none@none> |
dropped some old primrecs and some constdefs
|
#
2021b671 |
|
12-Nov-2009 |
haftmann <none@none> |
moved lemma map_of_zip_map to Map.thy
|
#
6914c079 |
|
27-Jul-2009 |
krauss <none@none> |
some lemmas about maps (contributed by Peter Lammich)
|
#
29ed20ca |
|
02-Jun-2009 |
haftmann <none@none> |
added/moved lemmas by Andreas Lochbihler
|
#
6ca1bd25 |
|
08-May-2009 |
nipkow <none@none> |
lemmas by Andreas Lochbihler
|
#
eba69609 |
|
16-Apr-2009 |
haftmann <none@none> |
dropped unnamed infix
|
#
262e6aa4 |
|
27-Mar-2009 |
haftmann <none@none> |
normalized imports
|
#
b391ac6a |
|
04-Mar-2009 |
nipkow <none@none> |
Made Option a separate theory and renamed option_map to Option.map
|
#
22d05b7b |
|
23-Jan-2009 |
haftmann <none@none> |
lemmas dom_const, dom_if
|
#
4936aad7 |
|
14-Nov-2008 |
haftmann <none@none> |
lemmas about dom and minus / insert
|
#
d63044b5 |
|
09-Oct-2008 |
haftmann <none@none> |
`code func` now just `code`
|
#
7d12779f |
|
27-Mar-2008 |
haftmann <none@none> |
lemmas about map_of (zip _ _)
|
#
c4bd05ca |
|
25-Jan-2008 |
haftmann <none@none> |
improved code theorem setup
|
#
1b95ceae |
|
17-Dec-2007 |
haftmann <none@none> |
whitespace typo
|
#
9245beb4 |
|
28-Nov-2007 |
haftmann <none@none> |
(reverted to unnamed infix)
|
#
78e8471d |
|
28-Nov-2007 |
haftmann <none@none> |
dropped legacy unnamed infix
|
#
1f542704 |
|
19-Aug-2007 |
nipkow <none@none> |
Made UN_Un simp
|
#
167fea11 |
|
20-Apr-2007 |
haftmann <none@none> |
Isar definitions are now added explicitly to code theorem table
|
#
6d96cc4f |
|
02-Feb-2007 |
nipkow <none@none> |
a few additions and deletions
|
#
cd65d9bc |
|
16-Nov-2006 |
wenzelm <none@none> |
more robust syntax for definition/abbreviation/notation;
|
#
cbb1a051 |
|
07-Nov-2006 |
wenzelm <none@none> |
renamed 'const_syntax' to 'notation';
|
#
f6377247 |
|
30-Sep-2006 |
wenzelm <none@none> |
tuned specifications and proofs;
|
#
5e2b6ec8 |
|
24-Jun-2006 |
wenzelm <none@none> |
fixed translations for _MapUpd: CONST;
|
#
61bd82ad |
|
16-May-2006 |
wenzelm <none@none> |
tuned concrete syntax -- abbreviation/const_syntax;
|
#
92e5bdc9 |
|
09-Apr-2006 |
nipkow <none@none> |
Made "empty" an abbreviation.
|
#
84161ae1 |
|
23-Mar-2006 |
nipkow <none@none> |
Converted translations to abbbreviations. Removed a few odd functions from Map and AssocList. Moved chg_map from Map to Bali/Basis.
|
#
64519e34 |
|
04-Jan-2006 |
nipkow <none@none> |
Reversed Larry's option/iff change.
|
#
d9f4c279 |
|
20-Dec-2005 |
paulson <none@none> |
removed or modified some instances of [iff]
|
#
c046356e |
|
07-Oct-2005 |
wenzelm <none@none> |
replaced _K by dummy abstraction;
|
#
4925430d |
|
29-Sep-2005 |
paulson <none@none> |
simprules need names
|
#
03830b02 |
|
14-Sep-2005 |
wenzelm <none@none> |
@{term [source] ...} in subsections probably more robust;
|
#
7017e0b4 |
|
14-Sep-2005 |
schirmer <none@none> |
removed syntax fun_map_comp; introduced map_comp;
|
#
c2710dc3 |
|
10-Apr-2005 |
nipkow <none@none> |
tuned
|
#
c48de73e |
|
10-Apr-2005 |
nipkow <none@none> |
tuned Map, renamed lex stuff in List.
|
#
bf3fe264 |
|
10-Apr-2005 |
nipkow <none@none> |
_(_|_) is now override_on
|
#
8e39439a |
|
03-Dec-2004 |
paulson <none@none> |
tidied
|
#
82c20b4c |
|
21-Nov-2004 |
nipkow <none@none> |
Added more lemmas
|
#
3f348152 |
|
21-Nov-2004 |
nipkow <none@none> |
added lemmas
|
#
997b6b04 |
|
19-Oct-2004 |
paulson <none@none> |
converted some induct_tac to induct
|
#
0fe1d442 |
|
18-Aug-2004 |
nipkow <none@none> |
import -> imports
|
#
e61c8d7d |
|
16-Aug-2004 |
nipkow <none@none> |
New theory header syntax.
|
#
22382750 |
|
04-Aug-2004 |
nipkow <none@none> |
Added a number of new thms and the new function remove1
|
#
a19ad723 |
|
12-May-2004 |
nipkow <none@none> |
renamed `> to o_m
|
#
0d5eb1ab |
|
12-Apr-2004 |
oheimb <none@none> |
added theorem chg_map_other
|
#
3cb9dcc6 |
|
04-Feb-2004 |
nipkow <none@none> |
Changed variable names.
|
#
36f64ffe |
|
18-Dec-2003 |
nipkow <none@none> |
*** empty log message ***
|
#
b79b3996 |
|
26-Sep-2003 |
paulson <none@none> |
misc tidying
|
#
86601865 |
|
14-Sep-2003 |
nipkow <none@none> |
Added new theorems
|
#
2688ecb2 |
|
11-Sep-2003 |
nipkow <none@none> |
Added a number of thms about map restriction.
|
#
cb68a121 |
|
03-Sep-2003 |
nipkow <none@none> |
Introduced new syntax for maplets x |-> y
|
#
67a49057 |
|
25-Jul-2003 |
nipkow <none@none> |
Replaced \<leadsto> by \<rightharpoonup>
|
#
3b716a04 |
|
11-Jul-2003 |
oheimb <none@none> |
added map_image, restrict_map, some thms
|
#
f5151ca2 |
|
16-May-2003 |
webertj <none@none> |
Added a few lemmas about map_le
|
#
748fa824 |
|
14-May-2003 |
nipkow <none@none> |
*** empty log message ***
|
#
3da8ff58 |
|
14-May-2003 |
nipkow <none@none> |
*** empty log message ***
|
#
efd5dc29 |
|
14-May-2003 |
nipkow <none@none> |
*** empty log message ***
|
#
46f11104 |
|
30-Apr-2003 |
nipkow <none@none> |
added a thm
|
#
0ea0d1f3 |
|
16-Apr-2003 |
nipkow <none@none> |
header
|
#
7d7b0514 |
|
14-Apr-2003 |
kleing <none@none> |
fixed document
|
#
2ec67d0a |
|
14-Apr-2003 |
nipkow <none@none> |
Added thms
|
#
5e24b6fe |
|
14-Apr-2003 |
webertj <none@none> |
Fixed non-escaped underscore in section headings (document generation should work again now).
|
#
474023cc |
|
11-Apr-2003 |
webertj <none@none> |
Map.ML integrated into Map.thy
|
#
829121c5 |
|
01-Apr-2003 |
nipkow <none@none> |
Made empty a translation rather than a constant.
|
#
3da61775 |
|
21-Feb-2002 |
wenzelm <none@none> |
removed theory Option;
|
#
c1694cb4 |
|
08-Nov-2001 |
wenzelm <none@none> |
eliminated old "symbols" syntax, use "xsymbols" instead;
|
#
3f2d0804 |
|
03-Oct-2000 |
wenzelm <none@none> |
removed "symbols" syntax for constant "override";
|
#
fe3d7081 |
|
27-Oct-1999 |
oheimb <none@none> |
added various little lemmas
|
#
a9f01c8c |
|
12-Aug-1998 |
oheimb <none@none> |
defined map_upd by translation via fun_upd changed syntax of map_upd to be consistent with that of fun_upd added chg_map, map_upds
|
#
55c59912 |
|
24-Jul-1998 |
nipkow <none@none> |
Map.update -> map_upd, Unpdate.update -> fun_upd Problem: macros get confused about two updates.
|
#
df41c559 |
|
24-Jul-1998 |
berghofe <none@none> |
Adapted to new datatype package.
|
#
79e81ed2 |
|
24-Oct-1997 |
nipkow <none@none> |
Added the new theory Map.
|