generate "id" rather than (%v. v)

correctly generate sel_coiter and sel_corec theorems

generate "sel_coiters" and friends

sanity check

implemented and use "mk_sum_casesN_balanced"

fixed general case of "mk_sumEN_balanced"

debug

fixed base case of "mk_sumEN_balanced"

prevent inconsistent selector types

minor optimization

allow same selector name for several constructors

removed done TODO

avoid type inference + tuning

use balanced sums for constructors (to gracefully handle 100 constructors or more)

busted -- let's use more neutral names

replacing own dummy value by Haskell's Prelude.undefined

prefer global default font over IsabelleText of jEdit TextArea;

uniform operation on initial delay;

option jedit_load_delay; tuned;

dynamic evaluation of time (e.g. via options); proper setInitialDelay, not setDelay;

proper multi-line tooltip;

more detailed option tooltip; more formal option.load; properties change propagation to Session_Dockable;

more systematic JEdit_Options.make_component; separate module Isabelle_Logic;

manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences);

formal markup for @{file} (for hyperlinks etc.) -- interpret path wrt. master directory as usual;

more explicit indication of legacy features;

more explicit indication of legacy features;

simplify "Process" example even further

stabilized generation of parameterized theorem

added snippets

simplify "Process" example further

simplify "Process" example

full name of a type as key in bnf table

fixed bug with one-value codatatype "codata 'a dead_foo = A"

tuning

fixed and reenabled "corecs" theorems

fixed and enabled generation of "coiters" theorems, including the recursive case

generate "fld_unf_corecs" as well

reactivated generation of "coiters" theorems

use map_id, not map_id', to allow better composition

open typedefs everywhere in the package

open typedef for datatypes

fixed and enabled iterator/recursor theorems

renamed for consistency

oops

tuning

for compatiblity with old datatype package: not only "recs" with "s", but also "iters" and their "fld_"/"unf_" variants

fixed bug with one-value types with phantom type arguments

imported patch debugging

repaired "nofail4" example

renamed xxxBNF to pre_xxx

fixed handling of map of "fun"

comment out code that's not ready

tuning

construct the right iterator theorem in the recursive case

some work on coiter tactic

more sugar on codatatypes

define corecursors

define coiterators

TODO

tuning

completed iter/rec proofs

TODOs

implemented "mk_iter_or_rec_tac"

generate iter/rec goals

repaired constant types

some work towards iterator and recursor properties

tuning

correctly curry recursor arguments

added high-level recursor, not yet curried

merged

tuned proofs;

postpone update of text overview panel after incoming session edits, to improve reactivity of editing massive theories like src/HOL/Multivariate_Analysis;

more explicit Delay operations;

tuned proofs;

clearer names for functions in Quickcheck's narrowing engine

merged

tuned latex

lattice instances for option type

combinator Option.these

adjusted examples

countable_datatype method: pre-instantiate induction rule to avoid failure with e.g. datatype a = A "b list" and b = B "a"

handle type constructors not known to be a BNF using the DEADID BNF

respect order of/additional type variables supplied by the user in fixed point constructions;

gracefully handle shadowing case (fourth step of sugar localization)

careful about constructor types w.r.t. fake context (third step of localization)

read the real types off the constant types, rather than using the fake parser types (second step of sugar localization)

tuning

use "add_type" rather than "add_types_global"

don't throw away the context when hacking the theory (first step to localize the sugar code)

tuning

introduced and used "mk_Freesss", and simplified "mk_Freess(')"

construct high-level iterator RHS

option for discarding build results, enabled in particular for Isabelle_makeall

by default, only generate one discriminator for a two-value datatype

eliminated potentially confusing terminology of Scala "layer";

merged

tuned proofs;

discontinued obsolete fork_mono to loosen some brakes -- NB: TTY interaction has Goal.future_proofs disabled due to missing Future.worker_task;

honor mixfix specifications

code indentation

print timing information

adapted example

check type variables on rhs

proper subsexp projection of Isabelle_Markup.Path, in correspondence to 5d0cd770828e;

added tooltip to reveal jEdit platform file name;

commented out slow examples again

fixed (n + 1)st bug in "mk_exhaust_tac" -- arose with uncurried constructors

