dropped lazy code equations

CONTRIBUTORS

always qualify NJ's old List.foldl/foldr in Isabelle/ML;

eliminated duplicate fold1 -- beware of argument order!

uniform use of Integer.add/mult/sum/prod;

Removed dead code in function mk_deftab.

Removed unneeded reference to inv_def.

Replaced inv by the_inv_onto.

Renamed inv to the_inv and turned it into an abbreviation (based on the_inv_onto).

fixed proof (cf. d1d4d7a08a66);

removed disjunctive group cancellation -- provers run independently; sledgehammer: kill earlier session, and removed obsolete max_atps; tuned;

tuned;

removed some unreferenced material; tuned;

merged

certificates for sos

merged

added sums of squares for standard deviation

merged

Inv -> inv_onto, inv abbr. inv_onto UNIV.

disable indent-tabs-mode in Proof General / Emacs;

merged

made SML/NJ happy;

Merged.

Finished revisions of locales tutorial.

Changed part of the examples to int.

Save current state of locales tutorial.

Observe order of declaration when printing registrations.

disable sunbroy2 for now;

tuned/moved divide_and_conquer';

tuned;

removed separate record_quick_and_dirty_sensitive;

simplified tactics; use proper SUBGOAL/CSUBGOAL;

eliminated old List.foldr and OldTerm operations; misc tuning;

removed unused names;

misc tuning and simplification;

less pervasive names;

operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;

Method.cheating: check quick_and_dirty here;

tuned;

Unsynchronized.set etc.;

indicate CRITICAL nature of various setmp combinators;

ISABELLE_TOOL;

tuned signature; observe coding conventions of this file;

merged

merged

added the_inv_onto

eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;

removed obsolete old goal command;

legacy Drule.standard is no longer pervasive;

explicitly qualify Drule.standard;

tuned white space;

local channels for tracing/debugging;

made SML/NJ happy;

sunbroy2: back to single-threaded mode for now -- deadlock in Poly/ML 5.3-SVN-900;

replaced String.concat by implode; replaced String.concatWith by space_implode; replaced (Seq.flat o Seq.map) by Seq.maps; replaced List.mapPartial by map_filter; replaced List.concat by flat; replaced (flat o map) by maps, which produces less garbage;

space_implode;

normalized aliases of Output operations;

eliminated slightly odd get/set operations in favour of Unsynchronized.ref; eliminated aliases of Output operations; print_cert: use warning for increased chance that the user actually sees the output; misc tuning and simplification;

natural argument order for prover; renamed atp_problem to problem; standard naming convention for the_system;

ATP_Manager.get_prover: canonical argument order; eliminated various aliases of existing operations, notably Output channels; tuned messages; misc tuning and clarification;

tuned proof (via atp_minimized);

sort_strings (cf. Pure/library.ML);

clarified File.platform_path vs. File.shell_path; tuned;

exported File.shell_quote;

misc tuning and recovery of Isabelle coding style;

eliminated extraneous wrapping of public records; tuned;

tuned signature; tuned;

renamed functor HeapFun to Heap;

misc tuning and clarification;

structure ATP_Manager: eliminated slightly odd get/set operations in favour of Unsynchronized.ref; uniform interpretation of ATP_Manager.atps via ATP_Manager.get_atps;

modernized structure names;

show direct GC time (which is included in CPU time);

eliminated obsolete C/flip combinator;

added List.nth

tuned make parameters for sunbroy2;

accomodate old version of "tail", e.g. on sunbroy2;

settings for parallel experimental Poly/ML 5.3;

sharpened name

more explicit notion of canonized code equations

more explicit notion of canonized code equations

tuned whitespace

tuned whitespace

dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology

merged

deactivated Datatype.distinct_simproc

dropped Datatype.distinct_simproc; tuned

order conjunctions to be printed without parentheses

approximation now fails earlier when using interval splitting; value [approximate] now supports bounded variables; renamed Var -> Atom for better readability

merged

added add_tyconames; tuned

merged

more appropriate abstraction over distinctness rules

merged

intro_base_names combinator

merged

dropped dist_ss

merged

added is_IVar

factored out Code_Printer.aux_params

dropped rule duplicates

less non-standard combinators

nth replaces List.nth

dropped redundancy

dropped dead code

using distinct rules directly

simplified proof

dropped simproc_dist formally

tuned order of lemmas

term styles also cover antiquotations term_type and typeof

merged

lookup for datatype constructors considers type annotations to resolve overloading

added group_stmts

moved labelled_name to code_thingol

updated generated documentation

corrected syntax diagrams for styles

new generalized concept for term styles

generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles

isatest: store test identifiers

tuned proofs

added bot_boolE, top_boolI

do not use Locale.add_registration_eqs any longer

Inf/Sup now purely syntactic

merged

inf/sup1/2_iff are mere duplicates of underlying definitions: dropped

merged

added Coset as constructor

sets and cosets

added syntactic Inf and Sup

merged

New lemmas connected with the reals and infinite series

