theory loader: removed obsolete touch/outdate operations (require_thy no longer changes the database implicitly);

avoid repeated File.read for theory text (as before); misc tuning and simplification;

tuned messages and comments;

simplified Thy_Header.read -- include Source.of_string_limited here; tuned;

simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps; explicit Thy_Info.toplevel_begin_theory, which does not maintain theory loader database; Outer_Syntax.load_thy: modify Toplevel.init for theory loading, and avoid slightly odd implicit batch mode of 'theory' command; added Thy_Load.begin_theory for clarity; structure ProofGeneral.ThyLoad.add_path appears to be old ThyLoad.add_path to Proof General, but actually operates on new Thy_Load.master_path instead -- for more precise imitation of theory loader; moved some basic commands from isar_cmd.ML to isar_syn.ML; misc tuning and simplification;

more precise stats;

merged

quickcheck images of goals under registration morphisms

get_registrations interface

restored unusual snd-biased merge/join policy -- required due to non-conservative code setups

merged

reactivated Scala check

corrected range check once more

added Code_Natural.thy

reactivated Scala check; tuned import order

reactivated Scala check

modified namespace policy

use Natural as index type for Haskell and Scala

merged

keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems; this is rather involved because the Flotter FOF-to-CNF translator is normally implicit. We must make this an explicit step and parse the Flotter output to find out which clauses correspond to which formulas.

first step in using "fof" rather than "cnf" in TPTP problems

fix polymorphic "val"

temporarily deactivating check for Scala

another refinement chapter in the neverending numeral story

inductive_cases: crude parallelization via Par_List.map;

modernized/unified some specifications;

Thy_Info.loaded_files: Thy_Load.loaded_files depends on master -- i.e. no files for finished theory;

simplified/clarified register_thy: more precise treatment of new dependencies, remove descendants; eliminated obsolete touch_child_thys, register_theory;

simplified handling of theory begin/end wrt. toplevel and theory loader;

Thy_Load.check_loaded via Theory.at_end;

tuned;

moved basic thy file name operations from Thy_Load to Thy_Header;

moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state; theory loader: reduced warnings -- thy database can be bypassed in certain situations; Proof/Local_Theory.propagate_ml_env; ML use function: propagate ML environment as well; pervasive type generic_theory;

merged

avoid unreliable Haskell Int type

proper subclass instead of sublocale

repaired tool invocation

observe standard conventions for doc-strings;

tuned message;

eliminated some unused Thy_Info operations;

refrain from generating <hr/> and from "hiding" it in isabelle.css -- the latter might be used in other situations as well;

generic external source files -- nothing special about ML here;

discontinued special treatment of ML files -- no longer complete extensions on demand; simplified Thy_Load.check_file, with uniform error reporting; added Thy_Load.test_file for non-strict checking; misc tuning and simplification;

eliminated obsolete/unused with_path(s) -- hardly usable because of CRITICAL; reset_path is CRITICAL;

tuned signature;

updated some headers;

merged

dedicated exec ... syntax for open state monad (partly already introduces in d00a3f47b607)

merged

more generous memory settings for scala check

no polymorphic "var"s

merged

adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples

do a better job at Skolemizing in Nitpick, for TPTP FOF

revert code that was submitted by mistake

renamings + only need second component of name pool to reconstruct proofs

rename "classrel" to "class_rel"

rename "combtyp" constructors

renamed "Literal" to "FOLLiteral"

renamed "HOLClause" to "FOLClause" -- it's really a FOL clause with combinators

merged

fixing quickcheck invocation in HOL-Mirabelle

hiding constants in Quickcheck_Types

adding a type for flat complete lattice to Quickcheck_Types

added new theories to IsaMakefile and ROOT.ML

adding Quickcheck examples for other quickcheck default types

adding Library theory for other quickcheck default types

removing obsolete ID in Quickcheck_Examples

correcting wellsortedness check and improving error message

using multiple default types in quickcheck

correcting merging of default_types

reordering quickcheck signature; exporting test_params and inspection function

changed default types to a list of types; extended quickcheck parameters to be a list of values to parse a list of default types

putting proof in the right context; adding if rewriting; tuned

load_thy: parallel parsing of units, which consist of statement/proof each;

