removed dead code; tuned;

more uniform ML keyword markup; tuned;

merged

tuned;

clarified Isabelle/ML strings;

refined ML keyword styles;

isabelle-ml mode with separate token marker; clarified ML_Lex.gap_start: end-of-input counts as single newline;

partial scans via ML_Lex.tokenize_context; simplified ML_char: no gaps (hardly relevant in practice); tuned;

proper signature; removed dead code;

lexical syntax for SML (in Scala); tuned;

tuned;

removed dead code;

tuned signature (in accordance to ML version);

tuned proofs;

tuned signature -- separate Lexicon from Parsers (in accordance to ML version);

prefer latest ProofGeneral-4.2-1 by default;

updated thy_info.dependencies;

tuned message;

more integrity checks of theory names vs. full node names;

abstract type must be a type constructor; check it

generate proper 'DtRec' indices in 'datatype_new_compat' for the case where some types are duplicated

better handling of recursion through functions

added examples/tests

tuned code to allow mutualized corecursion through different functions with the same target type

removed assumption in 'primrec_new' that a given constructor can only occur once

generate unique names

allow different functions to recurse on the same type, like in the old package

improved 'datatype_new_compat': generate more fixpoint equations for types like 'datatype_new x = C (x list) (x list)' (here, one equation for each x list instead of a single for both), for higher compatibility + code generation attributes on the recursor

made N2M more robust w.r.t. identical nested types

register bnfs for (co)datatypes under their proper name (lost in af71b753c459)

updated keywords;

restored old 'remotify' logic -- too many bugs were introduced when refactoring the code

more (co)datatype docs

hide 'rel' name -- this one is waiting to be merged with 'list_all2'

updated docs to reflect the new 'free_constructors' syntax

more precise spec rules for selectors

removed needless robustness (no longer needed thanks to new syntax)

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)

merged 'Option.map' and 'Option.map_option'

merged 'List.map' and 'List.list.map'

have 'Ctr_Sugar' register its 'Spec_Rules'

register 'Spec_Rules' for new-style (co)datatypes

added 'Spec_Rules' for 'primcorec'

more integrity checks of theory names vs. full node names -- at least for the scope of a single use_thys (or "theories" section in ROOT);

added a bit of documentation for the different commands

cleaner, complete proof in documentation, contributed by Dmitriy T.

do the right thing with provers that exist only remotely (e.g. e_sine)

more precise descripiton

all_args_conv works also for zero arguments

don't catch QOUT_THM_INTERNAL from the recursive call of parametrize_relation_conv

Lifting: support a type variable as a raw type

repaired logic for default provers -- ensures Z3 is kept if installed and configured as noncommercial

avoid changing the state's context -- this results in transfer problems later with SMT, and hence preplay tactic failures

removed hint that is seldom useful in practice

reactivate some examples that still appear to work;

removed dead code;

explicit indication that redefining outer syntax commands is not supposed to happen -- NB: interactive mode requires global change of syntax;

do not redefine outer syntax commands;

tuned whitespace;

static repair of ML file -- untested (!) by default since 76965c356d2a;

iteration n in the 'default' vs. 'update_new' vs. 'update' saga -- 'update' makes sense now that we honor the canonical order on 'merge' (as opposed to raising 'DUP')

don't hide constant forever, since it may appear in some 'primcorec'-generated theorems

tuning

HOL-IMP fastness

merged, resolving some conflicts;

eliminated hard tabs (assuming tab-width=2);

more platform notes;

tuned whitespace;

removed odd comments -- inferred types are shown by Prover IDE;

maintain blob edits within history, which is important for Snapshot.convert/revert;

more accurate eq_content;

clarified message_positions: cover alt_id as well; tuned;

maintain multiple command chunks and markup trees: for main chunk and loaded files; document view for all text areas, including auxiliary files;

common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content); more informative type Blob, to allow markup reports;

tuned signature;

report (but ignore) markup within auxiliary files;

merged

make integer_of_char and char_of_integer work with NBE and code_simp

make lifting setup for String.literal local to prevent transfer from replacing STR ''...'' literals

[mq]: news

remove hidden fact about hidden constant from code generator setup

for extraction -- use the exhaust rule that's registered with 'datatype_realizer.ML'

compile

updated certificates

tuned message

tabled, v.: postpone consideration of

adapted to renaming of 'Projl' and 'Projr'

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'

adapted theories to 'xxx_case' to 'case_xxx' * * * 'char_case' -> 'case_char' and same for 'rec' * * * compile * * * renamed 'xxx_case' to 'case_xxx'

renamed 'nat_{case,rec}' to '{case,rec}_nat'

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

adapted theories to '{case,rec}_{list,option}' names

avoid old 'prod.simps' -- better be more specific

repaired hard-coded constant names

killed 'rep_compat' option

made 'ctr_sugar' more friendly to the 'datatype_realizer' * * * reverted changes to 'datatype_realizer.ML'

use names like 'rec_mytype' and 'case_mytype' in old datatype package as well, to avoid a mixture

use right local theory -- shows up when 'no_discs_sels' is set

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'

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

tuned code

more 'ctr_sugar' modernization

tuning

ported predicate compiler to 'ctr_sugar' * * * ported predicate compiler to 'ctr_sugar', part 2

updated docs

generate 'fundec_cong' attribute for new-style (co)datatypes * * * compile

got rid of dynamic scoping the easy way

removed trivial 'rec' examples for nonrecursive types (I could also have added the 'old.' prefix in front of the constant names)

more liberal merging of BNFs and constructor sugar * * * make sure that the cache doesn't produce 'DUP's

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

have the same no-update semantics for 'case' as for 'Ctr_Sugar' and BNF data (this might not be the final word on the matter, but using a consistent policy seems like a good idea)

Mac OS X Lion (macbroy6) is baseline for portable executables; fringe platforms are unsupported;

"no_memory" option for the simplifier trace to bypass memoization

tuned

merged

seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;