added simp rules

moved lemmas from AFP

Map.empty now qualified to avoid name clashes

more abbrevs -- this makes "(=" ambiguous and thus simplifies input of "(=)" (within the context of Main HOL);

more symbols;

dedicated definition for coprimality

--HG--
extra : rebase_source : 891168c98ce62efae6b7e72c7d3365fea12b33ae

more facts on Map.map_of and List.zip

--HG--
extra : rebase_source : aabab8a4de88b4f4ff69c542f7e9d1c239fc1a0f

more facts on Map.ran

--HG--
extra : rebase_source : d61a2c0821deb956f90db3fb9c2dac2670a5c3da

executable domain membership checks

--HG--
extra : rebase_source : 77e2c6439ac87c558348313cdbfac8f7d3e81d95

tuned proofs;

added lemmas

"split add" -> "split"

more canonical names

former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";

isabelle update_cartouches -c -t;

prefer symbols;

standardized some occurences of ancient "split" alias

--HG--
extra : rebase_source : 706ba501d5c0596a2bde6e46d42aa8464a91ede5

eliminated clone;

more symbols;
more spaces;

more symbols;

isabelle update_cartouches;

add lemmas

modernized header uniformly as section;

more operations and lemmas

--HG--
extra : rebase_source : 8f5be7e0cdc09c667e66c2cda2c667d4da6e5f73

merged 'Option.map' and 'Option.map_option'

added lemmas

tuned proofs -- clarified flow of facts wrt. calculation;

standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;

removing some unnecessary premises from Map theory

tuned proofs

new fastforce replacing fastsimp - less confusing name

renewing specifications in HOL: replacing types by type_synonym

eliminated global prems;
tuned proofs;

replaced command 'nonterminals' by slightly modernized version 'nonterminal';

removed output syntax "'a ~=> 'b" for "'a => 'b option"

moved lemmas map_of_eqI and map_of_eq_dom to Map.thy

renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI

expand_fun_eq -> ext_iff
expand_set_eq -> set_ext_iff
Naming in line now with multisets

lemma restrict_complement_singleton_eq

added dom_option_map, map_of_map_keys

lemmas set_map_of_compr, map_of_inject_set

more uniform naming conventions

proper (type_)notation;

added lemma map_of_map_restrict; generalized lemma dom_const

modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;

more correspondence lemmas between related operations

dropped some old primrecs and some constdefs

moved lemma map_of_zip_map to Map.thy

some lemmas about maps (contributed by Peter Lammich)

added/moved lemmas by Andreas Lochbihler

lemmas by Andreas Lochbihler

dropped unnamed infix

normalized imports

Made Option a separate theory and renamed option_map to Option.map

lemmas dom_const, dom_if

lemmas about dom and minus / insert

`code func` now just `code`

lemmas about map_of (zip _ _)

improved code theorem setup

whitespace typo

(reverted to unnamed infix)

dropped legacy unnamed infix

Made UN_Un simp

Isar definitions are now added explicitly to code theorem table

a few additions and deletions

more robust syntax for definition/abbreviation/notation;

renamed 'const_syntax' to 'notation';

tuned specifications and proofs;

fixed translations for _MapUpd: CONST;

tuned concrete syntax -- abbreviation/const_syntax;

Made "empty" an abbreviation.

Converted translations to abbbreviations.
Removed a few odd functions from Map and AssocList.
Moved chg_map from Map to Bali/Basis.

Reversed Larry's option/iff change.

removed or modified some instances of [iff]

replaced _K by dummy abstraction;

simprules need names

@{term [source] ...} in subsections probably more robust;

removed syntax fun_map_comp;
introduced map_comp;

tuned

tuned Map, renamed lex stuff in List.

_(_|_) is now override_on

tidied

Added more lemmas

added lemmas

converted some induct_tac to induct

import -> imports

New theory header syntax.

Added a number of new thms and the new function remove1

renamed `> to o_m

added theorem chg_map_other

Changed variable names.

*** empty log message ***

misc tidying

Added new theorems

Added a number of thms about map restriction.

Introduced new syntax for maplets x |-> y

Replaced \<leadsto> by \<rightharpoonup>

added map_image, restrict_map, some thms

Added a few lemmas about map_le

*** empty log message ***

*** empty log message ***

*** empty log message ***

added a thm

header

fixed document

Added thms

Fixed non-escaped underscore in section headings (document generation should
work again now).

Map.ML integrated into Map.thy

Made empty a translation rather than a constant.

removed theory Option;

eliminated old "symbols" syntax, use "xsymbols" instead;

removed "symbols" syntax for constant "override";

added various little lemmas

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

Map.update -> map_upd, Unpdate.update -> fun_upd
Problem: macros get confused about two updates.

Adapted to new datatype package.

Added the new theory Map.