fixed "mk_exhaust_tac" for the nth time

updated README

ported "Misc_Codata" to new syntax

ported "Misc_Data" to new syntax

error message only in case of an error

do not trivialize important internal theorem in quick_and_dirty mode

merged

made "mk_case_eq_tac" work in the case where the first constructor is an "alternate" constructor (in which case its discriminator paradoxically starts with a negation)

tuning (systematic 1-based indices)

reindented code

added TODO

tell "select_prem_tac" not to thin any further premisses -- the "rotate_tac" otherwise confuses it

fixed "mk_alternate_disc_def_tac" in the case where the constructors are swapped compared with the common Nil/Cons case

don't get confused by extraneous premisses

added a check

NEWS; CONTRIBUTORS

misc tuning;

no need to wait 3h on macbroy30 (unlike former macbroy6, cf. 6e5b994070c1);

more conservative rechecking of processed constraints in subtyping constraint simplification

added comment for Dmitriy

fixed bug in type instantiation of case theorem

use empty binding rather than "*" for default

tuned

fixed bugs in one-constructor case

smoothly handle one-constructor types

fixed some type issues in sugar "exhaust_tac"

optionally provide extra dead variables to the FP constructions

merged

added robustness

added build option -R; more precise build_doc, using build -R -b;

implemented "mk_case_tac" -- and got rid of "cheat_tac"

define "case" constant

renamed low-level (co)iterators and (co)recursors with "fld_"/"unf_" prefix

implemented "mk_half_distinct_tac"

implemented "mk_inject_tac"

implemented "mk_exhaust_tac"

more work on FP sugar

more work on sugar + simplify Trueprop + eq idiom everywhere

renamed "disc_exclus" theorem to "disc_exclude"

more work on FP sugar

smarter "*" syntax -- fallback on "_" if "*" is impossible

more work on FP sugar

renamed theorem

tuned TODO comment

allow pseudo-definition of is_Cons in terms of is_Nil (and similarly for other two-constructor datatypes)

removed oddities

allow "*" to indicate no discriminator

tuned TODOs

started work on sugared "(co)data" commands

export "wrap" function

eliminated obsolete "parallel_proofs = 0" restriction (cf. 0e5b859e1c91)

no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;

enable parallel terminal proofs in interaction;

misc tuning;

merged

killed internal output

generate coinductive witnesses for codatatypes

generalized signature

added examples for testing of coinductive witnesses

continue with more robust dummy session after failed startup;

prefer old startup dialog scheme (cf. 514bb82514df);

more permissive handling of plugin startup failure;

bypass slow check for inlined files, where it is not really required;

more direct access to all-important chunks for text painting; clarified line_start offset: physical line start not start(i);

merged

added annotations after condition in if and while

merge, resolving trivial conflict;

forgot to add lemmas

hide newly introduced constant Sublist.sub to allow for name sub in TreeFsetI

reverted (accidentally commited) changes from changeset fd4aef9bc7a9

reverted (accidentally commited) changes from changeset fd4aef9bc7a9

added theory instantiating type class order for list prefixes

Main is implicitly imported via Sublist

added author

List is implicitly imported by Main

introduced "sub" as abbreviation for "emb (op =)"; Sublist_Order is now based on Sublist.sub; simplified and moved most lemmas on sub from Sublist_Order to Sublist; Sublist_Order merely contains ord and order instances for sub plus some lemmas on the strict part of the order

base Sublist_Order on Sublist (using a simplified form of embedding as sublist relation)

dropped ord and bot instance for list prefixes (use locale interpretation instead, which allows users to decide what order to use on lists)

more lemmas on suffixes and embedding

