ran isabelle update_op on all sources

isabelle update_cartouches -c -t;

restored surj as output abbreviation, amending 6af79184bef3

added inj_def (redundant, analogous to surj_def, bij_def);
tuned proofs;

tuned proofs;

tuned proof;

misc tuning and modernization;

misc tuning and modernization;

add lemmas contributed by Peter Gammie

avoid to hide equality behind (output) abbreviation

misc tuning and modernization;

more theorems

prefer HOL definitions;

tuned proof;

misc tuning and modernization;

renamings and refinements

Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results

Refactoring (moving theorems into better locations), plus a bit of new material

more canonical names

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

isabelle update_cartouches -c -t;

New theorems mostly from Peter Gammie

add various lemmas

Cauchy's integral formula, required lemmas, and a bit of reorganisation

discontinued specific HTML syntax;

new lemmas and movement of lemmas into place

more lemmas

--HG--
extra : rebase_source : 629d5d21c15fc4a23007104e9f5a8ccccbad1886

isabelle update_cartouches;

New material about paths, and some lemmas

add lemmas about bind and image

New lemmas and a bit of tidying up.

proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
occasionally clarified use of context;

modernized header uniformly as section;

eliminated aliases;

added various facts

tuned structure inclusion

Two basic lemmas on bij_betw.

more simp rules for Fun.swap

more complete set of lemmas wrt. image and composition

tuned proofs

bootstrap fundamental Fun theory immediately after Set theory, without dependency on complete lattices
* * *
tuned

more antiquotations;

renamed 'enriched_type' to more informative 'functor' (following the renaming of enriched type constructors to bounded natural functors)

--HG--
rename : src/HOL/Tools/enriched_type.ML => src/HOL/Tools/functor.ML

renamed '{prod,sum,bool,unit}_case' to 'case_...'

tuning

moved lemmas from 'Fun_More_FP' to where they belong

eliminated dependence of BNF on Infinite_Set by moving 3 theorems from the latter to Main

killed most "no_atp", to make Sledgehammer more complete

add lemmas

migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier

--HG--
extra : rebase_source : ff8027ac9606264aa4b2d4f8da037c426a3db98b

simplifier uses proper Proof.context instead of historic type simpset;

generalized lemma fold_image thanks to Peter Lammich

simp results for simplification results of Inf/Sup expressions on bool;
tuned proofs

consolidated names of theorems on composition;
generalized former theorem UN_o;
comp_assoc orients to the right, as is more common

prefer ML_file over old uses;

tuned lemmas (v)image_id;
removed duplicate of vimage_id

--HG--
extra : rebase_source : 9178db2e0f900cdeab723f13b8c0d5fc45786a95

centralized enriched_type declaration, thanks to in-situ available Isar commands

--HG--
extra : rebase_source : ea8947ffa8bb301d674c472c3427994b31c4c458

declare command keywords via theory header, including strict checking outside Pure;

generalizing inj_on_Int

removing lemma bij_betw_Disj_Un, as it is a special case of bij_between_combine (was added in d1fc454d6735, and has not been used since)

adding a remark about lemma which is too special and should be removed

explicit is better than implicit;

removing old code generator setup for function types

tuned proofs

renamed Complete_Lattices lemmas, removed legacy names

new fastforce replacing fastsimp - less confusing name

renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc.

--HG--
rename : src/HOL/Complete_Lattice.thy => src/HOL/Complete_Lattices.thy

added new lemmas

moved fundamental lemma fun_eq_iff to theory HOL; tuned whitespace

finite vimage on arbitrary domains

more on complement

added translation to fix critical pair between abbreviations for surj and ~=

add surj_vimage_empty

added "no_atp" to Cantor's paradox

moved theorem

"enriched_type" replaces less specific "type_lifting"

--HG--
rename : src/HOL/Tools/type_lifting.ML => src/HOL/Tools/enriched_type.ML

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

moved bootstrap of type_lifting to Fun

replace `type_mapper` by the more adequate `type_lifting`

--HG--
rename : src/HOL/Tools/type_mapper.ML => src/HOL/Tools/type_lifting.ML

keep private things private, without comments;

Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.

Replace surj by abbreviation; remove surj_on.

map_fun combinator in theory Fun

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

put expand_(fun/set)_eq back in as synonyms, for compatibility

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

Revert bij_betw changes to simp set (Problem in afp/Ordinals_and_Cardinals)

Introduce surj_on and replace surj and bij by abbreviations.

Permutation implies bij function

bij <--> bij_betw

inj_comp and inj_fun

dropped superfluous [code del]s

nicer xsymbol syntax for fcomp and scomp

replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;

generalized inj_uminus; added strict_mono_imp_inj_on

