merged

do not expose store flag of AxClass.add_*

merged

adapted to changes

capitalized type variables; added yield as keyword

brackify_infix etc.: no break before infix operator -- eases survival in Scala

basic support for sub/superscript token markup -- NB: need to maintain extended token types eagerly, since jEdit occasionally reinstalls a style array that is too short;

use local /home/isatest/polyml-5.3.0 on atbroy102 to avoid problems with the SMB filesystem via homebroy;

uniform ML environment setup for Isar and PG;

merged

Renamed TypeInfer to Type_Infer.

merged

assign now applies meet before update_new to avoid misleading error message.

Tuned.

Adapted to new format of proof terms containing explicit proofs of class membership.

classrel and arity theorems are now stored under proper name in theory. add_arity and add_classrel take extra boolean argument indicating whether theorems should be stored.

- outer_constraints with original variable names, to ensure that argsP is consistent with args - Exported map_proof_same, added implies_intr_proof' and forall_intr_proof' - Rewriting procedures used by rewrite_proof can now access hypotheses - Finally enabled unconstrain

outer_constraints with original variable names, to ensure that argsP is consistent with args

- Equality check on propositions after lookup of theorem now takes type variable renamings into account - Unconstrain theorem after lookup - Improved error messages for application cases

Use Proofterm.forall_intr_proof' instead of locally defined forall_intr_prf.

- Added extra flag to read_term and read_proof functions that allows to parse (proof)terms in which all type variables have the top sort - Adapted proof_of_term to handle proofs with explicit class membership proofs

merged

merged

corrected printing of characters

corrected implementation

added Scala code setup

tuned code setup

keep structure ThyLoad for the sake of Proof General;

added random instance for word

notes on Isabelle/jEdit;

remove presently unused Isabelle application;

modernized some structure names, keeping a few legacy aliases;

merged

merge

fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option

updated generated files

clarified

adjusted

terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);

Toplevel.run_command: reraise Interrupt, to terminate the Isar_Document.execution and not store a failed attempt;

merged

Typo in locales tutorial.

Theory_Target.pretty: more markup;

tuned abbrevs for long arrows, according to usual ASCII syntax;

more flexibile font size via CSS <style> instead of old <font> element; preformatted text;

tuned;

control tooltip font via Swing HTML, with tooltip-font-size property;

added HTML.encode (in Scala), similar to HTML.output in ML;

one extra space to accomodate symbolic indentifiers etc.;

replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information; ML_Context.eval/expression expect explicit ML_Lex source, which allows surrounding further text without loosing position information; fall back on ML_Context.eval_text if there is no position or no surrounding text; proper Args.name_source_position for method "tactic" and "raw_tactic"; tuned;

more detailed token markup, including command kind as sub_kind; type-safe access to Command.HighlightInfo;

tuned;

separate markup for ML delimiters;

less pschedelic token markup;

simplified command/keyword markup;

markup non-identifier keyword as operator;

Isabelle_Process: do not enforce future_terminal_proof by default -- no error propagation yet;

more basic default behaviour of ENTER, HOME, END;

tuned messages;

do not highlight ignored command spans; tuned;

more explicit handling of document;

explicit markup for forked goals, as indicated by Goal.fork; accumulate pending forks within command state and hilight accordingly; Isabelle_Process: enforce future_terminal_proof, which gives some impression of non-linear/parallel checking;

avoid :\ which is not tail-recursive and tends to overflow the tiny JVM stack, which is not resizable at runtime;

define_state/new_state: provide state immediately, which is now lazy; more careful document editing: single execution future forces all entries, synchronous cancelation after update;

force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling; recovered some similarity to sequential version;

future result: retain plain Interrupt for vacuous group exceptions;

remove two examples, now that the definition of "fst" and "snd" has changed

merged

Got rid of a warning about duplicate rewrite rules.

accumulate only local results -- no proper history support yet;

avoid deprecated Iterator.fromArray;

more compiler warnings;

eliminated hard tabs;

assume given SCALA_HOME, e.g. from component settings or external setup;

merged

merged

make sure chained facts appear in Isar proofs generated by Sledgehammer -- otherwise the proof won't work

Nitpick: show "..." in datatype values (e.g., [{0::nat, ...}]), since these are really equivalence classes

make Nitpick "show_all" option behave less surprisingly

merged

avoid reference to thm PairE

more coherent theory structure; tuned headings

made SML/NJ quite happy;

reuse main view.font from jEdit;

deleted some old fonts;

also set font for printing, which actually works out of the box;

lib/Tools/makeall does not hardiwre logics;

