added lemmas

some lemmas about the lex ordering on lists, etc.

more lemmas

A few lemmas connected with orderings

new examples of BNF lifting across quotients using a new theory of confluence,
which simplifies the relator subdistributivity proof obligation
(a few new useful notions were added to HOL;
notably the symmetric and equivalence closures of a relation)

more lemmas

tuned proof

strengthened lemma

more lemmas

--HG--
extra : rebase_source : 3e2ac977160873ea4b0f5fb90c505d1a2c674b91

incorporated various material from the AFP into the distribution

--HG--
extra : rebase_source : 5e560f26b11abb81e42f7e18947eaa6c0d2e5837

tuned proofs -- eliminated odd case_tac;

new material about summations and powers, along with some tweaks

isabelle update -u control_cartouches;

more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
tuned signature;

added and tuned lemmas

replaced some ancient ASCII syntax

clarified status of legacy input abbreviations

tuned;

added lemmas

added simp-lemma

added simp-lemma

more [simp]

shuffle -> shuffles

avoid confusing precedences

simpler def

A few new results, elimination of duplicates and more use of "pairwise"

tuned whitespace

--HG--
extra : rebase_source : 709c3ecd12d88f399349a5ad01c12f6828116fea

removed ineffective code declarations

recovered HOL-Proofs-Lambda from 8aedca31957d: avoid problems with program extraction according to d136af442665;

de-applying

de-applying

more de-applying

Generalising and renaming some basic results

allow tuple patterns in list comprehensions

unused

First step to remove nonstandard "[x <- xs. P]" syntax: only input

--HG--
extra : amend_source : a2e6a2312b63a5ed1947d3302e43341c073c9f03

added lemmas

removed duplicates

added lemmas

cleaning up sorted

more sorted cleaning

cleaning up sorted

mv lemma

added lemmas

more lemmas

announce sorted changes

more efficient code

more "sorted" changes

new def of sorted and sorted_wrt

--HG--
extra : amend_source : 063fe8412a72415725783d8336fe89d3cd0ca676

reinstated old lemma name

removed asm "finite"

proper datatype for 8-bit characters

added lemma

added lemmas

added lemma

more symbols;

simplified def of stable

more symbols;

added lemmas

made sorted fun again

imported patch sorted

add lemma on lists from Falling_Factorial_Sum entry

standardized towards new-style formal comments: isabelle update_comments;

ran isabelle update_op on all sources

added lemmas

added min_list and arg_min_list

added lemmas

more lemmas

more symbols;

more lemmas

added lemma

remove trailing whitespaces in List

drop a superfluous assumption that was found by the find_unused_assms command

drop a superfluous assumption that was found by the find_unused_assms command and tune proof

drop a superfluous assumption that was found by the find_unused_assms command and tune proof

added [simp]

added lemmas, tuned spaces

relaxed assm

tuned imports

--HG--
extra : rebase_source : bc9797cb892085195c2d8662a7ca3896dd1e5011

two new simp rules

added lemma

added lemma; zip_with -> map2

introduced zip_with

added lemma

more facts on Map.map_of and List.zip

--HG--
extra : rebase_source : aabab8a4de88b4f4ff69c542f7e9d1c239fc1a0f

Some small lemmas about polynomials and FPSs

--HG--
extra : rebase_source : b31b5bb1a9508cf7149022396f1a2b51a88c8dc9

Added lemmas

added lemma

more reorganization around sorted_wrt

added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy

slightly generalized card_lists_distinct_length_eq; renamed specialized card_lists_distinct_length_eq to card_lists_distinct_length_eq'; tuned

revised lemma

generalized lemma

added lemma

reorganised material on sublists

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

added shuffle product to HOL/List

--HG--
extra : amend_source : f69971cd7b125b625e2945b41373d36d943083aa

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

tuned whitespace;

added lemma

setprod -> prod

setsum -> sum

more symbols;

tuned proofs;

added lemma

lists form a monoid

--HG--
extra : rebase_source : 77a5f131b508e3b830e862b73e440f223ae25e1e

add lemmas contributed by Peter Gammie

tuned proofs -- avoid unstructured calculation;

added missing transfer rule

more theorems

bundle lifting_syntax;

Various additions to polynomials, FPSs, Gamma function

