removed obsolete test_markup; tuned;

Proof General interaction always uses Isar loop; pass Isabelle/Scala options to Proof General process as well;

proper context;

merged

more direct PGIP/Emacs processing and output;

more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;

removed redundant modules;

removed some obsolete PGIP/PGEclipse material;

never open structure Unsynchronized (cf. "implementation" manual);

prefer explicitly qualified exceptions, which is particular important for robust handlers;

avoid PolyML.makestring, even in dead code;

fixed bug introduced when reintroducing set constructor, and visible when applying <= to 2- or more-ary relations, e.g. "(R::'a=>'a=>bool) <= R"

don't apply an unnecessary morphism

tuned

relator coinduction for codatatypes

standard ivl notation [l,h]

merged

tuned

avoid polymorphic uncurried aliases with more arguments than there are arguments in the most general type of a HOL constant, to dodge issues at declaration time

proper unmangling -- the bug is visible when "uncurried_aliases" is enabled with Alt-Ergo or Poly. SPASS

use right default for "uncurried_aliases" with polymorphic SPASS

relator induction for datatypes

store proper theorems even for fixed points that have no passive live variables

stronger monotonicity property for relators

make tactic actually work for op = as relator

tuned

hide Fin on output

removed dead argument

more robust iterator construction (needed for mutualized FPs)

tuning

removed dead internal constants/theorems

removed tracing

export one more function

added field to record

tuning

removed dead code

move function to library

tuning

more

tuning

code tuning

merge

refactoring

export one more function + tuning

do not unfold the definition of the relator as it is not defined in terms of srel anymore

tuned

got rid of the set based relator---use (binary) predicate based relator instead

tuned names + extended ML signature

merged

tuned name: filter -> constrain (longer but more intuitive)

tuning

imported patch refactor_coiter_constr

tuned

started factoring out coiter construction

rationalize ML signature

factor out construction of iterator

tuning

improved defns and proofs

undo 46d911ab9170 since it causes problems

allow '-'s in tptp ids to avoid problems with remote_vampire

added preplay tracing

handle dummy atp terms

avoid dummy annotations; terminate preplay/compression if metis fails; fixed bug

added informative error messages

tail recursive version of map, for code generation, optionally

simplified proofs

tuning

pass certain readability-enhancing Vampire options only when an Isar proof is needed

added lemma

added lemma

renamings

code tuning

signature tuning

removed dead code

tuned signature

store (co)induction rules in data structure

tuning names

got rid of needless library function (find_minimum)

one more lib function

export one more function

rationalized data structure

added and moved library functions (used in primrec code)

tuned names -- co_ and un_ with underscore are to be understood as (co) and (un)

tuning

more code rationalization

more code rationalization

more code rationalization

refactoring

tuned

renamed a few FP-related files, to make it clear that these are not the sum of LFP + GFP but rather shared basic libraries

tuned

tuned

tuning

export more functions (useful for primrec_new)

further enrich data structure

more

rationalized terminology (iterator = fold or rec, xxfoo = (co)foo or (un)foo)

added fields to database

tuned data structure

renamed records

added constructors to data structure

added pre-BNFs to database

lowercase type constructor, for consistency (cf. fp_result not FP_result nor FP_Result)

renamed "bnf_def" keyword to "bnf" (since it's not a definition, but rather a registration)

Added maps, sets, rels to "simps" thm collection

tuned

comment tuning

tuning

tuning

tuning

signature tuning

whitespace tuning

tuned signature

canonical names of classes

merged

register all (co)datatypes in local data

create data structure for storing (co)datatype information

avoid empty isabelletags.sty for the sake of arXiv;

merged

cygwin_root as optional argument; tuned;

use record instead of big tuple

clarified module dependencies: avoid Properties and Document introding minimal "PIDE";

merge

use base names, not full names

tune signatures

tuning

tuning

removed unreferenced thm