clarified status of legacy input abbreviations

added simp rules

moved lemma to more appropriate place

ran isabelle update_op on all sources

more symbols;

tuning imports

"split add" -> "split"

bundle lifting_syntax;

Added code generation for PMFs

isabelle update_cartouches -c -t;

add various lemmas

proper qualified naming;

misc tuning and modernization;

isabelle update_cartouches;

more transfer rules

add lemmas about functions on option

tuned proof

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

Added Option.bind_split{,_asm,s}

modernized header uniformly as section;

updated news

tuned imports

renamed BNF theories

--HG--
rename : src/HOL/BNF_Comp.thy => src/HOL/BNF_Composition.thy
rename : src/HOL/BNF_FP_Base.thy => src/HOL/BNF_Fixpoint_Base.thy
rename : src/HOL/BNF_GFP.thy => src/HOL/BNF_Greatest_Fixpoint.thy
rename : src/HOL/BNF_LFP.thy => src/HOL/BNF_Least_Fixpoint.thy

renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place

--HG--
rename : src/HOL/Datatype.thy => src/HOL/Old_Datatype.thy
rename : src/HOL/Tools/Function/size.ML => src/HOL/Tools/Function/old_size.ML
rename : src/HOL/Tools/Datatype/datatype.ML => src/HOL/Tools/Old_Datatype/old_datatype.ML
rename : src/HOL/Tools/Datatype/datatype_aux.ML => src/HOL/Tools/Old_Datatype/old_datatype_aux.ML
rename : src/HOL/Tools/Datatype/datatype_codegen.ML => src/HOL/Tools/Old_Datatype/old_datatype_codegen.ML
rename : src/HOL/Tools/Datatype/datatype_data.ML => src/HOL/Tools/Old_Datatype/old_datatype_data.ML
rename : src/HOL/Tools/Datatype/datatype_prop.ML => src/HOL/Tools/Old_Datatype/old_datatype_prop.ML
rename : src/HOL/Tools/Datatype/datatype_realizer.ML => src/HOL/Tools/Old_Datatype/old_datatype_realizer.ML
rename : src/HOL/Tools/Datatype/primrec.ML => src/HOL/Tools/Old_Datatype/old_primrec.ML
rename : src/HOL/Tools/Datatype/rep_datatype.ML => src/HOL/Tools/Old_Datatype/old_rep_datatype.ML

tuned whitespace, to make datatype definitions slightly less intimidating

got rid of '=:' squiggly

rationalized internals

renamed 'datatype_new_compat' to 'datatype_compat'

folded 'Option.set' into BNF-generated 'set_option'

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'

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 '{prod,sum,bool,unit}_case' to 'case_...'

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'

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

swapped dependencies of 'Finite_Set' and 'Option' (to move BNF up)

Added symmetric code_unfold-lemmas for null and is_none

move useful lemmas to Main

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

--HG--
extra : rebase_source : ff8027ac9606264aa4b2d4f8da037c426a3db98b

modifiers for classical wrappers operate on Proof.context instead of claset;

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

combinator Option.these

added congruence rules for Option.{map|bind}

"enriched_type" replaces less specific "type_lifting"

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

tuned type_lifting declarations

replace `type_mapper` by the more adequate `type_lifting`

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

mapper for option type

Haskell == is infix, not infixl

more antiquotations;

removed duplicate lemma

added Option.bind

renamed class/constant eq to equal; tuned some instantiations

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

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

split off theory Big_Operators from theory Finite_Set

--HG--
rename : src/HOL/Finite_Set.thy => src/HOL/Big_Operators.thy

some syntax setup for Scala

prefer code_inline over code_unfold; use code_unfold_post where appropriate

code attributes use common underscore convention

preprocessing must consider eq

lemmas by Andreas Lochbihler

moved instance option :: finite to Option.thy

Option.thy

re-eliminated Option.thy

split off Option theory

theory Option has been assimilated by Datatype;

the is now defined using primrec, avoiding explicit use of arbitrary.

AddIffs[not_None_eq];
made wrapper ospec really safe

Adapted to new datatype package.

added o2s

replaced 8bit characters

added the, option_map, and case analysis theorems

Moved Option out of IOA into core HOL