added subtheory of longest common prefix

isabelle update_cartouches -c -t;

Moved material from AFP/Randomised_Social_Choice to distribution

eliminated use of empty "assms";

eliminated old 'def';
tuned comments;

moved

more canonical names

prefer abbreviations for compound operators INFIMUM and SUPREMUM

call the predicator of list list_all

isabelle update_cartouches -c -t;

added lemma

more uniform treatment of package internals;

Added some facts about polynomials

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

discontinued ASCII replacement syntax <->;

not_leE -> not_le_imp_less and other tidying

isabelle update_cartouches -c -t;

New theorems mostly from Peter Gammie

option "inductive_defs" controls exposure of def and mono facts;

reverted half-baken 7d1127ac2251

--HG--
extra : rebase_source : 457832304889dc2d80d98b8be1a7e19764f1c9dc

add various lemmas

qualifier is mandatory by default;

Keyword 'rewrites' identifies rewrite morphisms.

code abbreviation for mapping over a fixed range

--HG--
extra : rebase_source : ede20bd4497dbc9d290639d6c1abf8960f621d90

discontinued specific HTML syntax;

tuned proofs -- less legacy;

eliminated \<Colon>;

standardized some occurences of ancient "split" alias

--HG--
extra : rebase_source : 706ba501d5c0596a2bde6e46d42aa8464a91ede5

more lemmas on sorting and multisets (due to Thomas Sewell)

--HG--
extra : rebase_source : df9cf240f30d85ac4954aa584945beeef1d8de5c

isabelle update_cartouches;

prefer tactics with explicit context;

tuned proofs;

modernized name

more formal source, more PIDE markup;

tuned -- avoid odd rebinding of "ctxt" and "context";

tuned;

tuned;

added lemmas

tuned signature -- prefer qualified names;

add parametricity rules for monotone, fun_lub, and fun_ord

tuned;

added lemma

dropped redundant transfer rules (now proved and registered by datatype and plugins)

proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);

more complete fp_sugars for sum and prod;
tuned;
removed theorem duplicates;
removed obsolete Lifting_{Option,Product,Sum} theories

modernized header uniformly as section;

removed useless lemmas

tuned layout and proofs

updated news

enamed drop_Suc_conv_tl and nth_drop' to Cons_nth_drop_Suc

added various facts

silenced nonexhaustive primrec warnings

added lemmas

--HG--
extra : rebase_source : 9983f0122781b2719b4390818c18fedd04f9cbb5

separated listsum material

added lemmas

no need for 'set_simps' now that 'datatype_new' generates the desired 'set' property

add parametricity lemmas

reverse induction over nonempty lists

added lemmas

prefer ac_simps collections over separate name bindings for add and mult

reduced name variants for assoc and commute on plus and mult

fact consolidation

add lemma

added [simp]

reintroduced vital 'Thm.transfer'

reduces Sledgehammer dependencies

changed syntax of map: and rel: arguments to BNF-based datatypes

use 'where' clause for selector default value syntax

added List.union

tuned whitespace, to make datatype definitions slightly less intimidating

got rid of '=:' squiggly

added lemma

prefer plain ASCII / latex over not-so-universal Unicode;

move size hooks together, with new one preceding old one and sharing same theory data

more operations and lemmas

--HG--
extra : rebase_source : 8f5be7e0cdc09c667e66c2cda2c667d4da6e5f73

make list_all an abbreviation of pred_list - prevent duplication

simplify and fix theories thanks to 356a5efdb278

abstract Domainp in relator_domain rules => more natural statement of the rule

more appropriate name (Lifting.invariant -> eq_onp)

left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)

more qualified names;

elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION

normalising simp rules for compound operators

killed a few 'metis' calls

renamed 'fun_rel' to 'rel_fun'

renamed 'prod_rel' to 'rel_prod'

renamed 'set_rel' to 'rel_set'

renamed 'map_pair' to 'map_prod'

added function "List.extract"

load Metis a little later

adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'

merged 'List.set' with BNF-generated 'set'

delete or move now not necessary reflexivity rules due to 1726f46d2aa8

renamed 'datatype_new_compat' to 'datatype_compat'

folded 'rel_option' into 'option_rel'