eliminated some unreferenced identifiers;

tuned;

tuned comments;

replaced Source.of_list_limited by slightly more economic Source.of_string_limited;

deps_thy/load_thy: store compact text to reduce space by factor 12;

make SML/NJ happy, by adhoc type-constraints;

recovered benchmarks, which are not tested automatically;

made SML/NJ happy;

merged

abstract visualization of locale ingredients; all_locales yields proper locale identifiers

tuned

accomodate for scope of "as" binding in ML

tuned code

datatype classes are abstract

avoid deprecation

robustified metis proof

modernized abel_cancel simproc setup

keep explicit diff_def as legacy theorem; modernized abel_cancel simproc setup

diff_eq_diff_less_eq' replaces diff_eq_diff_less_eq

diff_minus subsumes diff_def

tuned whitespace

dropped essentially ineffective tuning

discontinued pretending that abel_cancel is logic-independent; cleaned up junk

merged

merged

distinguish different classes of const syntax

Scala: subtle difference in printing strings vs. complex mixfix syntax

check code generation for Scala

dropped superfluous prefixes

optional break

consolidate const_syntax naming

recovered benchmarks, which are not tested automatically;

reactivate SML/NJ test on macbroy28, while macbroy23 is unavailable;

eliminated old time_use/time_use_thy variants -- timing is implicitly controlled via Output.timing; misc tuning and simplification;

moved src/Tools/Compute_Oracle to src/HOL/Matrix/Compute_Oracle -- it actually depends on HOL anyway;

replaced Thy_Info.the_theory by Context.this_theory -- avoid referring to accidental theory loader state;

thm_deps/unused_thms: Context.get_theory based on proper theory ancestry, not accidental theory loader state;

explicit dependency on theory HOL;

ML antiquotations @{theory} and @{theory_ref} refer to the theory ancestry, not any accidental theory loader state; recovered @{theory_ref NAME} (cf. 1f09a22a1027);

added Context.get_theory -- avoid referring to accidental theory loader state (cf. Thy_Info.get_theory);

thy_deps: more direct comparison of sessions, which is presumably what "unfold" is meant to indicate here -- also avoid referring to accidental theory loader state;

clarified/exported Future.worker_subgroup, which is already the default for Future.fork;

qualified Thy_Info.get_theory;

discontinued pervasive val theory = Thy_Info.get_theory -- prefer antiquotations in most situations;

further Mac OS X deviations;

warning in proper transaction context;

SML/NJ: refrain from modifying toplevel pp for type string -- unclear if it could work here;

avoid duplicate printing of 'theory' state (cf. 173974e07dea);

toplevel pp for Proof.state and Toplevel.state;

execute document version at high priority;

Topelevel.run_command: interactive mode for initial 'theory' ensures that Thy_Info.begin_theory loads parent theories;

edit_document: join parent execution in synchronous/uninterruptible mode, to prevent spurious interrupts when cascaded executions run into each other;

back to more strict dependencies, even for canceled groups (reverting parts of 02936e77a07c); cancel passive tasks more actively via Exn.Interrupt, by treating them like ragular jobs here; attempts to re-assign canceled futures/promises raise Exn.Interrupt; tuned;

export Graph.get_entry for convenience;

eliminated old-style sys_error/SYS_ERROR in favour of exception Fail -- after careful checking that there is no overlap with existing handling of that; tuned some error messages;

tuned;

observe follow_caret (again);

Session: predefined real time parameters; Document_View: delayed caret handling, for improved reactivity; selected_command: proper_command_at ignores ignored commands;

bind and then latex symbols

minor update of dependencies;

corrected range chec

first roughly working version of Imperative HOL for Scala

tuned

merged

a first sketch for Imperative HOL witht Scala

don't fail gracefully

restored long-broken syntax sanity checks

tuned interpunctation

fragments of Scala

merged

adjusted; fixed typo

dropped spurious export_code

use different log server (macbroy23 down)

more consistent spacing in generated monadic code

braced needed in layout-insensitive syntax

repaired some implementations of imperative operations

repaired reference implementation for OCaml

part of pervasive test

avoid ambiguities; tuned

repaired of_list implementation for SML, OCaml

avoid export_code ... file -

explicit optional checking

added Isar syntax for code checking

corrected import