Rewrite rules for images of minus of intervals

replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)

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

killed a few warnings

moved lemmas o_eq_dest, o_eq_elim here

add lemma swap_triple

declare swap_self [simp], add lemma comp_swap

moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly

inv_onto -> inv_into

Some new lemmas concerning sets

Renamed inv to the_inv and turned it into an abbreviation (based on the_inv_onto).

Inv -> inv_onto, inv abbr. inv_onto UNIV.

added the_inv_onto

explicit indication of Unsynchronized.ref;

early bootstrap of generic transfer procedure

new lemma bij_comp

moved complete_lattice &c. into separate theory

--HG--
rename : src/HOL/Set.thy => src/HOL/Complete_Lattice.thy

moved Inductive.myinv to Fun.inv; tuned

uniformly capitialized names for subdirectories

--HG--
rename : src/HOL/Tools/datatype_package/datatype.ML => src/HOL/Tools/Datatype/datatype.ML
rename : src/HOL/Tools/datatype_package/datatype_abs_proofs.ML => src/HOL/Tools/Datatype/datatype_abs_proofs.ML
rename : src/HOL/Tools/datatype_package/datatype_aux.ML => src/HOL/Tools/Datatype/datatype_aux.ML
rename : src/HOL/Tools/datatype_package/datatype_case.ML => src/HOL/Tools/Datatype/datatype_case.ML
rename : src/HOL/Tools/datatype_package/datatype_codegen.ML => src/HOL/Tools/Datatype/datatype_codegen.ML
rename : src/HOL/Tools/datatype_package/datatype_prop.ML => src/HOL/Tools/Datatype/datatype_prop.ML
rename : src/HOL/Tools/datatype_package/datatype_realizer.ML => src/HOL/Tools/Datatype/datatype_realizer.ML
rename : src/HOL/Tools/datatype_package/datatype_rep_proofs.ML => src/HOL/Tools/Datatype/datatype_rep_proofs.ML
rename : src/HOL/Tools/function_package/auto_term.ML => src/HOL/Tools/Function/auto_term.ML
rename : src/HOL/Tools/function_package/context_tree.ML => src/HOL/Tools/Function/context_tree.ML
rename : src/HOL/Tools/function_package/decompose.ML => src/HOL/Tools/Function/decompose.ML
rename : src/HOL/Tools/function_package/descent.ML => src/HOL/Tools/Function/descent.ML
rename : src/HOL/Tools/function_package/fundef.ML => src/HOL/Tools/Function/fundef.ML
rename : src/HOL/Tools/function_package/fundef_common.ML => src/HOL/Tools/Function/fundef_common.ML
rename : src/HOL/Tools/function_package/fundef_core.ML => src/HOL/Tools/Function/fundef_core.ML
rename : src/HOL/Tools/function_package/fundef_datatype.ML => src/HOL/Tools/Function/fundef_datatype.ML
rename : src/HOL/Tools/function_package/fundef_lib.ML => src/HOL/Tools/Function/fundef_lib.ML
rename : src/HOL/Tools/function_package/induction_scheme.ML => src/HOL/Tools/Function/induction_scheme.ML
rename : src/HOL/Tools/function_package/inductive_wrap.ML => src/HOL/Tools/Function/inductive_wrap.ML
rename : src/HOL/Tools/function_package/lexicographic_order.ML => src/HOL/Tools/Function/lexicographic_order.ML
rename : src/HOL/Tools/function_package/measure_functions.ML => src/HOL/Tools/Function/measure_functions.ML
rename : src/HOL/Tools/function_package/mutual.ML => src/HOL/Tools/Function/mutual.ML
rename : src/HOL/Tools/function_package/pattern_split.ML => src/HOL/Tools/Function/pattern_split.ML
rename : src/HOL/Tools/function_package/scnp_reconstruct.ML => src/HOL/Tools/Function/scnp_reconstruct.ML
rename : src/HOL/Tools/function_package/scnp_solve.ML => src/HOL/Tools/Function/scnp_solve.ML
rename : src/HOL/Tools/function_package/size.ML => src/HOL/Tools/Function/size.ML
rename : src/HOL/Tools/function_package/sum_tree.ML => src/HOL/Tools/Function/sum_tree.ML
rename : src/HOL/Tools/function_package/termination.ML => src/HOL/Tools/Function/termination.ML
rename : src/Tools/code/code_haskell.ML => src/Tools/Code/code_haskell.ML
rename : src/Tools/code/code_ml.ML => src/Tools/Code/code_ml.ML
rename : src/Tools/code/code_preproc.ML => src/Tools/Code/code_preproc.ML
rename : src/Tools/code/code_printer.ML => src/Tools/Code/code_printer.ML
rename : src/Tools/code/code_target.ML => src/Tools/Code/code_target.ML
rename : src/Tools/code/code_thingol.ML => src/Tools/Code/code_thingol.ML

