Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)

--HG--
extra : amend_source : fa78190ac2ee02ba33d22a4ee58362bc893ff097

Changes to complete distributive lattices due to Viorel Preoteasa

more symbols;

ran isabelle update_op on all sources

more symbols;

clarified uniqueness criterion for euclidean rings

--HG--
extra : rebase_source : 3f8d28b5e69282e9e5f36f72ad0d4d2e551ca7ab

euclidean rings need no normalization

--HG--
extra : rebase_source : 7f2e3f676b513d6c59f526f099be30240183bf05

abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel

--HG--
extra : rebase_source : c6612d6016d811043143eafb7a671631287494a1

reorganised material on sublists

--HG--
rename : src/HOL/Library/Sublist_Order.thy => src/HOL/Library/Subseq_Order.thy
extra : amend_source : e295fcfca4d0d9db4c5591741cb62b62bb340c87

more fine-grained type class hierarchy for div and mod

--HG--
extra : rebase_source : fffbeef99e834ca17596f478178e94bed8a014bc

suitable logical type class for abs, sgn

--HG--
extra : rebase_source : 27e95dd7f038f114d0cad11ec69599a166229041

syntactic type class for operation mod named after mod;
simplified assumptions of type class semiring_div

--HG--
extra : rebase_source : 3714be7474835787b2a513b731c9864d1ac9d2c4

more canonical names

prefer abbreviations for compound operators INFIMUM and SUPREMUM

isabelle update_cartouches -c -t;

tuned proofs -- less legacy;

eliminated \<Colon>;

isabelle update_cartouches;

uniform _ div _ as infix syntax for ring division

--HG--
extra : rebase_source : c4a1892078772c7ce9af33ad66e2abfefe7adea9

separate class for division operator, with particular syntax added in more specific classes

given up separate type classes demanding `inverse 0 = 0`

tuned signature -- prefer qualified names;

modernized header uniformly as section;

augmented and tuned facts on even/odd and division

Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;

specialized specification: avoid trivial instances

added 'extraction' plugins -- this might help 'HOL-Proofs'

disable datatype 'plugins' for internal types

updated news

use 'datatype_new' in 'Main'

separated listsum material

add algebraic type class instances for Enum.finite* types

add complete_lattice instances for Enum.finite_* types such that quickcheck deals with lattice class operations

added [simp]

moved 'bacc' back to 'Enum' (cf. 744934b818c7) -- reduces baggage loaded by 'Hilbert_Choice'

fundamental treatment of undefined vs. universally partial replaces code_abort

qualifed popular user space names

killed more "no_atp"s

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

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

--HG--
extra : rebase_source : ff8027ac9606264aa4b2d4f8da037c426a3db98b

providing a custom code equation for vimage to overwrite the vimage definition that would be rewritten by set_comprehension_pointfree simproc in the code preprocessor to an non-terminating code equation

incorporated constant chars into instantiation proof for enum;
tuned proofs for properties on enum of chars;
swapped theory dependency of Enum.thy and String.thy

tailored enum specification towards simple instantiation;
tuned enum instantiations

--HG--
extra : rebase_source : 0b8e3e6fb67c5a5bf29b205ea3072f7927d6dc6b

refined internal structure of Enum.thy

--HG--
extra : rebase_source : e1ee78f9065555b71380d5352e73c013e17e11ff

moved quite generic material from theory Enum to more appropriate places

--HG--
extra : rebase_source : aada8b3ff46b715201e6ecbb53f390c25461ebd9

some special code equations for Id with class constraint enum after adding the set comprehension simproc to the code preprocessing

tuned proofs, less guesswork;

rephrase lemma card_Pow using '2' instead of 'Suc (Suc 0)'

adding code equations for max_extp and mlex

adding code equation for rtranclp in Enum

adding code equation for max_ext

adding code equation for tranclp

an executable version of accessible part (only for finite types yet)

evaluation of THE with a non-singleton set raises a Match exception during the evaluation to yield a potential counterexample in quickcheck.

adding code equation for Collect on finite types

enum type class instance for `set`; dropped misfitting code lemma for trancl

moved sublists to More_List.thy

avoid very specific code equation for card; corrected spelling

--HG--
extra : rebase_source : 7a43ff22845a7caa93989e5f5ab5908190833404

bouned transitive closure

--HG--
extra : rebase_source : 3d0df473619b9c72b32a96ed4951a34dd2ad6c82

tune text for document generation

adding code equations for cardinality and (reflexive) transitive closure on finite types

adding an executable THE operator on finite types

adding a smarter enumeration scheme for finite functions

adding more efficient implementations for quantifiers in Enum

adding shorter output syntax for the finite types of quickcheck

changed order of lemmas to overwrite the general code equation with the nbe-specific one

removing Enum.in_enum from the claset

hiding enum

hiding the constants

adding code equations for EX1 on finite types

adding code equation for function equality; adding some instantiations for the finite types

adding Enum to HOL-Main image and removing it from HOL-Library

moving Enum theory from HOL/Library to HOL

--HG--
rename : src/HOL/Library/Enum.thy => src/HOL/Enum.thy