conclude simplification with default simpset

drop subsumed default equations (requires a little bit unfortunate laziness)

avoid Scala legacy operations

prefer fold over foldl

made List.thy a join point in the theory graph

tuned set_replicate lemmas

merged

added lemmas

dropped dead code

replaced unreliable metis proof

rev is reverse in Haskell

first serious draft of a scala code generator

more precise code

explicit type variable arguments for constructors

transitive superclasses were also only a misunderstanding

formal introduction of transitive superclasses

dropped obscure type argument weakening mapping -- was only a misunderstanding

added simp evaluator

merged

added code_simp infrastructure

tuned whitespace

maintain cong rules for case combinators; more precise permissiveness

drop function definitions of combinators

maintain cong rules for case combinators

formal introduction of case cong

found missing beta-eta-contraction

added missing Umlaut

make example run a bit faster (might help atbroy102)

merged

tuned documents

teaked naming of superclass projections

added lemma funpow_mult

extended bib

updated generated code

added reference

subsection on locale interpretation

explicitly name and note equations for class eq

use various predefined Haskell operations when generating code

NEWS

tuned internal order

dropped unused bindings

corrected syntax diagram

turn off new polymorphism code again -- a new issue popped up

missing case

A function called "untyped_aconv" shouldn't look at the bound names!

no point in introducing combinators for inlined Skolem functions

better error reporting for Vampire

expect SPASS 3.7, and give a friendly warning if an older version is used

improve ATP-specific error messages

merged

removed simplifier congruence rule of "prod_case"

adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"

merged

declare lexn.simps [code del]

declare lex_prod_def [code del]

modernized specifications

avoid references to old constdefs

merged

disable new polymorphic code for now, until remaining issues in "equality_inf" are resolved

"raise Fail" for internal errors + one new internal error (instead of "Match")

make test work again (broken since 09467cdfa198?)

adjust Nitpick example to follow latest wave of renamings

proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter

beta-eta-contract, to respect "first_order_match"'s specification; Sledgehammer's Skolem cache sometimes failed without the contraction

adjust Nitpick's handling of "<" on "rat"s and "reals"

remove needless variables

hide sum explicitly

merged

adjust popular symbolic type constructors

tailored set of code equations manually

tuned quotes, antiquotations and whitespace

moved inductive_codegen to place where product type is available; tuned structure name

qualified type "*"; qualified constants Pair, fst, snd, split

tuned quotes, antiquotations and whitespace

qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications

Adapted Mirabelle script (cf. f60e4dd6d76f)

merged

more consistent naming aroud type classes and instances

back to non-release mode;

removed obsolete test tags;

Added tag Isabelle2009-2 for changeset 35815ce9218a

final tuning;

corrected syntax diagram

Adapted Mirabelle script (cf. f60e4dd6d76f)

Added tag isa2009-2-test3 for changeset 0eacedd5f780

merged

NEWS: IsabelleText font;

Pretty.string_of (in Scala): actually observe margin/metric;

tuned Command.toString -- preserving uniqueness allows the Scala toplevel to print Linear_Set[Command] results without crashing;

tuned tooltips;

obsolete;

explicit treatment of empty exception block, which could lead to confusing output (e.g. in the theory loader), or even prevent error output altogether;

contrib/README;

removed outdated/confusing INSTALL file;

clarified font_family vs. font_family_default; install_fonts: refrain from any magic that does not really work on Mac OS, but introduces strange problems on other platforms;

disable set_styles for now -- there are still some race conditions of PropertiesChanged vs. TextArea painting (NB: without it Isabelle_Token_Marker will crash if sub/superscript is actually used);

Added tag isa2009-2-test2 for changeset dfca6c4cd1e8

more uniform treatment of options and attributes, preferring formal markup over old-style LaTeX macros;

merged;

Tuned.

Documented changes in induct, cases, and nominal_induct method.

merged

made SML/NJ happy again;

recovered some untested theories;

proper target directory;

refer to isabelle-release branch;

no symlinks; tuned;

merged

tuned ANNOUNCEMENT;

more NEWS;

more NEWS; tuned;

merged

cosmetics

renaming

show more respect for user-specified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound

fix remote Vampire diagnosis

make Sledgehammer's "add:" and "del:" syntax work better in the presence of aliases; some of these aliases pop up only after Sledgehammer has converted the formula to CNF, so it can be very confusing to the user who said "add: foo del: bar" that "bar" is used in the end.

totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax; faster and more reliable

single heaps archive;

merged

tuned;

removed obsolete dry-run option; just one archive for heaps, with the full cumulative collection (proper dependencies for rebuild);

Added tag isa2009-2-test1 for changeset d1cdbc7524b6

merged

avoid "$"

tuned whitespace

avoid flowerish abbreviation

merged

merge

don't raise Option.Option if assumptions contain schematic variables

recongize one more outcome string for "remote_vampire"

"print_vars_terms" wasn't doing its job properly; the offending line was "find_vars t1 #> find_vars t1", where the second "t1" should clearly have been "t2"

merged

made "clausify" attribute a legacy feature; seems to have ever only been a debugging feature

made "neg_clausify" a legacy feature

kill active Sledgehammer threads when running minimize, to avoid confusing the user with too much output

redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs

fix bugs in Sledgehammer's Isar proof "redirection" code

handle Vampire's definitions smoothly

fix bug in direct Isar proofs, which was exhibited by the "BigO" example

honor "xsymbols"

kill another neg_clausify proof

show types in Isar proofs, but not for free variables; this makes proofs more robust, without as much clutter as there used to be when types were enabled previously

give more helpful error message

first proposal for a announcement

NEWS (more strict internal axioms/defs format)

one all-inclusive bundle for each platform;

more robust handling of additional type variables: warning, more canonical order, drop mixfix syntax if implicit type arguments are introduced (to avoid delusion due to shifted arguments);

tuned warning;

less ambitious settings;

spelling;

do not open Proofterm, which is very ould style;

eliminated ML structure alias;

tuned default perspective;

tracing in aliceblue;

discontinued obsolete Isar.context() -- long superseded by @{context};

diagnostic commands 'ML_val' and 'ML_command' may refer to antiquotations @{Isar.state} and @{Isar.goal};

allow qualified names;

CONTRIBUTORS

clarified

mention unconstrain in NEWS

merged

hide default, map_entry, map_default

improved parallelism of proof term normalization;

always unconstrain thm proofs;

replaced ML pokes by explicit usedir -p; prefer -q 0 for proof terms, which avoids overhead of proof promises, while exploiting implicit parallelism of internal normalization;

merged

absolute import -- must work with Main.thy / HOL-Proofs

avoid duplicate import

HOL-Proofs is based in Main.thy

dropped lemma duplicate

msetprod_empty, msetprod_singleton

induction over non-empty lists

removed dependency of Euclid on Old_Number_Theory

modernized

removed obsolete usedir -p 1 option;

actually test smlnj;

updated keywords;

Added tag isa2009-2-test0 for changeset 935c75359742

more CONTRIBUTORS;

merged

Hilbert_Classical: disable multithreading altogether, otherwise proof normalization will fork futures independently of Goal.parallel_proofs;

merged

added lemmas

merged

merge

fix parameter settings

merged

merged

update NEWS

fix Nitpick soundness bug regarding The and Eps

added examples/tests for THE and SOME

cosmetics

adapt example

fix code that used to raise an exception if bound variables were given a finite function type, because the old vs. new bound variable types were confused

improved precision of "set" based on an example from Lukas

remove debug output

removed "nitpick_intro" attribute -- Nitpick noew uses Spec_Rules instead

subsumed by NEWS -- for older history, see previous versions of Nitpick

don't show spurious "..." in Nitpick's output for free variables of set type (e.g., P (op +) example from Manual_Nits.thy); undoes parts of 38ba15040455, which was too aggressive

honor xsymbols in Nitpick

added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"

document new option

make Nitpick handle multiple typedef entries for same typedef

remove comment

thread along context instead of theory for typedef lookup

obsolete FIXME

move SAT solver warning from every invocation of SAT solver to the tool, Refute, that uses it; "size_change" rarely needs anything beyond "dpll", so this warning is annoying at best, and when "size_change" is called from Nitpick the warning confuses users, who then think that Nitpick is using "dpll" when it's really using MiniSat or some other fast solver

don't include any axioms for "TYPE" in Nitpick

dropped obsolete script

normalize and postprocess proof body in a separate future, taking care of platforms without multithreading (greately improves parallelization in general without the overhead of promised proofs, cf. usedir -q 0);

merged

avoid store flag in add_* operations

arities: no need to maintain original codomain (cf. f795c1164708) -- completion happens in axclass.ML; misc tuning;

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