discontinued Sun/Solaris tests;

some updates for release;

merged

added function update examples and set examples

updated SMT certificates

sort signature in SMT-LIB output (improves sharing of SMT certificates: goals of the same logical structure are translated into equal SMT-LIB benchmarks)

merged

renamed constant "apply" to "fun_app" (which is closer to the related "fun_upd")

made script executable

use Z3's builtin support for div and mod

moved SMT into the HOL image

slightly odd workaround to ignore markup that is typically displaced;

substantial performance improvement by avoiding "re-ified" execution structure via future dependencies, instead use singleton execution (dummy future) that forces lazy state updates bottom-up; tuned;

further formal thread-safety (follow-up to 88300168baf8) -- in practice there is only a single Isar toplevel loop, but this is not enforced;

renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;

renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;

misc updates for release;

constant Rat.normalize needs to be qualified;

merged

merged

dropped legacy theorem bindings

dropped legacy theorem bindings

dropped legacy theorem bindings

dropped legacy theorem bindings

dropped legacy theorem bindings

normalized references to constant "split"

Revise locale test theory layout.

Merge mixins of distinct interpretations with same base.

indicate prospective properties;

clarified auto_update vs. update; tuned;

more reactive message handling, notably for follow_caret mode; misc tuning and clarification;

Command.toString: include id for debugging; Command.consume: explicit forward, avoid dependency on Session and side-effect on event bus; State.+ without side-effect on event bus; Session.commands_changed: delayed command changes (outside of Swing thread), also subsumes former Session.results; Document_View: tuned commands_changed handling and caret listening; Document_View.selected_command: proper function, not event handler state; Output_Dockable: directly act upon commands_changed, not caret events (via former Session.results);

merged

refer to polyml-5.3.0-old for ppc-darwin;

try logical and theory abstraction before full abstraction (avoids warnings of linarith)

updated SMT certificates

hide constants and types introduced by SMT, simplified SMT patterns syntax, added examples for SMT patterns

more convenient order of code equations

misc updates for release;

eliminated obsolete priority message from Isabelle_Process protocol;

moved ML files where they are actually used; more precise dependencies;

renamed HOLCF/Library/ROOT.ML to HOLCF/Library/HOLCF_Library_ROOT.ML to avoid accidental uses of this ML file via the load path -- see also d7711be8c3a9 (obsolete) and ccae4ecd67f4;

eliminated slightly odd Library/Library session setup (cf. d7711be8c3a9) which is obsolete due to usedir -f HOL_Library_ROOT.ML;

eliminated various catch-all exception patterns, guessing at the concrete exeptions that are intended here;

tuned -- avoid catch-all exception pattern;

updated generated files;

merged

merged

Typo fixed.

move HOLCF/Sum_Cpo.thy to HOLCF/Library

move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path

move unused pattern match syntax stuff into HOLCF/ex

rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed

more lemmas

induction and case rules

Store registrations in efficient data structure.

Avoid recomputation of registration instance for lookup.

Consistently use equality for registration lookup.

Cleaner implementation of sublocale command.

Reapply mixin patch: base for performance improvements.

merged

declare a few more cont2cont rules

HOLCF no longer redefines 'consts' command

for functions with only variable patterns, fixrec definitions no longer use Fixrec.return/Fixrec.run

simplify fixrec continuity tactic

used sledgehammer[isar_proof] to replace slow metis call

Typo fixed.

Typo fixed.

Minor proof tuning.

Improved document structure.

Minor proof tuning.

merged

Refactoring, minor extensions (e.g., church_rosser).

NEWS: removed fixrec_simp attribute

merged

disambiguate some syntax

optimize continuity proofs in fixrec package, using cont2cont rules

add beta_cfun simproc, which uses cont2cont rules

removed fixrec_simp attribute (cf. a2a1c8a658ef)

simplify definition of eta_tac

remove fixrec_simp attribute; fixrec uses default simpset from theory context instead

remove cont2cont simproc; instead declare cont2cont rules as simp rules

domain package internal proofs use fixed set of continuity rules, rather than taking cont2cont rules from context

merged

modernized sorting algorithms; quicksort implements sort

modernized sorting algorithms; quicksort implements sort

localized properties_for_sort

@tailrec annotation;

renamed "rev" to "reverse" following usual Scala conventions;

parse_spans: cover full range including adjacent well-formed commands -- intermediate ignored and malformed commands are reparsed as well;

added rev_iterator;

tuned;

access statically typed dockable windows;

simplified dockables using class Dockable;

generic dockable window;

separate event bus and dockable for raw output (stdout);

more Mac OS problems;