New facts about domain and range in

merged

experimental de-facto abolishment of distinctness limit

tuned handling of type variable names further

variables in type schemes must be renamed simultaneously with variables in equations

explicitly unsynchronized

explicitly unsynchronized

recovered support for Spass: re-enabled writing problems in DFG format

avoid exception Option: only apply "the" if needed

merged

atp_minimal using chain_ths again

merged

re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values, eliminated unused provers, turned references into configuration values

eliminated dead code; tuned;

eliminated dead code and redundant parameters; tuned;

eliminated dead code;

replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools; tuned;

replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools;

Refute.refute_goal: goal addressing from 1 as usual;

Refute.refute_goal: canonical goal addresses from 1 (renamed from refute_subgoal to clarify change in semantics); command 'refute': Proof.flat_goal provides standard view on internally structured Isar goal, suitable for (semi)automated tools;

clarified Proof.refine_insert -- always "refine" to apply standard method treatment (of conjunctions);

misc tuning and simplification;

macbroy2: bigger jobs first, to avoid danger of swapping during daytime;

less ambitious heap settings;

merged

merged

proper merge of interpretation equations

merged

Merged again.

Merged.

News entry: inheritance of mixins; print_interps.

Avoid administrative overhead for identity mixins.

tuned;

moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;

added Ctermtab, cterm_cache, thm_cache; tuned;

added term_cache; tuned;

Concurrently cached values.

tuned header; tuned whitespace;

core_sos_tac: SUBPROOF body operates on subgoal 1; tuned;

merged

updated generated files;

enable slow-motion mode to accomodate unsynchronized refs within theory sources;

avoid unsynchronized refs within theory sources;

explicitly Unsynchronized;

additional fixes in normarith.ML due to FuncFun and FuncUtil changes

changed core_sos_tac to use SUBPROOF

replaced and tuned uses of foldr1

tuned FuncFun and FuncUtil structure in positivstellensatz.ML

removed opening of structures

merged

merged

merged

made spass additional default prover

merged

Proved a new theorem: nat_to_nat2_inj

turned unsynchronized ref into synchronized var

merged

resolved conflict

record max lemmas used

Lazy evaluation with memoing (sequential version).

more official status of sequential implementations; tuned;

separate concurrent/sequential versions of lazy evaluation; lazy based on future avoids wasted evaluations;

added Task_Queue.depend (again) -- light-weight version for transitive graph; Future.join_results: record explicit dependency, detect direct task-task join cycles; Future.join_results: no change of interruptibility, allows to interrupt wait; added Future.worker_task; ThyInfo.schedule_futures: uninterruptible outer join;

handle Pattern.MATCH, not arbitrary exceptions; misc tuning, trying to reduce line length a bit;

more precise dependencies;

eliminated redundant parameters;

back to simple fold_body_thms and fulfill_proof/thm_proof (reverting a900d3cd47cc) -- the cycle check is implicit in the future computation of join_proofs;

avoid mixed l/r infixes, which do not work in some versions of SML;

tuned;

merged

explicitly Unsynchronized

Merged.

Propagation of mixins for interpretation; reactivated diagnostic command print_interps.

Archive registrations by external view.

Stricter test: raise error if registration generates duplicate theorem.

Explicit management of registration mixins.

Improved comments and api names.

eliminated dead code, redundant bindings and parameters; use === term operator, which is defined here; handle Type.TYPE_MATCH, not arbitrary exceptions; misc tuning and simplification;

misc tuning and simplification; be explicit about expressions involving infixes with non-obvious priorities; removed dead code; some attempts to recover basic Isabelle coding conventions;

eliminated dead code; eliminated redundant bindings; misc tuning;

eliminated dead code;

Sorts.of_sort_derivation: no pp here;

eliminated redundant bindings; schedule_tasks/require_thy: eliminated obsolete tasks_len, which was a leftover from theory-only parallelization;

actually perform Isar_Document.init on startup;

eliminated dead code; eliminated redundant parameters;

removed dead code; Sorts.of_sort_derivation: removed unused pp;

handle Type.TYPE_MATCH, not arbitrary exceptions;

removed redundant Sign.certify_prop, use Sign.cert_prop instead; tuned;

PARALLEL_GOALS: proper scope for exception FAILED, with dummy argument to prevent its interpretation as variable;

actually export unit parser;

eliminated dead code;

eliminated redundant parameters;

eliminated redundant bindings;

merged

moved lemmas about sup on bool to Lattices.thy

moved lemmas about sup on bool to Lattices.thy

tuned proofs

tuned headings

report unreferenced ids;

tuned whitespace;

more uniform treatment of structure Unsynchronized in ML bootstrap phase;

merged

mandatory prefix where appropriate

mandatory prefix where appropriate

tuned whitespace

replaced chained_goal by slightly more appropriate flat_goal;

made SML/NJ happy;

added chained_goal, which presents the goal thm as seen by semi-structured methods;

tuned;

removed dead/duplicate code;