standardized towards new-style formal comments: isabelle update_comments;

misc tuning and modernization;

misc tuning and modernization;

isabelle update_cartouches -c -t;

eliminated \<Colon>;

isabelle update_cartouches;

modernized header uniformly as section;

renamed 'rep_datatype' to 'old_rep_datatype' (HOL)

added 'plugins' option to control which hooks are enabled

renamed 'map_sum' to 'sum_map'

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

moved 'primrec' up (for real this time) and removed temporary 'old_primrec'

renamed old 'primrec' to 'old_primrec' (until the new 'primrec' can be moved above 'Nat' in the theory dependencies)

aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax

renamed 'wrap_free_constructors' to 'free_constructors' (cf. 'functor', 'bnf', etc.)

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

tuning

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

avoid duplicate 'case' definitions by first looking up 'Ctr_Sugar'

se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
* * *
cleaner simp/iff sets

move useful lemmas to Main

moved quite generic material from theory Enum to more appropriate places

--HG--
extra : rebase_source : aada8b3ff46b715201e6ecbb53f390c25461ebd9

discontinued obsolete typedef (open) syntax;

prefer typedef without extra definition and alternative name;
tuned proofs;

hide typedef-generated constants Product_Type.prod and Sum_Type.sum

"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 sum type

hide Sum_Type.Plus

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

"prod" and "sum" replace "*" and "+" respectively

tuned quotes, antiquotations and whitespace

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

tuned whitespace

modernized; dropped ancient constant Part

--HG--
extra : rebase_source : 0faf72a7a9ce8bddd68df34e5b385b26d032c146

centralized sum type matter in Sum_Type.thy

--HG--
extra : rebase_source : e3b0c15d9ae3766c59620daf0f992723a16b9206

lemmas by Andreas Lochbihler

removed duplicate sum_case used only by function package;
moved projections;
hide (open)

move lemmas from Numeral_Type.thy to other theories

arbitrary is undefined

rep_datatype command now takes list of constructors as input arguments

simplified infrastructure for code generator operational equality

tuned

Moving "FunDef" up in the HOL development graph, since it is independent from "Recdef" and "Datatype" now.

*** empty log message ***

dropped eq const

moved HOL code generator setup to Code_Generator

added operational equality

simplified code generator setup

improved code generator devarification

classical rules must have names for ATP integration

new lemma

converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global

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

`` -> and ``` -> ``

*** empty log message ***