ignore system messages;

use proper ISABELLE_PLATFORM instead of adhoc uname;

refrain from using bold within the term language -- looks odd in Lobo with error/warning background;

tuned;

removed timing;

rendering information and style sheets via settings; generalized Isabelle_System.try_read; prefer getenv_strict in most situations;

more brackets -- unaligned to prevent odd auto-indentation;

merged

adjusted to changes in Mapping.thy

merged

tuned

more lemmas about mappings, in particular keys

refined

nats in Haskell are readable

Let rsp and prs in fun_rel/fun_map format

tuned zoom_box; tuned tooltips;

print calculation result in the context where the fact is actually defined -- proper externing; misc tuning;

future_job: propagate current Position.thread_data to the forked job -- this is important to provide a default position, e.g. for parallelizied Goal.prove within a package (proper command transactions are wrapped via Toplevel.setmp_thread_position);

some message styling;

simplified message markup, using plain XML.Elem directly;

more robust Position.setmp_thread_data, independently of Output.debugging (essentially reverts f9ec18f7c0f6, which was motivated by clean exception_trace, but without transaction positions the Isabelle_Process protocol breaks down);

refrain from forcing a hardwired SHELL value, cf. 1494ded298a6 but it becomes obsolete again in 549969a7f582 and follow-ups;

bad_result: report fully explicit message;

observe additional isabelle-jedit.css for component and user; visial separation of message divs;

added checkboxes for debug/tracing filter; misc tuning;

more abstract view on prover output messages;

added some tooltips;

HTML_Panel.handler as overridable method;

added Library.undefined (in Scala);

more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread; do not re-use mutable DOM -- avoid races wrt. the rendering engine; more thorough resize -- always recalculate metrics/margin synchronously; asynchronous setDocument; tuned;

component resize: full handle_resize;

speed up some proofs and fix some warnings

merged

merged

proper code generator for complement

proper document text

implement Mapping.map_entry

operations default, map_entry, map_default; more lemmas

added More_List.thy explicitly

renamed List_Set to the now more appropriate More_Set

added theory More_List

moved generic List operations to theory More_List

adjusted

turned old-style mem into an input abbreviation

zoom font size;

added somewhat generic zoom box;

try CheckBox instead of ToggleButton, which is visually confusing without window focus, e.g. in a floating instance (problem of MacOS look-and-feel);

mutate displayed document synchronously in Swing thread, for improved robustness;

read style sheets only once;

handle component resize for output / HTML panel;

Isabelle_System: allow explicit isabelle_home argument;

enable shell script editor mode;

merged

merged

deactivated timing of infering modes

adapting examples

changing operations for accessing data to work with contexts

removed unnecessary Thm.transfer in the predicate compiler

changing compilation to work only with contexts; adapting quickcheck

removing unused argument in print_modes function

moving towards working with proof contexts in the predicate compiler

improved values command to handle a special case with tuples and polymorphic predicates more correctly

improved behaviour of defined_functions in the predicate compiler

move some example files into new HOLCF/Tutorial directory

remove redundant hdvd relation

remove unnecessary constant Fixrec.bind

add section about fixrec definitions with looping simp rules

more informative error message for fixrec when continuity proof fails

determine margin just before rendering -- proper reformatting when updating;

simplified alignment via FlowPanel; tuned;

more systematic treatment of physical document wrt. font size etc.; eliminated (crude) double buffering; tuned;

tuned;

general Isabelle_System.try_read;

explicit Command.Status.UNDEFINED -- avoid fragile/cumbersome treatment of Option[State];

inverted "Freeze" to "Follow", which is the default; update unconditionally;

basic controls to freeze/update prover results;

show fully detailed protocol messages;

some updates following src/Tools/jEdit/dist-template/settings;

spelt out normalizer explicitly -- avoid dynamic reference to code generator configuration; avoid using old Codegen.eval_term

merged

dropped legacy_unconstrainT

new version of triv_of_class machinery without legacy_unconstrain

merge

added implementations of Fset.Set, Fset.Coset; do not delete code equations for relational operators on fsets

remove several redundant lemmas about floor and ceiling

merged

declare add_nonneg_nonneg [simp]; remove now-redundant lemmas realpow_two_le_order(2)

simplify proof

simplify proof

remove some unnamed simp rules from Transcendental.thy; move the needed ones to MacLaurin.thy where they are used

prefer structure Keyword and Parse;

merged

merged

remove simp attribute from square_eq_1_iff

merged

make sure chained facts don't pop up in the metis proof

fix bug in Isar proof reconstruction step relabeling + don't try to infer the sorts of TVars, since this often fails miserably

