new examples of BNF lifting across quotients using a new theory of confluence,
which simplifies the relator subdistributivity proof obligation
(a few new useful notions were added to HOL;
notably the symmetric and equivalence closures of a relation)

More type class generalisations. Note that linorder_antisym_conv1 and linorder_antisym_conv2 no longer exist.

isabelle update -u path_cartouches;

isabelle update -u control_cartouches;

isabelle update -u control_cartouches;

replaced some ancient ASCII syntax

de-applying (mostly Set_Interval)

more simp

moved lemmas from AFP

more abbrevs;

more symbols;

ran isabelle update_op on all sources

misc tuning and modernization;

misc tuning and modernization;

tuned;

prefer abbreviations for compound operators INFIMUM and SUPREMUM

more uniform treatment of package internals;

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

isabelle update_cartouches -c -t;

option "inductive_defs" controls exposure of def and mono facts;

prod_case as canonical name for product type eliminator

discontinued specific HTML syntax;

standardized some occurences of ancient "split" alias

--HG--
extra : rebase_source : 706ba501d5c0596a2bde6e46d42aa8464a91ede5

isabelle update_cartouches;

add monotonicity rule for rtranclp

modernized header uniformly as section;

r_into_(r)trancl should not be [simp]: helps little and comlicates some AFP proofs

added [simp]

added lemmas

more antiquotations;

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)

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'

add acyclicI_order

simplifier uses proper Proof.context instead of historic type simpset;

renamed and added lemmas

prefer ML_file over old uses;

duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")

renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")

power on predicate relations

more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)

moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy

--HG--
extra : rebase_source : ed15629634477aff0a8efea30547f496c70907ad

moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy

renaming all lemmas with name rel_pow to relpow

adding code generation for relpow by copying the ideas for code generation of funpow

new code equation for ntrancl that allows computation of the transitive closure of sets on infinite types as well

cleanup of code declarations

--HG--
extra : rebase_source : 7376929a640011e27309be6654ccf370df37e60a

tuned layout

eliminated obsolete "standard";

tuned type annnotation

avoid very specific code equation for card; corrected spelling

--HG--
extra : rebase_source : 7a43ff22845a7caa93989e5f5ab5908190833404

bouned transitive closure

--HG--
extra : rebase_source : 3d0df473619b9c72b32a96ed4951a34dd2ad6c82

moved acyclic predicate up in hierarchy

--HG--
extra : rebase_source : 4c9a0c3c1dd3de32826493a20016e209648a4e47

modernized definitions

--HG--
extra : rebase_source : d50ecbd4a46b11ec1f49c3eb54ad2ee86a8981ce

adding lemma about rel_pow in Transitive_Closure for executable equation of the (refl) transitive closure

tuned proofs

new fastforce replacing fastsimp - less confusing name

simplified/unified Simplifier.mk_solver;

clarified map_simpset versus Simplifier.map_simpset_global;

added lemmas

renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics

renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI

expand_fun_eq -> ext_iff
expand_set_eq -> set_ext_iff
Naming in line now with multisets

qualified constants Set.member and Set.Collect

tuned quotes, antiquotations and whitespace

get rid of many duplicate simp rule warnings

lemma Image_closed_trancl

Tuned some proofs; nicer case names for some of the induction / cases rules.

removed "nitpick_def" attributes from (r)trancl(p), since "Nitpick.thy" overrides these

a few lemmas for point-free reasoning about transitive closure

simplified proof

inf/sup1/2_iff are mere duplicates of underlying definitions: dropped

be more cautious wrt. simp rules: sup1_iff, sup2_iff, inf1_iff, inf2_iff, SUP1_iff, SUP2_iff, INF1_iff, INF2_iff are no longer simp by default

"more standard" argument order of relation composition (op O)

replaced old METAHYPS by FOCUS;
eliminated homegrown SUBGOAL combinator -- beware of exception Subscript in body;
modernized functor names;
minimal tuning of sources;
reactivated dead quasi.ML (ever used?);

move rel_pow_commute: "R O R ^^ n = R ^^ n O R" to Transitive_Closure

rtrancl lemmas

added lemma

added lemma

new lemma

funpow and relpow with shared "^^" syntax

power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure

simplified method setup;

unified type Proof.method and pervasive METHOD combinators;

Merge.

name changes

Fixed nonexhaustive match problem in decomp, to make it fail more gracefully
in case assumptions are not of the form (Trueprop $ ...).

changed import hierarchy

- Function dec in Trancl_Tac must eta-contract relation before calling
decr, since it is now a function and could therefore be in eta-expanded form
- The trancl prover now does more eta-contraction itself, so eta-contraction
is no longer necessary in Tranclp_tac.

more antiquotations;
eliminated change_claset/simpset;

Added lemmas

rtranclp_induct, tranclp_induct: added case_names;
tuned proofs;

rtranclE, tranclE: tuned statement, added case_names;

Removed some case_names and consumes attributes that are now no longer
needed due to changes in the to_pred and to_set attributes.

tranclD2 (tranclD at the other end) + trancl_power

rtrancl and trancl are now defined using inductive_set.

stepping towards uniform lattice theory development in HOL

Adapted to new inductive definition package.

some new lemmas

induction rules for trancl/rtrancl expressed using subsets

simplified method setup;
reactivated dead code;

more robust syntax for definition/abbreviation/notation;

renamed 'const_syntax' to 'notation';

Changed precedence of "op O" (relation composition) from 60 to 75.

tuned concrete syntax -- abbreviation/const_syntax;

added lemma in_measure

added many simple lemmas

tuned proofs;

change_claset/simpset;

renamed rules to iprover

lemma, equation between rtrancl and trancl

migrated theory headers to new format

superceded by Pure.thy and CPure.thy;

unfold theorems for trancl and rtrancl

Deleted Library.option type.

import -> imports

New theory header syntax.

Documentation added; minor improvements.

New prover for transitive and reflexive-transitive closure of relations.
- Code in Provers/trancl.ML
- HOL: Simplifier set up to use it as solver

use more symbols in HTML output

Transitive_Closure: added consumes and case_names attributes
Isar: fixed parameter name handling in simulatneous induction
which I had not done properly 2 years ago.

Efficient, graph-based reasoner for linear and partial orders.
+ Setup as solver in the HOL simplifier.

* Support for raw latex output in control symbols: \<^raw...>
* Symbols may only start with one backslash: \<...>. \\<...> is no longer
accepted by the scanner.
- Adapted some Isar-theories to fit to this policy

undid split_comp_eq[simp] because it leads to nontermination together with split_def!

misc tidying

just a few mods to a few thms

Replaced some blasts by rules.

Transitive closure is now defined inductively as well.

clarified syntax of ``long'' statements: fixes/assumes/shows;

Made some proofs constructive.

converted theory Transitive_Closure;

renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl

setup [trans] rules for calculational Isar reasoning

Transitive closure is now defined via "inductive".

a new theorem from Bryan Ford

tuned;

unsymbolized;
tuned;

Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy

Transitive_Closure turned into new-style theory;

syntax (xsymbols);

superscripts: syntax (latex);

more "xsymbols" syntax;

*** empty log message ***