more specific keyword kinds;

isabelle update -u path_cartouches;

more symbols;

print_record: diagnostic printing of record definitions

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

isabelle update_cartouches -c -t;

isabelle update_cartouches;

modernized header uniformly as section;

updated news

use 'datatype_new' in 'Main'

modernized theory setup;

moved 'Quickcheck_Narrowing' further down the theory graph

make it possible to load Quickcheck exhaustive & narrowing in parallel

tuning

killed most "no_atp", to make Sledgehammer more complete

abandoned theory Plain

--HG--
extra : rebase_source : 6f5a395a55e8879386d1f79ab252c6fc2aca7dc5

prefer ML_file over old uses;

specialised fact in the Record theory should not be appear in proofs discovered by sledgehammer

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

tuned proofs

adding theory Quickcheck_Narrowing to HOL-Main image

adding creation of exhaustive generators for records; simplifying dependencies in Main theory

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

removed separate quickcheck_record module

dropped make_/dest_ naming convention

eliminated typecopy interpretation

moved Record.thy from session Plain to Main; avoid variable name acc

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

simplified/clarified record translations;

moved generic update_name to Pure syntax -- not specific to HOL/record;

tuned;

tuned document;

prefer prefix "iso" over potentially misleading "is"; tuned

substantial simplification restores code generation

eliminated dead code, redundant bindings and parameters;
use === term operator, which is defined here;
handle Type.TYPE_MATCH, not arbitrary exceptions;
misc tuning and simplification;

replaced meta_iffD2 by existing Drule.equal_elim_rule2;
replaced SymSymTab by existing Symreltab;
more antiquotations;
eliminated old-style Library.foldl, Library.foldl_map;
tuned;

tuned header;

Fix unescaped expressions breaking latex output in Record.thy

Expressions containing _ and ^ need to be adjusted or antiquoted in
text comments for latex compatibility. This is in fact a little
annoying, since it makes the comment less readable in both source
and HTML form.

Initial response to feedback from Norbert, Makarius on record patch

As Norbert recommended, the IsTuple.thy and istuple_support.ML files
have been integrated into Record.thy and record.ML. I haven't merged
the structures - record.ML now contains Record and IsTupleSupport.

Some of the cosmetic changes Makarius requested have been made,
including renaming variables with camel-case and run-together names
and removing the tab character from the Author: line. Constants are
defined with definition rather than constdefs. The split_ex_prf
inner function has been cleaned up.

Simplification of various aspects of the IsTuple component
of the new record package. Extensive documentation added in
IsTuple.thy - it should now be possible to figure out what's
going on from the sources supplied.

Record patch imported and working.

Initial attempt at porting record update to repository Isabelle.

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

replaced K_record by lambda term %x. c

added header;

reverted to classical syntax for K_record

Isar definitions are now added explicitly to code theorem table

field-update in records is generalised to take a function on the field
rather than the new value.

avoid home-grown meta_allE;

migrated theory headers to new format

tuned;

import -> imports

New theory header syntax.

tuned;

reimplementation of HOL records; only one type is created for
each record extension, instead of one type for each field. See NEWS.

Added split_paired_All rule for splitting variables bound by
object-level universal quantifiers.

simplified locale predicates;

predicate defs via locales;

removed "more" class;

tuned;

proper setup for abstract product types;

abstract product types;

_constify;

fix problem with user translations by making field names appear as consts;

added "_update_name" and parse_translation;

more "xsymbols" syntax;

intro_classes by default;

more symbolic syntax (currently "input");

\<dots> syntax;

proper bootstrap of HOL theory and packages;

tuned block indent;

Datatype instead of Prod;

removed global_names flag;

added type and update syntax;

changed {: :} syntax to (| |);

Extensible records with structural subtyping in HOL. See
Tools/record_package.ML for the actual implementation.