folded 'list_all2' with the relator generated by 'datatype_new'

hide 'rel' name -- this one is waiting to be merged with 'list_all2'

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

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

merged 'List.map' and 'List.list.map'

tuning

adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
* * *
more transition of 'xxx_rec' to 'rec_xxx' and same for case
* * *
compile
* * *
'rename_tac's to avoid referring to generated names
* * *
more robust scripts with 'rename_tac'
* * *
'where' -> 'of'
* * *
'where' -> 'of'
* * *
renamed 'xxx_rec' to 'rec_xxx'

renamed 'nat_{case,rec}' to '{case,rec}_nat'

compatibility names

use new selector support to define 'the', 'hd', 'tl'

transformed 'option' and 'list' into new-style datatypes (but register them as old-style as well)
* * *
compile
* * *
tuned imports to prevent merge issues in 'Main'

avoid (now superfluous) indirect passing of constant names

prefer explicit code symbol type over ad-hoc name mangling

killed 'More_BNFs' by moving its various bits where they (now) belong

fundamental treatment of undefined vs. universally partial replaces code_abort

more abstract declaration of code attributes

prefer target-style syntaxx for sublocale

prefer more canonical names for lemmas on min/max

remove junk

rationalize imports

add predicate version of lexicographic order on lists

eliminiated neg_numeral in favour of - (numeral _)

add lemmas Suc_funpow and id_funpow to simpset; add lemma map_add_upt

--HG--
extra : rebase_source : 02e892232f20d46af3dd46c4047e264fc49d378b

port list comprehension simproc to 'Ctr_Sugar' abstraction

qualifed popular user space names

killed most "no_atp", to make Sledgehammer more complete

added code eqns for bounded LEAST operator

Added symmetric code_unfold-lemmas for null and is_none

added two functions to List (one contributed by Manuel Eberl)

added and tuned lemmas

list_to_set_comprehension: don't crash in case distinctions on datatypes with even number of constructors

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

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

move Lifting/Transfer relevant parts of Library/Quotient_* to Main

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

--HG--
extra : rebase_source : ff8027ac9606264aa4b2d4f8da037c426a3db98b

lifting for primitive definitions;
explicit conversions from and to lists of coefficients, used for generated code;
replaced recursion operator poly_rec by fold_coeffs, preferring function definitions for non-trivial recursions;
prefer pre-existing gcd operation for gcd

selection operator smallest_prime_beyond

weaker precendence of syntax for big intersection and union on sets

syntax translations always depend on context;

tuned signature;

more lemmas for sorted_list_of_set

tail recursive version of map, for code generation, optionally

tuned: unnamed contexts, interpretation and sublocale in locale target;
corrected slip in List.thy: setsum requires commmutativity

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

allow redundant cases in the list comprehension translation

centralized various multiset operations in theory multiset;
more conversions between multisets and lists respectively

--HG--
extra : rebase_source : 93a1492ea9887e2bb60374621b48587c8a351c80

explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts

fundamental revision of big operators on sets

provide common HOLogic.conj_conv and HOLogic.eq_conv;

just one HOLogic.Trueprop_conv, with regular exception CTERM;
tuned;

prefer stateless 'ML_val' for tests;

Sieve of Eratosthenes

simplified construction of upto_aux

tail recursive code for function "upto"

systematic conversions between nat and nibble/char;
more uniform approaches to execute operations on nibble/char

--HG--
extra : rebase_source : 982810ecce9e31070e2293715ed744c3b68ae21d

abandoned theory Plain

--HG--
extra : rebase_source : 6f5a395a55e8879386d1f79ab252c6fc2aca7dc5

combinator List.those;
simprule for case distinction on Option.map expression

separate data used for case translation from the datatype package

case translations performed in a separate check phase (with adjustments by traytel)

unified layout of defs

avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time) -- relevant for any application using it, e.g. small paper sessions;

add Countable_Set theory

adjusting proofs as the set_comprehension_pointfree simproc breaks some existing proofs

moved quite generic material from theory Enum to more appropriate places

--HG--
extra : rebase_source : aada8b3ff46b715201e6ecbb53f390c25461ebd9

Renamed {left,right}_distrib to distrib_{right,left}.

tail-recursive implementation for length