changed arguement order of suffixeq (to facilitate reading "suffixeq xs ys" as "xs is a (possibly empty) suffix of ys)

added embedding for lists (constant emb)

renamed (in Sublist): postfix ~> suffixeq, and dropped infix syntax >>=

renamed (in Sublist): prefix ~> prefixeq, strict_prefix ~> prefix

renamed theory List_Prefix into Sublist (since it is not only about prefixes)

compile

rearrange dependencies

renamed three BNF/(co)datatype-related commands

tuned boundary cases of command-line; adhoc removal of PDFs stemming from base sessions;

"isabelle logo" produces EPS and PDF format simultaneously; more robust invocation of epstopdf: avoid filter mode;

actually reset output when there is no valid command span here (especially relevant at very end of jEdit buffer, which lacks the terminating newline);

tuned proofs;

some parallel ML;

proper classpath on windows;

proper classpath for Java FX;

basic setup for HTML5 panel; more JFX_Thread.operations;

basic support for Java FX;

maintain stable state of node entries from last round -- bypass slightly different Thm.join_theory_proofs;

removed unused material;

discontinued complicated/unreliable notion of recent proofs within context;

central management of forked goals wrt. transaction id; clarified stable_exec_id: consider ragular failure as stable; more robust counting of forked proofs, with global reset after cancellation due to document editing;

merged

always register proofs, even for empty binding;

tuned signature;

made parser a bit more flexible

tuning

pad the selectors' list with default names

generate default names for selectors

renamed "disc_disjoint" property "disj_exclus"

optimized "mk_split_tac" + use "notes"

optimized "mk_case_disc_tac" further

optimized "mk_case_disc_tac"

tuning

rationalized data structure for distinctness theorems

optimized "case_cong" proof

allow default names for selectors via wildcard (_) + fix wrong index (k)

minor fixes (for compatibility with existing datatype package)

generate "split_asm" property

generate "split" property

more precise register_proofs for local goals; tuned signature;

more informative error message from failed goal forks (violating old-style TTY protocol!);

avoid empty tooltips;

clarified command status (again);

recovered ScrollPane from d899be1cfe6d;

more markup for failed goal forks, reusing "bad";

further refinement of command status, to accomodate forked proofs;

merged;

make parallel list indexing possible for inject theorems

generate "weak_case_cong" property

generate "case_cong" property

generate "case_disc" property

generate "ctr_sels" theorems

generate "disc_exhaust" property

generate "disc_distinct" theorems

added discriminator theorems

adjust example

more work on sugar

updated Java-related error message

changed order of arguments to "bnf_sugar"

define selectors and discriminators

tuning

more work on BNF sugar -- up to derivation of nchotomy

more work on BNF sugar

renamed ML function for consistency

started work on datatype sugar

killed obsolete "bnf_of_typ" command

removed dead code

have "bnf_of_typ" command seal the BNF

register proofs of Isar goals, to enable recovery from unstable command states after interactive cancellation;

refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390); stretched meaning of Goal.parallel_proofs to enable future_terminal_proofs in interactive document model, despite its lack for regular forking of proofs;

some support for registering forked proofs within Proof.state, using its bottom context; tuned signature;

tuned signature;

refined status of forked goals;

proper merge of promises to avoid exponential blow-up in pathologic situations (e.g. lack of PThm wrapping);

tuned message;

discontinued old init_components script, superseded by init_components shell function as explained in README_REPOSITORY;

approximative build of pdf documents in 1 pass instead of 3;

more formal isabelle makedist from repository;

removed remains of generated material, which tends to rot;

one more round to ensure that base images are already there, without producing document output themselves;

more robust document setup;

provide polyml-5.4.1 as regular component; discontinued old-style choosefrom settings with hardwired defaults;

clarified handling of raw output messages;

no attempt to build documentation for now -- requires ML_HOME etc. which is not present here;

command 'use' is legacy;

clarified separated_chunks vs. space_explode;

more precise indentation;

modernized specifications;

tuned signature;

renamed Position.str_of to Position.here;

init components from local clone that is used to produce the test distribition, which itself lacks Admin;

discontinued centralistic changelog;

discontinued odd copy of eps logos (cf. 8fc3828fdc8a);

prefer cp over mv, to reduce assumptions about file-system boundaries and GNU vs. non-GNU tools;

removed odd left-over file;

update on "isabelle build" and "isabelle build_doc";

renamed doc-src to src/Doc; renamed TutorialI to Tutorial;

do not hardwire document output options -- to be provided by the user;

more permanent update of keywords (cf. 3517d6f50b12);

merged

updated keywords

fixed import paths in examples

fixed import paths

tuning

