more specific keyword kinds;

isabelle update -u path_cartouches;

isabelle update -u control_cartouches;

print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'

tuned proofs;

Isar proof of Schroeder_Bernstein without using Hilbert_Choice (and metis);

clarified lfp/gfp statements and proofs;

added lemma;

don't expose internal construction in the coinduction rule for mutual coinductive predicates

misc tuning and modernization;

add lemmas contributed by Peter Gammie

tuned proofs -- avoid unstructured calculation;

misc tuning and modernization;

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

prefer symbols for "Union", "Inter";

isabelle update_cartouches -c -t;

fewer aliases for toplevel theorem statements;

eliminated \<Colon>;

isabelle update_cartouches;

add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer

--HG--
extra : rebase_source : b8f67b531a15510b1f468145a6194cf68875d262

strengthened lfp_ordinal_induct; added dual gfp variant

--HG--
extra : rebase_source : faeeb4ca40153738fce12fd2ab3522b788b18d32

add rules for least/greatest fixed point calculus

--HG--
extra : rebase_source : 01de51c6333edb1f57ff734be51f94050a97d40a

modernized header uniformly as section;

modernized setup;

renamed 'rep_datatype' to 'old_rep_datatype' (HOL)

fixed infinite loops in 'register' functions + more uniform API

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

discontinued somewhat pointless "thy_script" keyword kind;

less flex-flex pairs

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)

generalized datatype code generation code so that it works with old-style and new-style (co)datatypes (as long as they are not local)

moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it

syntax translations always depend on context;

tuned pretty layout: avoid nested Pretty.string_of, which merely happens to work with Isabelle/jEdit since formatting is delegated to Scala side;
declare command "print_case_translations" where it is actually defined;

disallow coercions to interfere with case translations

allow redundant cases in the list comprehension translation

special constant to prevent eta-contraction of the check-phase syntax of case translations

separate data used for case translation from the datatype package

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

added 'print_inductives' command;

prefer ML_file over old uses;

removed ML module DSeq which was a part of the ancient code generator (cf. 58e33a125f32)

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

declare minor keywords via theory header;

reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008";
tuned proofs;

clarified modules that contribute to datatype package;

prefer Name.context operations;

clarified modules that contribute to datatype package;

--HG--
rename : src/HOL/Tools/primrec.ML => src/HOL/Tools/Datatype/primrec.ML

clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;

separate rep_datatype.ML;
tuned signature;

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

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;

tuned

dropped old primrec package

moved inductive_codegen to place where product type is available; tuned structure name

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

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

Streamlined setup for monotonicity rules (no longer requires classical rules).

renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on 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 : 1966817fe0f19fbb990981dff02b8c829770c173

bootstrap datatype_rep_proofs in Datatype.thy (avoids unchecked dynamic name references)

--HG--
extra : rebase_source : f0d460622d846c9dca7630d50d097b93aa8008eb

stripped legacy ML bindings

inter and union are mere abbreviations for inf and sup

Inter and Union are mere abbreviations for Inf and Sup

moved Inductive.myinv to Fun.inv; tuned

tuned interfaces of datatype module

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

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

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

eliminated OldTerm.add_term_free_names;

moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;

Instantiated some rules to avoid problems with HO unification.

Theorem Inductive.lfp_ordinal_induct generalized to complete lattices

added new primrec package

simplified infrastructure for code generator operational equality

adjustions to due to instance target

integrated FixedPoint into Inductive

tuned datatype_codegen setup

removed dead code;

datatype interpretators for size and datatype_realizer

introduced generic concepts for theory interpretators

separated code for inductive sequences from inductive_codegen.ML

Final mods for list comprehension

Added new package for inductive sets.

clarified import

Fixed problem with patterns in lambdas

Added pattern maatching for lambda abstraction

tuned proofs: avoid implicit prems;

moved recfun_codegen.ML to Code_Generator.thy

simplified DataFun interfaces;

Added datatype_case.

dropped lemma duplicates in HOL.thy

Added new package for inductive definitions, moved old package
to old_inductive_package.ML

added auxiliary lemma for code generation 2

added DatatypeHooks

updated auxiliary facts for induct method;

import FixedPoint instead of Gfp

migrated theory headers to new format

import -> imports

New theory header syntax.

Merged in license change from Isabelle2004

Added InductiveRealizer package.

Added file Tools/datatype_realizer.ML

include theory Record (tuned dependencies);

Moved code generator setup from Recdef to Inductive.

tuned;

use induct_rulify2;

moved InductMethod.setup to theory HOL;

generic induct_method.ML;
tuned;

tuned;

private "myinv" (uses "The" instead of "Eps");

Inductive definitions are now introduced earlier in the theory hierarchy.

added if_def2

added inductive_conj;

simplified atomize;
added inductive_rulify2 (to accomodate malformed induction rules);

inductive_atomize, inductive_rulify;

declare trancl rules;

*** empty log message ***

Added setup for primrec theory data.

require NatDef;

early setup of induct_method;

Monotonicity rules for inductive definitions can now be added to a theory via
attribute "mono".

load / setup datatype package;

proper bootstrap of HOL theory and packages;

'HOL/inductive' theory data;

tuned Inductive.thy;

Adapted to new inductive definition package.

New dummy .thy files to document dependencies

Includes Sum.thy as a parent for mutual recursion

new version of HOL with curried function application