separate directory for datatype package

--HG--
rename : src/HOL/Tools/datatype_abs_proofs.ML => src/HOL/Tools/datatype_package/datatype_abs_proofs.ML
rename : src/HOL/Tools/datatype_case.ML => src/HOL/Tools/datatype_package/datatype_case.ML
rename : src/HOL/Tools/datatype_codegen.ML => src/HOL/Tools/datatype_package/datatype_codegen.ML
rename : src/HOL/Tools/datatype_package.ML => src/HOL/Tools/datatype_package/datatype_package.ML
rename : src/HOL/Tools/datatype_prop.ML => src/HOL/Tools/datatype_package/datatype_prop.ML
rename : src/HOL/Tools/datatype_realizer.ML => src/HOL/Tools/datatype_package/datatype_realizer.ML
rename : src/HOL/Tools/datatype_rep_proofs.ML => src/HOL/Tools/datatype_package/datatype_rep_proofs.ML

A few finite lemmas

pretty printing of functional combinators for evaluation code

lemmas by Andreas Lochbihler

dropped Id

Replaced arbitrary by undefined.

`code func` now just `code`

Logic.all/mk_equals/mk_implies;

hide -> hide (open)

Hid swap

tuned proofs -- case_tac *is* available here;

removed some dubious code lemmas

removed syntax from monad combinators; renamed mbind to scomp

added forward composition

more antiquotations;

moved some set lemmas to Set.thy

moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
added some

Added test data generator for function type (from Pure/codegen.ML).

ATP blacklisting is now in theory data, attribute noatp

simproc_setup fun_upd2;

simplified HOL bootstrap

Added ML bindings for sup_fun_eq and sup_bool_eq.

moved recfun_codegen.ML to Code_Generator.thy

changed code generator invocation syntax

Isar definitions are now added explicitly to code theorem table

ML antiquotes;

moved lattice instance here

explizit serialization for Haskell id

infix syntax for generated code for composition

moved order arities for fun and bool to Fun/Orderings

dropped Typedef dependency

renamed 'const_syntax' to 'notation';

simprocs: no theory argument -- use simpset context instead;

tuned concrete syntax -- abbreviation/const_syntax;

replaced syntax/translations by abbreviation;

refined 'abbreviation';

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

add header

Goal.prove;

Simplifier.inherit_context instead of Simplifier.inherit_bounds;

renamed rules to iprover

classical rules must have names for ATP integration

simprocs: Simplifier.inherit_bounds;

linear arithmetic now takes "&" in assumptions apart.

_(_|_) is now override_on

Deleted Library.option type.

new foldSet proofs

made diff_less a simp rule

added lemmas

import -> imports

New theory header syntax.

added some inj_on thms

use more symbols in HTML output

Added thms

- Added range_ex1_eq
- Removed obsolete theorems inj_o and inj_fun_lemma

Converted Fun to Isar style.
Moved Pi, funcset, restrict from Fun.thy to Library/FuncSet.thy.
Renamed constant "Fun.op o" to "Fun.comp"

oops;

bounded abstraction now uses syntax "%" / "\<lambda>" instead of "lam";

renamed class "term" to "type" (actually "HOL.type");

got rid of theory Inverse_Image;

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

eliminated theories "equalities" and "mono" (made part of "Typedef",
which supercedes "subset");

partial restructuring to reduce dependence on Axiom of Choice

removed whitespace

Removed Applyall

*** empty log message ***

syntax (symbols) "op o" moved from HOL to Fun;

added hint on fun_sum

fixed compose decl;

tuned;

we must not require SetInterval this early

Added SetInterval

changed precedence of function update

the bij predicate (at last)

inj is now a translation of inj_on

the function space operator

id <-> Id

cleanup for Fun.thy:
merged Update.{thy|ML} into Fun.{thy|ML}
moved o_def from HOL.thy to Fun.thy
added Id_def to Fun.thy
moved image_compose from Set.ML to Fun.ML
moved o_apply and o_assoc from simpdata.ML to Fun.ML
moved fun_upd_same and fun_upd_other (from Map.ML) to Fun.ML
added fun_upd_twist to Fun.ML

Added a few lemmas.
Renamed expand_const -> split_const.

New theory of the inverse image of a function

New Blast_tac (and minor tidying...)

moved inj and surj from Set to Fun and Inv -> inv.

expanded tabs; renamed subtype to typedef;
incorporated Konrad's changes

new version of HOL with curried function application