use generic description slot for formal code checking

formal slot for code checker

export_code without file prints to standard output

check without explicit path

load cache_io before code generator; moved adhoc-overloading to generic tools

tuned infix syntax

dropped M suffix; added predicate monad bind

self-built symbol for part of bind operator

redirect stderr to stdout

merged

merged

corrected mixfix declarations and tidied proofs

merged

Fixed syntax and tidied some proofs

correcting function name of generator for products of traditional code generator (introduced in 0040bafffdef)

consolidated names of theorems

qualified names for (really) all array operations

canonical argument order for get

qualified names for (almost) all array operations

canonical argument order for present

canonical argument order for length

merged

new crontab

merged

proper merge of operation changes and generic do-syntax

merged

hide_const; update replaces change

remove separate afp settings again, use plain mac-poly64-M4 instead.

merged

new settings for afp test

Heap_Monad uses Monad_Syntax

State_Monad uses Monad_Syntax

uniform do notation for monads

generic ad-hoc overloading via check/uncheck

corrected title

theorem collections do not contain default rules any longer

fixed handling of Ball/Bex: turn equalities into meta-equalities for the rewriting conversions; added tests for Ball/Bex

removed unused/untested IOA 'automaton' package;

removed impractical tolerate_legacy_features flag;

tuned comment;

removed legacy aliases;

moved misc legacy stuff from OldGoals to Misc_Legacy; OldGoals: removed unused strip_context, metahyps_thms, read_term, read_prop, gethyps;

eliminated OldGoals.strip_context;

removed old HOL/HOLCF-Modelcheck setup, which has been unused/untested for many years;

do not intercept ML exceptions -- printing exception positions/text is the job of the Isar/ML toplevel; use up-to-date ML_Compiler.exn_message;

some modernization of really ancient Meson experiments;

dropped empty theory

moved auxiliary lemma

dropped unused lemmas of dubious value

dropped unused lemmas of dubious value

split off mrec into separate theory

spelt out relational framework in a consistent way

avoid explicit mandatory prefix markers when prefixes are mandatory implicitly

merged

moved co-regularity to class section; avoid duplicated class_deps

dropped superfluous [code del]s

merged

dropped superfluous [code del]s

more regular session structure

regular image setup for HOL-Library (cf. 4915de09b4d3 and ccae4ecd67f4) -- note that document preparation requires a separate session directory, and library.ML is a bit too generic as a file in the default load path;

merged

Added current crontab of macbroy28

moved example to its own file in HOL/ex

merged

pervasive success combinator

added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"

avoid slightly odd "M" suffix; rename mapM to fold_map (fold_map_abort would be more correct, though)

adapted to changes

guard combinator

tuned reference theory

tuned array theory

nicer xsymbol syntax for fcomp and scomp

dropped ancient in-place compilation of SML; more tests

updated documentation

dropped ancient in-place compilation of SML

more accurate dependencies

empty default

checking generated code for various target languages

tuned titles

tuned module names

tuned tabs

tuned script

combinator with_tmp_dir

rm_tree: remove entire file system trees

Boxes may now have different widths.

tuned

replaced manual derivation of equations for inductive predicates by automatic derivation by inductive_simps

added NEWS entry

added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation

merged

generalize type of is_interval to class euclidean_space

section -> subsection

generalize some lemmas about derivatives

uniqueness of Frechet derivative

implode pseudo utf8, i.e. decode byte-stuffed low ASCII characters;

merged

even more fun with primrec

refactored reference operations

tuned

tuned empty heap

merged

merged

Unification (flexflex) bug fix; making "auto" deterministic

moved "open" operations from Heap.thy to Array.thy and Ref.thy

only definite assignment

moved special operation array_ran here

remove primitive operation Heap.array in favour of Heap.array_of_list

tuned proof

tuned

Outer_Syntax.prepare_command: disallow control commands here, and consequently in Isar documents;

specific ML_val vs. ML_command;

async_state: report within proper transaction context;

merged

simplified representation of monad type

attempt to reconstruct missing HOL/Codegenerator_Test/ROOT.ML;

merged

updated document

dropped passed irregular names

adapt Nitpick to "prod_case" and "*" -> "sum" renaming; the code in "Nitpick_Preproc", which sorted the types using "typ_ord", was wrong and evil; it seems to have worked only because "*" was called "*"