rename Set.project to Set.filter - more appropriate name

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;

prefer eta-expanded code equations for fold, to accomodate tail recursion optimisation in Scala

more set operations expressed by Finite_Set.fold

making sorted_list_of_set executable

strengthen rule list_all2_induct

abandoned almost redundant *_foldr lemmas

tuned

no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code

renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")

reverted to canonical name

Functions and lemmas by Christian Sternagel

merged fork with new numeral representation (see NEWS)

tuned proofs -- eliminated pointless chaining of facts after 'interpret';

tuned proofs

converting "set [...]" to "{...}" in evaluation results

one general list_all2_update_cong instead of two special ones

moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy

--HG--
extra : rebase_source : ed15629634477aff0a8efea30547f496c70907ad

moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy

removing unnecessary premises in theorems of List theory

more specification of the quotient package in IsarRef

use 'primrec' to define "rotate1", for uniformity (and to help first-order tools that rely on "Spec_Rules")

removed fact that confuses SPASS -- better rely on "rev_rev_ident", which is stronger and more ATP friendly

adding code equation for Relation.image; adding map_project as correspondence to map_filter on lists

another try to improve code generation of set equality (cf. da32cf32c0c7)

adding a minimally refined equality on sets for code generation

adding code equation for setsum

generalize type of List.listrel

adding code generation for some list relations

pred_subset/equals_eq are now standard pred_set_conv rules

massaging of code setup for sets

--HG--
extra : rebase_source : d88e8eabd9d4067b161ff0d4e077408f826712f8

corrected slip

restore convenient code_abbrev declarations (particulary important if List.set is not the formal constructor for sets)

moved lemmas about List.set and set operations to List theory

--HG--
extra : rebase_source : acbab180eefc1dba0e1ed3007e87bf7039ff4047

farewell to theory More_List

--HG--
extra : rebase_source : 1faf1250c2e2d8499bbb199b166580783121c606

improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
tuned;

incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)

--HG--
extra : rebase_source : 022f0a101d8cefadae578fbbd0c1fd8958d910af

improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
tuned;

qualified Finite_Set.fold

attribute code_abbrev superseedes code_unfold_post; tuned text

--HG--
extra : rebase_source : 151b02554e820ef4b9e8f43b9a53512fbfc0e053

dropped fact whose names clash with corresponding facts on canonical fold

dropped obsolete lemma member_set

add lemmas

clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;

added lemmas

add induction rule for list_all2

removing special code generator setup for hd and last function because this causes problems with quickcheck narrowing as the Haskell Prelude functions throw errors that cannot be caught instead of PatternFail exceptions

cardinality of sets of lists

eliminated obsolete "standard";

removing old code generator setup for lists

adding lemma to List library for executable equation of the (refl) transitive closure

tuned proofs

added lemma motivated by a more specific lemma in the AFP-KBPs theories

renamed Complete_Lattices lemmas, removed legacy names

new fastforce replacing fastsimp - less confusing name

added two lemmas about "distinct" to help Sledgehammer

adding list_size_append (thanks to Rene Thiemann)

strengthening list_size_pointwise (thanks to Rene Thiemann)

moved recdef package to HOL/Library/Old_Recdef.thy

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

modernized some simproc setup;

new Datatype.info_of_constr with strict behaviour wrt. to overloaded constructors -- side effect: function package correctly identifies 0::int as a non-constructor;
renamed old version to info_of_constr_permissive, reflecting its semantics

discontinued Name.variant to emphasize that this is old-style / indirect;

names of fold_set locales resemble name of characteristic property more closely

use pointfree characterisation for fold_set locale

add a lemma about commutative append to List.thy

removed assumption from lemma List.take_add

eliminated Codegen.mode in favour of explicit argument;

modernized structure Proof_Context;

prefer local name spaces;
tuned signatures;
tuned;

separate structure Term_Position;
dismantled remains of structure Type_Ext;

actually check list comprehension examples;

list comprehension: strip positions where the translation cannot handle them right now;

more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;

added lemma

added simp lemma nth_Cons_pos to List

explicit is better than implicit;

"enriched_type" replaces less specific "type_lifting"

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

adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs

tuned type_lifting declarations

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

primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`

replace `type_mapper` by the more adequate `type_lifting`

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

gave more standard finite set rules simp and intro attribute

adding code equations for EX1 on finite types

mapper for list type; map_pair replaces prod_fun

code eqn for slice was missing; redefined splice with fun

added two lemmas about injectivity of concat to the list theory

lemmas sorted_map_same, sorted_same

added lemmas about listrel(1)

sorting: avoid _key suffix if lemma applies both to simple and generalized variant; generalized insort_insert to insort_insert_key; additional lemmas

include ATP in theory List -- avoid theory edge by-passing the prominent list theory

dropped (almost) redundant distinct.induct rule; distinct_simps again named distinct.simps

nat_number -> eval_nat_numeral

move Metis into Plain

--HG--
rename : src/HOL/Tools/Sledgehammer/metis_reconstruct.ML => src/HOL/Tools/Metis/metis_reconstruct.ML
rename : src/HOL/Tools/Sledgehammer/metis_tactics.ML => src/HOL/Tools/Metis/metis_tactics.ML
rename : src/HOL/Tools/Sledgehammer/metis_translate.ML => src/HOL/Tools/Metis/metis_translate.ML

turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs

localized listsum

lemma remdups_map_remdups

more lists lemmas

new lemma

generalized lemma insort_remove1 to insort_key_remove1

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

Haskell == is infix, not infixl

added lemma

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

Add filter_remove1

renamed class/constant eq to equal; tuned some instantiations

renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;

Scala: subtle difference in printing strings vs. complex mixfix syntax

dropped superfluous [code del]s

put section on distinctness before listsum; refined code generation operations; dropped ancient infix mem

tuned set_replicate lemmas

added lemmas

made List.thy a join point in the theory graph

rev is reverse in Haskell

use various predefined Haskell operations when generating code

declare lexn.simps [code del]

induction over non-empty lists

more convenient order of code equations

more lemmas

turned old-style mem into an input abbreviation

added listsum lemmas

Multiset: renamed, added and tuned lemmas;
Permutation: replaced local "remove" by List.remove1

added lemmas concerning last, butlast, insort

lemmas concerning remdups

Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.

more convenient equations for zip

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

Respectfullness and preservation of list_rel

now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"

renamed "ATP_Linkup" theory to "Sledgehammer"

--HG--
rename : src/HOL/ATP_Linkup.thy => src/HOL/Sledgehammer.thy

added insort_insert

moved lemma map_sorted_distinct_set_unique

Slightly generalised a theorem

adapted to authentic syntax;

lemma distinct_insert

added lemma

moved remaning class operations from Algebras.thy to Groups.thy

get rid of many duplicate simp rule warnings

added lemma

more lemmas about sort(_key)

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

more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS

canonical insert operation; generalized lemma foldl_apply_inv to foldl_apply

Added transpose_rectangle, when the input list is rectangular.

Add transpose to the List-theory.

dropped some old primrecs and some constdefs

some syntax setup for Scala

same_append_eq / append_same_eq are now used for simplifying induction rules.

avoid dependency on implicit dest rule predicate1D in proofs

tuned lattices theory fragements; generlized some lemmas from sets to lattices

added remdups_filter lemma

modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML

--HG--
rename : src/HOL/Tools/Datatype/datatype.ML => src/HOL/Tools/Datatype/datatype_data.ML
extra : rebase_source : 552900fbf6783258465fa5000202d52cf1f99a1f

Remove map_compose, replaced by map_map

New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key

tuned imports

moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly

eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;

lemma relating fold1 and foldl; code_unfold rules for Inf_fin, Sup_fin, Min, Max, Inf, Sup

code generator: quantifiers over {_.._::int} and {_..<_::nat}
are now translated into (tail recursive) loops - no list is built.

tuned code generation for lists

got rid of complicated class finite_intvl_succ and defined "upto" directly on int, the only instance of the class.

more antiquotations;

Made "prime" executable

made upt/upto executable on nat/int by simp

prefer code_inline over code_unfold; use code_unfold_post where appropriate

code attributes use common underscore convention

lemma foldl_apply_inv

tuned interfaces of datatype module

discontinued ancient tradition to suffix certain ML module names with "_package"

--HG--
rename : src/HOL/Import/import_package.ML => src/HOL/Import/import.ML
rename : src/HOL/Nominal/nominal_package.ML => src/HOL/Nominal/nominal.ML
rename : src/HOL/Tools/specification_package.ML => src/HOL/Tools/choice_specification.ML
rename : src/HOL/Tools/datatype_package/datatype_package.ML => src/HOL/Tools/datatype_package/datatype.ML
rename : src/HOL/Tools/function_package/fundef_package.ML => src/HOL/Tools/function_package/fundef.ML
rename : src/HOL/Tools/inductive_package.ML => src/HOL/Tools/inductive.ML
rename : src/HOL/Tools/inductive_set_package.ML => src/HOL/Tools/inductive_set.ML
rename : src/HOL/Tools/old_primrec_package.ML => src/HOL/Tools/old_primrec.ML
rename : src/HOL/Tools/primrec_package.ML => src/HOL/Tools/primrec.ML
rename : src/HOL/Tools/recdef_package.ML => src/HOL/Tools/recdef.ML
rename : src/HOL/Tools/record_package.ML => src/HOL/Tools/record.ML
rename : src/HOL/Tools/typecopy_package.ML => src/HOL/Tools/typecopy.ML
rename : src/HOL/Tools/typedef_package.ML => src/HOL/Tools/typedef.ML

two finiteness lemmas by Robert Himmelmann

lemma about List.foldl and Finite_Set.fold

Added theorems about distinct & concat, map & replicate and concat & replicate

more lemmas

listsum lemmas

new lemma

new lemma

preprocessing must consider eq

lemmas by Andreas Lochbihler

more lemmas

proper structures for list and string code generation stuff

refined HOL string theories and corresponding ML fragments

added listsum lemmas

funpow and relpow with shared "^^" syntax

power operation on functions with syntax o^; power operation on relations with syntax ^^

separated funpow, relpow from power on monoids

Merge.

name changes

revert some Suc 0 lemmas back to their original forms; added some simp rules for (1::nat)

make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules

defensive implementation of pretty serialisation of lists and characters

Added nitpick attribute, and fixed typo.

const_name antiquotations

code theorems for nth, list_update

code theorems for nth, list_update

authentic syntax for List.nth

dropped global Nil/Append interpretation

sorted_take, sorted_drop

migrated class package to new locale implementation

eliminated OldTerm.add_term_free_names;

moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;

Conversion of HOL-Main and ZF to new locales.

cleaned up binding module and related code

tuned unfold_locales invocation

added length_unique operation for code generation

explicit check for pattern discipline before code translation

code identifier namings are no longer imperative

added lemmas

`code func` now just `code`

established canonical argument order in SML code generators

dropped superfluous if

removed obsolete name convention "func"

discontinued special treatment of op = vs. eq_class.eq

back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;

a sophisticated char/nibble conversion combinator

explicit size of characters

distributed literal code generation out of central infrastructure

It appears that the code generator (Stefan's) needs some laws that appear superfluous: {..n} = set ...

cleaned up code generation for {.._} and {..<_}
moved lemmas into SetInterval where they belong

restructured code generation of literals

restructured and split code serializer module

made setsum executable on int.

added removeAll

@{lemma}: 'by' keyword;

established Plain theory and image

removed some dubious code lemmas

Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
set print_mode and margin appropriately.

Measure functions can now be declared via special rules, allowing for a
prolog-style generation of measure functions for a specific type.

- Explicitely applied predicate1I in a few proofs, because it is no longer
part of the claset
- Explicitely passed pred_subset_eq and pred_equals_eq as an argument to the
to_set attribute, because it is no longer applied automatically

Added documentation

* New attribute "termination_simp": Simp rules for termination proofs
* General lemmas about list_size

dropped some metis calls

move lemmas from Word/BinBoolList.thy to List.thy

replaced 'ML_setup' by 'ML';

restructuring; explicit case names for rule list_induct2

removed duplicate lemmas;

char and nibble are finite

Added useful general lemmas from the work with the HeapMonad

more lemmas

dropped superfluous code theorems

New interface for test data generators.

swtiched ATP_Linkup and PreList in theory hierarchy

instantiation target rather than legacy instance

temporary code generator work arounds

authentic primrec