generate proper arity declarations for TFrees for SPASS's DFG format; and renamed a confusing function in the process

identify common SPASS error more clearly

remove simp attribute from power2_eq_1_iff

dropped old Library/Word.thy and toy example ex/Adder.thy

dropped old Library/Word.thy and toy example ex/Adder.thy

do not open Legacy by default;

prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;

renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time; eliminated slightly odd alias structure T;

tuned;

tuned signature;

renamed class Outer_Lex to Token and Token_Kind to Token.Kind;

centralized legacy aliases;

prefer structure Parse_Spec;

renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;

renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;

renamed structure ValueParse to Parse_Value; eliminated old-style structure alias V;

refer directly to structure Keyword and Parse; eliminated old-style structure aliases K and P;

renamed structure OuterKeyword to Keyword and OuterParse to Parse, keeping the old names as legacy aliases for some time;

renamed Outer_Parse to Parse (in Scala);

renamed Outer_Keyword to Keyword (in Scala);

avoid open Conv;

less pervasive names from structure Thm;

less pervasive names from structure Thm;

tuned;

merged

add real_le_linear to list of legacy theorem names

make SML/NJ happy

removed unused conversions;

tuned header; tuned white space;

moved normarith.ML where it is actually used; less inaccurate dependencies;

incorporated further conversions and conversionals, after some minor tuning;

eliminated redundant runtime checks;

normalize atyp names after unconstrainT, which may rename atyps arbitrarily;

more precise dependencies for HOL-Word-SMT_Examples;

merged

merge

added Sledgehammer documentation to TOC

added some Sledgehammer news

document Nitpick changes

merge

added Sledgehammer manual; some material was recovered from the Isar material, the rest is new

renamed Sledgehammer options

renamed options

remove support for crashing beta solver HaifaSat

renamed two Sledgehammer options

merged

added listsum lemmas

Revert mixin patch due to inacceptable performance drop.

add "no_atp"s to Nitpick lemmas

query _HOME environment variables at run-time, not at build-time

move Refute dependency from Plain to Main

move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong

recognize new Kodkod error message syntax

improve precision of set constructs in Nitpick

produce more potential counterexamples for subset operator (cf. quantifiers)

improved Sledgehammer proofs

pass "full_type" argument to proof reconstruction

made Sledgehammer's full-typed proof reconstruction work for the first time; previously, Isar proofs and full-type mode were mutually exclusive because both options were hard-coded in the ATP names (e.g., "e_isar" and "full_vampire") -- making the options orthogonal revealed that some code was missing to handle types in the proof reconstruction code

delect installed ATPs dynamically, _not_ at image built time

Fix syntax; apparently constant apply was introduced in an earlier changeset.

Merged.

Add mixin to base morphism, required by class package; cf ab324ffd6f3d.

Remove improper use of mixin in class package.

Multiset: renamed, added and tuned lemmas; Permutation: replaced local "remove" by List.remove1

use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document

more precise dependencies

updated SMT certificates

layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable

integrated SMT into the HOL image