remove needless signature entry

references to ghc and ocaml

explicit code_datatype declaration prevents multiple instantiations later on

refrain from using datatype declaration -- opens chance for quickcheck later on

tuned proof

reverted to verion from fc27be4c6b1c

traceback for error messages

accomodate for different behvaiour of nitpick (c.f. also 180e80b4eac1)

introduced distinct session HOL-Codegenerator_Test

tuned bootstrap files

remove codegeneration-related theories from big library theory

drop unconvenient code declarations

build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test

general Future.report -- also for Toplevel.async_state;

simplified Isabelle_Process.Result: use markup directly;

run_command: actually observe "print" flag;

Toplevel.run_command: asynchronous state output, as an attempt to address potentially slow pretty printing (e.g. in HOL/Bali);

more precise timing;

more efficient document model/view -- avoid repeated iteration over commands from start, prefer bulk operations; misc tuning;

standard argument order; tuned;

do not open auxiliary ML structures; misc tuning;

tuned white space;

fixed spelling

merged

"prod" and "sum" replace "*" and "+" respectively; qualified constants Set.member and Set.Collect

"prod" and "sum" replace "*" and "+" respectively

qualified constants Set.member and Set.Collect

"prod" and "sum" replace "*" and "+" respectively; qualified constants Set.member and Set.Collect

merged

convert theorem path_connected_sphere to euclidean_space class

generalize more lemmas from ordered_euclidean_space to euclidean_space

avoid Old_Number_Theory; more precise dependencies;

misc tuning and modernization;

merged

once more a try with mkdir_leaf

refined semantics of mkdir_leaf: do not fail if directory already exists

avoid bitstrings in generated code

Updated NEWS

Add theory for indicator function.

Instantiate product type as euclidean space.

merged

repaired line ending

revert to plain for now mkdir

one unified Word theory

more speaking names

more speaking names

moved specific operations here

more speaking theory names

more speaking theory names

use existing bit type from theory Bit

split off Cardinality from Numeral_Type

added literal and typerep instances

mkdir_leaf -- avoiding surprises with typos in user-given paths

generalize some lemmas about derivatives

add lemma at_within_interior

generalize more euclidean_space lemmas

minimize dependencies on Numeral_Type

change type of 'dimension' to 'a itself => nat

generalize some euclidean_space lemmas

merged

rewrote the TPTP problem generation code more or less from scratch; there is now an explicit AST data structure which will make it easy to support alternative formats (e.g., DFG, sorted TPTP, sorted DFG); also, if "full_types" is enabled, "hAPP" is then tagged properly

rename functions

merged

unfold_fun_n

pervasive tuning of code

explicit printing function for applify

fail with low-level exception, not user error;

eliminated some unused bindings;

recovered some indentation from the depths of time;

cleaned by using descending instead of lifting

merged

move function

compile

compile

more elegant cheating

Sledgehammer can save some msecs by cheating

more precise error message for remote ATPs

move blacklisting completely out of the clausifier; the only reason it was in the clausifier as well was the Skolem cache

rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems

move "nice names" from Metis to TPTP format

move functions not needed by Metis out of "Metis_Clauses"

no setup is necessary anymore

adapt call

remove obsolete component of CNF clause tuple (and reorder it)

killed "expand_defs_tac"; it has no raison d'etre now that Skolemization is always done "inline"; the comment in the code suggested that it was used for other things as well but the code clearly did nothing if no Skolem "Frees" were in the problem

get rid of Skolem cache by performing CNF-conversion after fact selection

always perform "inline" skolemization, polymorphism or not, Skolem cache or not

always perform relevance filtering on original formulas

merged

split off predicate compiler into separate theory

split off predicate compiler into separate theory

adapted to reorganization of auxiliary list operations; split off predicate compiler into separate theory

adapted to change in interface

updated generated document

tuned

merged

tuned theory text

inner_simps is not enough, need also local facts

put section on distinctness before listsum; refined code generation operations; dropped ancient infix mem

explicit is better than implicit

avoid List.all

tuned whitespace

tuned lemma formulations

list_ex replaces list_exists

tuned syntax

explicit is better than implicit

modernized specifications

