the rule is not needed due to 1726f46d2aa8

merged

tuned tactic

tuned

less flex-flex pairs

less flex-flex pairs (thanks to Lars' statistics)

made tactics more robust

offical tool

more convenient syntax for permanent interpretation

aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"

move stronger rules into exercise

added a function that carries out all the reconstruction steps, for improved usability; added documentation;

reconstruction framework for LEO-II's TPTP proofs;

made list of test files a parameter to timed_test in TPTP_Test.thy, and updated dependent definitions;

cleaned code used to produce a proof-graph;

improved configurability of DOT exporter; tuned;

behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not; tuned;

experimented with presentation of DOT+LaTeX;

edges are now being shown in the proof graph; removed the shapes related to the conjecture and the negated conjecture, to remove clutter (since i'm also showing the inference's conclusion in latex);

added case for handling 'assumption' lines in Satallax proofs;

improved latex output: spacing between terms, and encoding terms in mathrm; tuned comments;

experimenting with improving DOT output, and embedding LaTeX code for formulas (rather than only giving the clause number);

added more node shapes (matched with roles);

updated NEWS

merged 'List.set' with BNF-generated 'set'

moved advanced folding into separate exercise

tuned definition

another simplification of internal codatatype construction

reflect 207538943038 in NEWS

reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes

removed not anymore used constants and theorems

simplifications of internal codatatype construction

adapted Nitpick to 'primrec' refactoring

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

rewrote a small portion of code to avoid dependency on low-level constant

tuning

provide more automation for type definitions (makes book exercises easier)

prepare two-stage 'primrec' setup

tuning

removed deadcode

merged

tuning

made SML/NJ happier

simplify proofs because of the stronger reflexivity prover

delete or move now not necessary reflexivity rules due to 1726f46d2aa8

implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules

merged

more markup;

proper term equality; proper Args.term_pattern parser (like 'is' or 'let' in Isar);

tuned message;

more uniform treatment of dockables and their standard actions;

standardized action and panel names;

tuned imports;

prefer concrete list append;

tuned whitespace;

more standard names for protocol and markup elements;

tuned whitespace;

tuned signature;

generic markup for embedded languages;

clarified special eol treatment (amending 3d55ef732cd7): allow last line to be empty, which means stop == end for second-last line;

more uniform/robust restriction of reported positions, e.g. relevant for "bad" markup due to unclosed comment in ML file;

subtle change of semantics of Thm.eq_thm, e.g. relevant for merge of src/HOL/Tools/Predicate_Compile/core_data.ML (cf. HOL-IMP);

always show PIDE positions as \<here> (0x002302 "House" from DejaVuSansMono);

hyperlink for visible positions;

more informative error;

more informative error;

removed not anymore used theorems

syntactic simplifications of internal (co)datatype constructions

follow up of 0819931d652d -- put right induction rule in the old data structure, repairs 'HOL-Proof'-based sessions

simplified data structure by reducing the incidence of clumsy indices

tuning * * * moved 'primrec' up to displace the few remaining uses of 'old_primrec'

made SML/NJ happy;

NEWS;

name derivations in 'primrec' for code extraction from proof terms

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

updated NEWS

updated keywords

renamed 'datatype_new_compat' to 'datatype_compat'

renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)

tuning: moved code where it belongs

have 'primrec_new' fall back on old 'primrec' when given old-style datatypes

tuning

more markup;

folded 'rel_option' into 'option_rel'

folded 'list_all2' with the relator generated by 'datatype_new'

removed final periods in messages for proof methods

tuned proofs;

added a version of the Metis tactic that returns the unused facts

tuned code

more NEWS

folded 'Option.set' into BNF-generated 'set_option'

merged

prefer user-space tool within Pure.thy;

more markup;

more uniform rendering of text that is formally interpreted: avoid clash with inner markup;

recovered Isabelle_Sidekick_Markup from 9c53198dbb1c: snapshot requires Swing_Thread;

support ML antiquotations in Scala; tuned -- more uniform ML vs. Scala;

antiquotations within plain text: Scala version in accordance to ML;

tuned signature -- emphasize line-oriented aspect;

eliminated odd dislocation of keyword declaration and implementation (leftover from 318cd8ac1817)

tuned whitespace;

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

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'