tuned document; tuned proofs;

more precise dependencies;

inlined antiquotations;

misc tuning and modernization;

optional timing, to avoid redundant allocation of mutable cells;

tuned;

misc tuning;

merged

more use of global operations (see 98ec8b51af9c)

more uniform instT_subst vs. inst_subst: compare variable names only;

tuned cterm_instantiate: avoid somewhat expensive Term.map_types and cterm_of;

misc tuning and modernization;

some performance tuning via Term_Subst/Same.operation; tuned;

pruned signature;

added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types; tuned;

more conventional syntax const;

proper syntactic category for abstraction syntax, to avoid low-level exception for malformed "\<integral> x y. f \<partial>M", for example;

merged

prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);

document new experimental provers

added remote iProver(-Eq) for experimentation

merged

ex/Tree23.thy: automate proof of gfull_add

ex/Tree23.thy: simplify proof of bal_del0

ex/Tree23.thy: simplify proof of bal_add0

ex/Tree23.thy: simpler definition of ordered-ness predicate

ex/Tree23.thy: prove that deletion preserves balance

more liberal Parse.fixes, to avoid overlap of mixfix with is-pattern (notably in 'obtain' syntax);

more general Proof_Context.bind_propp, which allows outer parameters; obtain: some support for term bindings within the proof, depending on parameters;

tuned whitespace;

tuned signature;

tuned signature -- canonical argument order;

tuned -- Variable.declare_term is already part of Variable.auto_fixes;

ex/Tree23.thy: prove that insertion preserves tree balance and order

more IMP fragments

string -> vname

JMPF(LESS|GE) -> JMP(LESS|GE) because jumps are int now.

more IMP text fragments

moved latex generation for HOL-IMP out of distribution

renaming Quotient_Set and List_Quotient_Set to Quotient_Cset and List_Quotient_Cset to avoid name clash with existing Quotient_Set (again, cf. 66823a0066db)

merged

more robust, declarative and unsurprising computation of types in the quotient type definition

improve handling of bound type variables (esp. for TFF1)

improved TFF1 output

clarified signature

tuned

tuned

even more uniform Local_Theory.declaration for locales (cf. 57def0b39696, aa35859c8741);

removed obsolete argument (cf. aa35859c8741);

removed ad-hoc simp rules sin_cos_eq[symmetric], minus_sin_cos_eq[symmetric], cos_sin_eq[symmetric]

extend cancellation simproc patterns to cover terms like '- (2 * pi) < pi'

merged

remove unused function

also export DFG formats

always use DFG format to talk to SPASS -- since that's what we'll need to use anyway to benefit from sorts and other extensions

added DFG unsorted support (like in the old days)

gracefully do nothing if the SPASS input file is already in DFG format

added sorted DFG output for coming version of SPASS

specify proof output level 1 (i.e. no detailed, potentially huge E proofs) to LEO-II; requires version 1.2.9

check "sound" flag before doing something unsound...

uniform treatment of syntax declaration wrt. aux. context (NB: notation avoids duplicate mixfix internally);

tuned;

more accurate class constraints on cancellation simproc patterns

tuned;

tuned Named_Thms: proper binding;

refined Local_Theory.declaration {syntax = false, pervasive} semantics: update is applied to auxiliary context as well;

more robust data storage (NB: the morphism can change the shape of qconst, and in the auxiliary context it is not even a constant yet);

uniform Local_Theory.declaration with explicit params;

tuned signature -- refined terminology;

slightly more explicit/syntactic modelling of morphisms;

correct import path

allow to build Probability and MV-Analysis with one ROOT.ML

removing dead code

ex/Simproc_Tests.thy: remove duplicate simprocs

use simproc_setup for cancellation simprocs, to get proper name bindings

tuned;

eliminated aliases of standard functions;

more standard attribute setup;

localized quotient data;

simplified/standardized signatures;

tuned signature;

uses IMP and hence requires its tex setup

merged

tuned text

respecting isabelle's programming style in the quotient package by simplifying qconsts_lookup function for data access; removing odd NotFound exception

respecting isabelle's programming style in the quotient package by simplifying map_lookup function for data access

respecting isabelle's programming style in the quotient package by simplifying quotdata_lookup function for data access

merged

fix bug in cancel_factor simprocs so they will work on goals like 'x * y < x * z' where the common term is already on the left

more robust ML pretty printing (cf. b6c527c64789);

tuned;

renaming Cset and List_Cset in Quotient_Examples to Quotient_Set and List_Quotient_Set to avoid a name clash of theory names with the ones in HOL-Library

tuned text

tuned names to avoid shadowing

merge Gcd/GCD and Lcm/LCM

clarify types of terms: use proper set type

instance bool :: linorder

removing poor man's dictionary construction which were only for the ancient code generator with no support of type classes

fixed typo

latex output not needed because errors manifest themselves earlier

some text on inner-syntax;

renamed in ASM

tuned order of eqns

tuned

script for exporting filtered IMP files as tar.gz

removed Norbert's email from isatest (bounces)

class Lexicon as abstract datatype;

more private stuff;

class Text.Edit as abstract datatype;

class Time as abstract datatype;

class Volatile as abstract datatype;

merged