updated NEWS and CONTRIBUTORS

documentation cleanup

added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)

Typo fixed.

updated .hgignore to reflect to (almost) clean result of build_doc;

more formal build_doc tool (Admin only); removed some doc-src junk;

prepare document more uniformly; fewer latex runs, in accordance to "isabelle document"; apply fixbookmarks last to operate on final root.out;

prefer \input which actually checks file existence;

tuned;

prefer (old) isa-index as provided here, to get exactly the same index layout as in Isabelle2012; more accurate ROOT/files;

removed old stuff;

more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;

removed old stuff;

removed historic manual;

more standard document preparation within session context;

more standard document preparation within session context;

updated IsarRef/document/style.sty;

missing file;

removed junk;

more standard document preparation within session context;

removed outdated IsarRef/Thy/HOLCF_Specific.thy -- make IsarRef depend on HOL only;

prefer doc-src/pdfsetup.sty; moved IsarRef/Thy/ZF_Specific.thy to ZF/ZF_Isar.thy to avoid dependence of IsarRef on another object-logic;

more official way to set margin;

avoid clash with generated Adaptation.tex on case-insensible file-systems;

missing file;

deactivate updated doc-src sessions, to make Admin/build doc and makedist work for now;

more standard document preparation within session context;

more standard document preparation within session context;

more standard document preparation within session context;

more standard document preparation within session context;

more standard document preparation within session context;

more standard document preparation within session context;

more standard document preparation within session context;

more standard document preparation within session context;

more standard document preparation within session context;

more standard document preparation within session context;

more standard document preparation within session context;

more portable perl invocation;

more standard document preparation within session context;

more standard document preparation within session context; more uniform document build;

more standard document preparation within session context;

clarified "isabelle logo";

clarified document directories: browser_info as backdrop vs. optional output directory in the foreground;

less ambitious test -- terminate more quickly;

tuned;

actual use of (sos remote_csdp) via ISABELLE_FULL_TEST;

test with many add-ons;

updated Theory.begin_theory;

entity markup for theory Pure, to enable hyperlinks etc.;

more accurate defining position of theory;

theory def/ref position reports, which enable hyperlinks etc.; more official header command parsing;

fixed theory dependency

more convenient switching of buffers;

report source path and let front-end resolve implicit master location (e.g. URL);

prefer jEdit file name representation (potentially via VFS); tuned;

more precise counting of line/column;

support for direct hyperlinks, without the Hyperlinks plugin;

tuned signature;

some markup for inlined files;

check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);

updated READMEs -- most Mac OS X problems are gone thanks to jdk-7u6;

clarified syntax boundary cases and errors;

simplified JVM startup, based on stronger assumptions about the Java version provided as Isabelle component;

eliminated obsolete byte_reader -- theory headers + body files are parsed in full;

more direct File.read_bytes -- avoid cumulative copying of StringBuilder;

improved errors of parser combinators;

tuned messages: end-of-input rarely means physical end-of-file from the past;

merged

remove Hoare dependency from Fold.thy

added specific 'spark_open_vcg' and 'spark_open_siv' with formal management of corresponding source files;

turned 'boogie_open' into thy_load command, without any declarations of 'uses';

tuned signature;

clarified type Token.file;

expand all files uniformly;

added build option -l (list files);

prefer classic take_prefix/take_suffix over chop_while (cf. 0659e84bdc5f);

more basic file dependencies -- no load command here;

tuned signature (again, cf. ff9cd47be39b);

updated Thy_Load.check_thy;

simplified Thy_Load.check_thy (again) -- no need to pass keywords nor find files in body text;

tuned signature;

simplified Thy_Load.provide: do not store full path;

prefer ML_file over old uses; updated generated files;

merged

abstracted lemmas

prefer ML_file over old uses;

prefer ML_file over old uses;

'ML_file' evaluates ML text from a file directly within the theory, without predeclaration via 'uses';

add keywords of this node as well (e.g. relevant for Pure.thy);

tuned;

tuned message -- dynamic loading happens routinely, e.g. in TTY/PG interaction;

discontinued separate list of required files -- maintain only provided files as they occur at runtime; tuned signature;