dropped ancient infix mem

dropped ancient infix mem; refined code generation operations in List.thy

cosmetics: avoided statement of raw theorems, used the method descending instead

separated the lifting and descending procedures in the quotient package

separation of translations in derive_qtrm / derive_rtrm (similarly for types)

merged constants "split" and "prod_case"

merged constants "split" and "prod_case" -- nitpick behaves differently

tuned whitespace

merged

compile

merged

multiplexing

factor out thread creation

factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration

update docs

simpler argument

got rid of "respect_no_atp" option, which even I don't use

reorder ML files

renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer

merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME

get rid of type alias

exploit "Name.desymbolize" to remove some dependencies

renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier"; the new name reflects that it's not used only by Sledgehammer (but also by "meson" and "metis") and that it doesn't only clausify facts (but also goals)

fewer dependencies

more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe

more moving around of ML files in "Sledgehammer.thy"

got rid of needless exception

move "MESON" up; the ultimate goal is to make Sledgehammer depend on MESON and Metis, rather than a big spaghetti

remove junk

further reduce dependencies on "sledgehammer_fact_filter.ML"

move "prepare_clauses" from "sledgehammer_fact_filter.ML" to "sledgehammer_hol_clause.ML"; since it has nothing to do with filtering

merged

Quotient package reverse lifting

Add reverse lifting flag to automated theorem derivation

Restrict quotient definitions to constants

mixfix can be given for automatically lifted constants

streamlined the generation of quotient theorems out of raw theorems

merged

avoid REPEAT after THEN_ALL_NEW

refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched;

treat alternative newline symbols as in Isabelle/ML;

simplified text_area_painter, with more precise treatment of visible line end;

merged

merged

eta-expand

improve the natural formula relevance filter code, so that it behaves more like the CNF one

split SPASS time slot between SOS and non-SOS, in case SOS times out

yields ill-typed ATP/metis proofs -- raus!

make sure "metisFT" is tried upon "metis" failure in "resolve_inc_tyvars"

merged

more direct definition simplifies proofs

merged

more precise tactic: do not escape to a different goal branch (REPEAT is still problematic, though)

a76ace919f1c wasn't quite right; second try

merge

never include anything from the Sledgehammer theory in the relevant facts + killed two obsolete facts

better eta-expansion in Sledgehammer's clausification; make the eta-expansion code more robust in the face of polymorphic arguments + make eta-expansion happen more often, since it first-orderizes things

cosmetics

make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds

improve the new "natural formula" fact filter

explicit treatment of UTF8 sequences as Isabelle symbols;

ML pretty printing of type string according to (quasi-abstract) YXML markup and symbols (including UTF8);

escape UTF8 symbols for the ML compiler;

explicit treatment of UTF8 character sequences as Isabelle symbols;

slight cleaning and simplification of the automatic wrapper for quotient definitions

merged

export of proper information in the ML-interface of the quotient package

treat Pretty.T as strictly abstract type;

slightly more standard data merge: Symtax.merge (K true) avoids equality on abstract type Pretty.T and gracefully accepts overriding, Symtab.join prefers first entry as usual;

avoid equality on abstract type Pretty.T;

notes on packaging;

misc tuning;

tuned auxiliary structures;

Net.encode_type;

more accurate dependencies;

made smlnj happy

fix syntax bug in the TPTP output, by ensuring that "hBOOL" is correctly used for n-ary predicates even if (n + k)-ary occurrences of the same predicate, but with a different type, occur in the same problem

renamed for easier grep

use Skolem inlining also in the nonpolymorphic case, as a step toward simplifying the source code

steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs

have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry

fix bug with "skolem_id" + sort facts for increased readability

if SPASS fails at finding a proof with the SOS option turned on, turn it off and try again

merged

this looks like the most appropriate place to do the beta-eta-contraction

killed legacy "neg_clausify" and "clausify"

merged

factor out TPTP format output into file of its own, to facilitate further changes

merged

turn on "natural form" filtering in the Mirabelle tests, to see how it performs

missing "Unsynchronized" + make exception take a unit

added code to optionally perform fact filtering on the original (non-CNF) formulas

more cosmetics

cosmetics + prevent consideration of inlined Skolem terms in relevance filter

canonical argument order