clarified context;
avoid Unsynchronized.ref;

isabelle update_cartouches;

swap False to the right in assumptions to be eliminated at the right end

undid 6d7b7a037e8d

new ==> simp rule

prepared for more meta-simp rules (by Stefan Berghofer)

local setup of induction tools, with restricted access to auxiliary consts;
proper antiquotations for formerly inaccessible consts;

modernized header uniformly as section;

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

'code' is needed for extraction datatype

generate 'code' attribute only if 'code' plugin is enabled

disable datatype 'plugins' for internal types

updated news

use 'datatype_new'

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

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

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'

just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;

prefer ML_file over old uses;

Adapted to new format of proof terms containing explicit proofs of class membership.

Expand proofs of induct_atomize'/rulify'.

eliminated dead code;

add_expand_thm: explicit indication of is_def instead of fragile heuristic, tuned signature;
explicit extraction_expand vs. extraction_expand_def attribute;

Made Option a separate theory and renamed option_map to Option.map

Adapted to encoding of sets as predicates.

rewrite_proof: simplified simprocs (no name required);

default replaces arbitrary

Added TrueE to extraction_expand.

re-eliminated Option.thy

split off theory Option for benefit of code generator

Added meta_spec to extraction_expand.

added eq_True eq_False True_implies_equals to extraction_expand

setup: theory -> theory;

removed obsolete induct_atomize_old;

updated auxiliary facts for induct method;

refer to theory instead of low-level tsig;

migrated theory headers to new format

tuned;

Deleted Library.option type.

Realizer for exE now uses let instead of case.

import -> imports

New theory header syntax.

Merged in license change from Isabelle2004

Prepared for extended identifiers (\<alpha>, etc.)

induct_impliesI is now unfolded.

Tuned realizer for exE rule, to avoid blowup of extracted program.

Changed format of realizers / correctness proofs.

Added elim_vars to preprocessor.

Removed (now unneeded) declaration of realizers for induction on natural numbers.

Removed reference to theory NatDef.

Added theory for setting up program extraction.