find files via load commands within theory text; clarified Thy_Load.with_thy_text, simplified Thy_Load.check_thy;

clarified global get_recent_syntax: session always has its base_syntax, but it might be absent itself;

pass syntax through check_thy;

use Thy_Header.read on explicit text only -- potentially via File.read, not Scan.byte_reader; tuned signatures;

clarified Parse.path vs. Parse.explode -- prefer errors in proper transaction context;

tuned;

clarified bootstrapping of Pure;

tuned errors;

prefer File.full_path in accordance to check_file;

more standard Thy_Load.check_thy for Pure.thy, relying on its header; pass uses and keywords from Thy_Load.check_thy to Thy_Info.load_thy; clarified 'ML_file' wrt. Thy_Load.require/provide, which is also relevant for Thy_Load.all_current;

updated Thy_Load.check_thy;

refined Thy_Load.check_thy: find more uses in body text, based on keywords; refined Thy_Info.require_thy(s): cumulate additional keywords; slightly more value-oriented type Keywords.keywords;

more direct cumulation of (sparse) keywords; discontinued slightly odd patching of Pure keywords; tuned signature;

some support for thy_load_commands; clarified signatures;

tuned signature;

clarified initialization of Thy_Load, Thy_Info, Session;

tuned;

more robust cleaning of "% tag" and "-- cmt";

some support for inlining file content into outer syntax token language;

tuned comment;

tuned;

added keyword kind "thy_load" (with optional list of file extensions);

updated generated files;

more strict syntax, according to manual;

abstracted lemma

retain unknown options within preferences; tuned print;

more comprehensible platform family name;

tuned message;

fewer components, more roots;

actually remove makeall (cf. 292b97e17fb7);

tuned;

Backed out changeset ec82c33c75f8;

Typo fixed.

merged

merged

fixed lemmas

abstracted lemmas

updated to new init_components, hoping that mira can digest that;

some explanations on component categories;

specific cygwin components;

obsolete;

some explanations on isabelle components;

some grouping of components;

renamed components to components_old, to make room for some directory of the same name;

minor robustification;

added "isabelle components" tool;

tuned;

direct support for component forests via init_components; explicit ISABELLE_COMPONENTS_MISSING;

allow to provide external ISABELLE_IDENTIFIER for repository clone -- potentially relevant for isatest and mira; clarified spaces in file names -- ISABELLE_HOME is non-critical after abolishment of "make";

tuned;

tuned;

updated component repository;

updates on 32 bit vs. 64 bit platforms; added Mountain Lion; dropped Leopard; tuned;

updated to jedit_build-20120813, pointing to another contrib directory as a change;

merged

tuned proofs;

look in current directory first before looking up includes in the TPTP directory, as required by Geoff

prefer eta-expanded code equations for fold, to accomodate tail recursion optimisation in Scala

more robust multi-platform support;

updated to jdk-7u6 and jedit_build-20120813 -- NB: plain Isabelle/Scala still happens to work with jdk-6;

support for jdk-7u6 component;

Clarification: free variables allowed in interpreted locale instances.

merged

fixed proof

abstracted lemmas

Backed out changeset 6cf7a9d8bbaf

abstracted lemmas

merged

Turned into Admin tool download_components.

tuned;

tuned;

some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");

tuned;

fixed handling of "int" in the wake of its port to the quotient package

removed dead code

merged

Added various options, notably -c to download components listed in Admin/components. Also, curl instead of wget.

ignore some administrative files on newer Mercurial versions as well;

some support for persistent user preferences;

merged

explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;

more direct interpretation of document_variants for build (unchanged for usedir);

tone down "z3_tptp", now that Z3 (starting with 4.1) no longer supports TPTP TFF0

fixed then-else confusion

tweak Vampire setup in the light of new evaluation

improved set of reconstructor methods

warn users about unused "using" facts

be less aggressive at kicking out chained facts

recognize bus errors as crash

consider removing chained facts last, so that they're more likely to be kept

clarified format of etc/options: only declarations, not re-definitions;

check_errors for cumulative session content;

even more defensive path expansion (see also 8d381fdef898);

support for 'typ' with explicit sort constraint;

added jedit option -d;

always retain doc-src (as regular component);

merged