merged

tuned

Theory of homotopic paths (from HOL Light), plus comments and minor refinements

merged

tuned

explicit nested local theory for definitions, however retaining arcane low-level fiddling with background theory

tuned;

tuned whitespace;

trim lines for @{theory_text} similarly to @{text};

tuned;

tuned and converted to cmp

misc. changes to Imperative-HOL from Peter Gammie

Refine the supression of abbreviations for morphisms that are not identities.

Merge

New theorems mostly from Peter Gammie

make SML/NJ happy;

converted to cmp

moved lemmas

derive lemmas uniformly

Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths

converted lookup to cmp

removed lemmas that were only needed for old version of isin.

clarified contexts by factoring out reading and definition of mixins

merged

export internal definition

corrected inefficient implementation

more tracing in MaSh

tuned names

NEWS

formally correct context for export

merged

merged

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

tuned message;

added pretty syntax

tuned white space

leftover from 27ca6147e3b3

tuned whitespace

NEWS

droppen diagnostic junk from 4b53042d7a40

represent both algebraic and local-theory views on locale interpretation in interfaces

tuned -- share implementations as far as appropriate

prefer "rewrites" and "defines" to note rewrite morphisms

coalesce permanent_interpretation.ML with interpretation.ML

separate ML module for interpretation

reverted half-baken 7d1127ac2251

explicit computation of sort arguments for code equations makes less assumption about sort arguments of underlying type class instances

more standard ML, to make SML/NJ more happy;

tuned;

tuned whitespace;

tuned;

tuned whitespace;

merged

added antiquotation @{doc}, e.g. useful for demonstration purposes;

preserve names of for-fixes for faithfully;

more documentation;

tuned whitespace;

more uniform jEdit properties;

avoid vacuous quantification, as usual for shared variable scope;

support for structure statements in 'assume', 'presume';

support short form for \<^theory_text>;

MIR decision procedure again working

unnecessary precondition

Merge

Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.

tuned name

tuned

use cartouches instead of backquotes

translation for conjunctive premises

tuned

added proof state output warning

tuned

merged

no CRLF

new conversion theorems for int, nat to float

merged

uniform proof of lemmas

merged

adapt to 90f54d9e63f2

add various lemmas

add lemmas

generalise lemma

add lemmas for extended nats and reals

add various lemmas

cancel complementary terms as arguments to sup/inf in boolean algebras

add lemmas about monoids and groups

tuned

recovered from a9c0572109af;

merged

tuned whitespace;

added @{command}, @{method}, @{attribute};

smart quoting of non-identifiers, e.g. jEdit actions;

more thorough check_action, including completion;

tuned signature;

clarified modules;

more thorough check_command, including completion;

clarified modules;

unused;

ignore pointless/unused options;

added document antiquotation @{theory_text}; tuned document;

allow open symboloid;

generalized so that is also works for veriT proofs

fixing premises in veriT proof reconstruction

Merge

Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.

subdegree/shift/cutoff and Euclidean ring instance for formal power series

prefer static Font -- evade spontaneous change of TextField.font seen with Metal L&F in Plugin Options / Isabelle / General / Apply;

uniform mandatory qualifier for all locale expressions, including 'statespace' parent; removed obsolete '!' syntax;

qualifier is mandatory by default;

prefer explicit State panel;

suppress already persistent state output as well;

added option timeout_scale;

syntactic completion may supersede semantic completion, e.g. relevant for "\undefined" vs. "undefined" in ML;

clarified completion of explicit symbols (see also f6bd97a587b7, e0e4ac981cf1);

tuned;

less confusing markup;

added @{undefined} with somewhat undefined symbol;

ML cartouches via control antiquotation;

more formal treatment of control symbols;

more antiquotations;