replaced More_conv.top_conv (which does not re-apply the given conversion to its results, only to the result's subterms) by Simplifier.full_rewrite

use proper context operations (for fresh names of type and term variables, and for hypothetical definitions), monomorphize theorems (instead of terms, necessary for hypothetical definitions made during lambda lifting)

split monolithic Z3 proof reconstruction structure into separate structures, use one set of schematic theorems for all uncertain proof rules (to extend proof reconstruction by missing cases), added several schematic theorems, improved abstraction of goals (abstract all uninterpreted sub-terms, only leave builtin symbols)

added tracing of reconstruction data

added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms

deleted SMT translation files (to be replaced by a simplified version)

move the addition of extra facts into a separate module

normalize numerals: also rewrite Numeral0 into 0

added missing rewrite rules for natural min and max

rewrite bool case expressions as if expression

simplified normalize_rule and moved it further down in the code

merged addition of rules into one function

added simplification for distinctness of small lists

moved the addition of DLO tactic into the Z3 theory (DLO is required only for Z3 proof reconstruction)

added Proofterm.unconstrain_thm_proof for Thm.unconstrainT -- loosely based on the version by krauss/schropp;

conditionally unconstrain thm proofs -- loosely based on the version by krauss/schropp;

the_classrel/the_arity: avoid Thm.transfer for proofterm version -- theory might already have become stale within the proof_body future;

avoid redundant rebinding of name/prop -- probably introduced accidentally in 80bb72a0f577;

raise Fail uniformly for proofterm errors, which appear to be rather low-level;

unconstrainT operations on proofs, according to krauss/schropp;

added Proofterm.get_name variants according to krauss/schropp; tuned signature;

conditional structure SingleAssignment;

merged

merged

tuned proofs and fact and class names

tuned fact collection names and some proofs

grouped local statements

tuned test problems

merged

merged

simplified proof

modernized specifications;

updated/unified some legacy warnings;

tuned;

do not emit legacy_feature warnings here -- users have no chance to disable them;

removed obsolete CVS Ids;

removed some obsolete admin stuff;

check NEWS;

removed obsolete CVS Ids;

updated some version numbers;

minor tuning;

reverted parts of 7902dc7ea11d -- note that NEWS of published Isabelle releases are essentially read-only; (Spelling note: "supersede" is indeed more common in Isabelle sources, although "supercede" is also correct according to major dictionaries.)

merged

merged

modernized specifications; tuned reification

merged

added lemmas concerning last, butlast, insort

Remove RANGE_WARN

clarified NEWS entry

merged

added NEWS entry

Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'

Add rules directly to the corresponding class locales instead.

Removed usage of normalizating locales.

speed up some proofs, fixing linarith_split_limit warnings

fix some linarith_split_limit warnings

include iszero_simps in semiring_norm just once (they are already included in rel_simps)

fix duplicate simp rule warning

no more RealPow.thy (remaining lemmas moved to RealDef.thy)

merged

simplify code for emptiness check

removed lemma real_sq_order; use power2_le_imp_le instead

merged

merged

represent de-Bruin indices simply by position in list

tuned reification functions

tuned code; toward a tightended interface with generated code

fix spelling of 'superseded'

NEWS: removed theory PReal

collected NEWS updates for HOLCF

merged

move floor lemmas from RealPow.thy to RComplete.thy

add lemma tendsto_Complex

move some theorems from RealPow.thy to Transcendental.thy

add lemma power2_eq_1_iff; generalize some other lemmas

minimize imports

move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff

clarified Pretty.font_metrics;

format as topmost list of "divs", not just adjacent "spans" -- for proper line breaking;

tuned;

more precise pretty printing based on actual font metrics; removed obsolete relative margin;

predefined spaces;

merged

support Isabelle plugin properties with defaults; font size relative to view.textsize of jEdit; margin relative to component width and approximative font metrics;

merged

tuned proof so that no simplifier warning is printed

renamed former Int.int_induct to Int.int_of_nat_induct, former Presburger.int_induct to Int.int_induct: is more conservative and more natural than the intermediate solution

merged

tuned

theorem Presburger.int_induct has been renamed to Int.int_bidirectional_induct

tuned; dropped strange myassoc2

stylized COOPER exception

simplified oracle

shorten names

updated references to ML files

only one module fpr presburger method

moved int induction lemma to theory Int as int_bidirectional_induct

tuned theory text; dropped unused lemma

one structure is better than three

less complex organization of cooper source code

dropped unused bindings; avoid open (documents dependency on generated code more explicitly)

add real_mult_commute to legacy theorem names

new construction of real numbers using Cauchy sequences

add more credits to ex/Dedekind_Real.thy

put construction of reals using Dedekind cuts in HOL/ex

disable two stage save by default, to avoid change of file permissions (notably the dreaded executable bit on Cygwin);

simple dialogs: ensure Swing thread;

font size re-adjustment according to Lobo internals;

Scala for Netbeans 6.8v1.1.0rc2;

more convenient get_font;

renamed Config.get_thy to Config.get_global etc. to indicate that this is not the real thing;

more convenient look-and-feel setup;

more convenient get_font;

explicit getLines(n) ensures platform-independence -- our files follow the POSIX standard, not DOS;

updated to jedit 4.3.2;

ignore spurious TIMEOUT messages, maybe caused by change of actor semantics in scala-2.8;

adapted to scala-2.8.0.RC2;

merged

real_mult_commute -> mult_commute

avoid using real-specific versions of generic lemmas

avoid using real-specific versions of generic lemmas

remove a couple of redundant lemmas; simplify some proofs

merged

add lemmas one_less_inverse and one_le_inverse

do not redeclare [simp] rules, to avoid "duplicate rewrite rule" warnings

added lemmas rel_comp_UNION_distrib(2)

made SML/NJ happy;

reactivated Thm.legacy_unconstrainT for Nbe.lift_triv_classes_conv;

Thm.unconstrainT based on Logic.unconstrainT -- no proofterm yet;

just one version of Thm.unconstrainT, which affects all variables; temporary workaround for Nbe.lift_triv_classes_conv;