merged

printing combinator for hierarchical programs

merged

add lemma cont2cont_Let_simple

add lemma cont2cont_split_simple

add List_Cpo.thy to HOLCF/Library

dropped names from serializer interface

added more explicit warning

ML_Context.ml_store_thm(s): operate on thread context instead of Unsynchronized.ref;

use setmp_noncritical for PGIP, which is presumably sequential (PG clone);

use setmp_noncritical for sequential Pure bootstrap;

turned show_brackets into proper configuration option; Sign.certify/type_check: dropped Syntax.pp_show_brackets, which is hard to hold up due to Pretty.pp and not even present in the regular end-user type check;

Syntax.standard_parse_term: eliminated redundant Pretty.pp;

structure Syntax: define "interfaces" before actual implementations;

turned show_sorts/show_types into proper configuration options;

pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;

refined treatment of multi-line subexpressions;

basic support for subexpression highlighting (see also gatchan.jedit.hyperlinks.HyperlinkManager/HyperlinkTextAreaPainter);

updated configuration options;

recovered options for goal antiquotations from f45d332a90e3: actually pass context to Proof.pretty_goals (see also 45facd8f358e);

turned eta_contract into proper configuration option;

turned show_structs into proper configuration option;

configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;

pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;

tuned comment;

merged

merged

QND_FLAG is a shell variable, not a string

modernized session ROOT;

disposed left-over user preferences;

turned show_all_types into proper configuration option;

treat show_free_types as plain ML option, without the extras of global default and registration in the attribute name space -- NB: 'print_configs' only shows the latter;

more explicit Config.declare vs. Config.declare_global;

turned show_no_free_types into proper configuration option show_free_types, with flipped polarity;

remove code I submitted accidentally

merged

disable "definitional CNF"; it has a bad impact on "Metis_Examples". Perhaps we should use it more selectively, based on how many clauses we would get using the naive method

redisable Nitpick from Cygwin, until I've investigated the issue

show the number of facts for each prover in "verbose" mode

fix bug in "debug" mode

make sure "Unknown ATP" errors reach the users -- i.e. don't generate them from a thread

If Geoff puts some important message in his TPTP problems (e.g., money requests), we should show them to the user

fix trivial "x = x" fact detection

merged

merged

merged

hand out deresolver from serializer invocation

Revert bij_betw changes to simp set (Problem in afp/Ordinals_and_Cardinals)

merged

Updated proofs in Dining Cryptographers theory

Corrected definition and hence removed sorry.

Moved lemmas to appropriate locations

merged

merged

measure unique

merge

move lemmas to correct theory files

factorizable measurable functions

Introduced sigma algebra generated by function preimages.

vimage of measurable function is a measure space

Measurable on product space is equiv. to measurable components

Measurable on euclidean space is equiv. to measurable components

preimages of open sets over continuous function are open

added definition of conditional expectation

proved existence of conditional expectation

introduced integration on subalgebras

changed definition of dynkin; replaces proofs by metis calles

dynkin

dynkin system

merged

Fixes lemma names

NEWS

Introduce surj_on and replace surj and bij by abbreviations.

Permutation implies bij function

bij <--> bij_betw

Add filter_remove1

Add lessThan_Suc_eq_insert_0

merged

updated

set printmode while marking

updated

avoid reference to theory Ferrack altogether

more canonical theory setup

set depth to 1

avoid theory Imperative_HOL altogether

adapted to change eq -> equal

corrected printmode handling

swapped slip

updated

restored and added surpression of case combinators

dropped superfluous presentation names

manage statement selection for presentation wholly through markup

formal markup of generated code for statements

removed namespace stuff from code_printer

merged

reenable Nitpick on Cygwin; we'll see tomorrow if there's still a failure, and if so I'll investigate

merged;

Proof.pretty_state: print everything in the foreground context to give users a chance to configure options, e.g. via "using [[show_consts]]";

turned show_consts into proper configuration option;

prefer regular Proof.context over background theory; misc tuning and simplification;

just one refute.ML;

use existing Integer.pow, despite its slightly odd argument order;

tuned whitespace and indentation, emphasizing the logical structure of this long text;

inner parsing: refrain from too many nested position reports to achieve more precise error feedback in the source;

Document_View: squiggly underline for messages; tuned;

added gfx_range convenience;

Isar_Document.reported_positions: more precise include/exclude, include root as last resort only;

Position.Range: exclude singularity (again);

merged

merged

FIXME -> TODO (nothing is broken)

Let MESON take an additional "preskolemization tactic", which can be used to put the goal in definitional CNF

use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd; this *really* speeds up things -- HOL now builds 12% faster on my machine

make definitional CNF translation code more robust in the presence of existential quantifiers in the "literals"

formal framework for presentation of selected statements

merged

Table.map replaces Table.map'

dropped dead code; tuned

include names need not be considered as reserved any longer

skip empty name bunches; fill up trailing positions with NONEs

use code_namespace module for SML and OCaml code

Table.map replaces Table.map'

avoid cyclic modules

merged

simultaneous modification of statements: statement names

simultaneous modification of statements

explicit modify_stmt parameter

Graph.map, in analogy to Table.map

replaced Table.map' by Table.map

merged

tuned

generalized hierarchical data structure over statements

merged

normalization is allowed to solve True

merged

merged

cosmetics

SNARK doesn't like facts

show real CPU time

factor out code shared by all ATPs so that it's run only once

handle all whitespace, not just ASCII 32

speed up SPASS hack + output time information in "blocking" mode

remove time information in output, since it's confusing anyway

minor refactoring

translate the axioms to FOF once and for all ATPs

run relevance filter in a thread, to avoid blocking

add dependency of "spass" script

more elegant ML

only kill ATP threads in nonblocking mode

lower number of facts given to SInE

share the relevance filter among the provers

got rid of the "theory_relevant" option; instead, have fudge factors that behave more smoothly for all provers

generalize theorem argument parsing syntax

support new option in Mirabelle

fiddled with fudge factor (based on Mirabelle)

give priority to assumptions in structured proofs

introduce fudge factors to deal with "theory const"

rename sledgehammer config attributes

finish moving file

move file

finished renaming

fix typo

shorten a few file names

added "expect" feature of Nitpick to Sledgehammer, for regression testing

update docs

update docs

added "blocking" option to Sledgehammer to run in synchronous mode; sometimes useful, e.g. for testing

normalization fails on unchanged goal

turned show_question_marks into proper configuration option; show_question_marks only affects regular type/term pretty printing, not raw Term.string_of_vname; tuned;

prefer regular print functions over slightly low-level Term.string_of_vname;

eliminated obsolete old-style goal stack package, which was considered the main Isabelle user interface at some point;

eliminated really ancient OldGoals operations in favour of Goal.prove_internal (with its minimal checks and without normalization of result); tuned white space; tuned indentation;

Document.State.Assignment: eliminated promise in favour of plain values -- signalling is done via event bus in Session;

actually declare "_constrainAbs" as @{syntax_const};

merged

repaired attribute code_unfold_post which has ever been broken

tuned text segment

merged

factored out generic part of Scala serializer into code_namespace.ML

merged

do not print object frame around Scala includes -- this is in the responsibility of the user

repaired codegen tool

tuned internally and made smlnj happy

merged

renewing specifications in HOL-Auth

adapting and tuning example theories

adding further example for quickcheck with prolog code generation

handling the quickcheck result no counterexample more correctly

adding manual reordering of premises to prolog generation

towards support of limited predicates for mutually recursive predicates

improving clash-free naming of variables and preds in code_prolog

exporting mode analysis for use in prolog generation

renaming

improving naming of predicates in code_prolog; changing order of flattened premises once again

changing order of premises generated when flattening functions in premises; adapting example for second attack for hotel key card system

added further hotel key card attack in example file

avoiding warning for a duplicate rewrite rule in preprocessing of the predicate compiler

using Cache_IO interface for a safe parallel prolog execution

storing options for prolog code generation in the theory

adapting example files to latest changes

adding Lambda example theory; tuned

added quite adhoc logic program transformations limited_predicates and replacements of predicates

distinguish between "by" and "apply"

merged

fiddling with "try"

updated

"try" -- a new diagnosis tool that tries to apply several methods in parallel

add one option to Mirabelle

update docs

add a penalty for being higher-order

improve weighting of irrelevant constants, based on Mirabelle experiments

take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter

repaired casual accident; tuned names

corrected misbehaved additional qualification of generated names

merged

avoid strange special treatment of empty module names

allow explicit parameter for code width

evaluate takes ml context and ml expression parameter

modernized; avoid pointless tinkering with structure names

distinguish code production and code presentation

dropped single_module parameter

tuned

record argument for serializers

tuned serializer argument interface

removed serializer interface redundancies

more coherent naming of syntax data structures

Code_Printer.tuplify

dropped legacy interfaces

more permissive: simplification solves the goal when rhs = undefined

merged

tuned

tuned

tuned

tuned

tuned file interface

tuned

eliminated some obscure higher-order arguments

trailing newline by default

width is a formal parameter of serialization

whitespace tuning

tuned comment

merged

fiddle with fact filter

adjust Mirabelle

rule out low-level class facts

make Sledgehammer's relevance filter somewhat slacker

move imperative code to where it belongs

fiddle with fact filter based on Mirabelle experiments

allow configuration of fact filter fudge factors

made all fudge factors in relevance filter references, so that Mirabelle can set them (for experiments)

execute actions in same order as specified on command line

show index in fact list of all found facts

allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID

deal with duplicates

improve new "sledgehammer_filter" action

remove useless var

added evaluation method for relevance filter

remove needless parameter

bring Sledgehammer's combinators in line with Metis's; cf. email from Larry

fiddle with the relevance filter

moved Toplevel.run_command to Pure/PIDE/document.ML; eliminated aliases of exception Toplevel.TERMINATE and Toplevel.EXCURSION_FAIL; tuned signatures;

Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body; Position.Id_Range convenience;

tuned;

Node.full_index: allow command spans larger than block_size;

Document_View: repaint overview for any command change of this node (again);

refined proper_line_range (again), to make text_area_extension work with soft wwrap; NB: text_area.offsetToXY returns null for "invisible" positions;

Document state assignment indicates command change;

tuned commands_changed_actor: more precise/efficient handling of visible screen lines;

simplified/clarified Document_View.text_area_extension; tuned Document.Node.block_size, trading some space for better time;

Document.Node: significant speedup of command_range etc. via lazy full_index;

text_edits/recover_spans: reparse at least until line boundary -- increases chance of recovery for bad ML text, for example;

Command.newlines: account for physical newlines;

Toplevel.run_command: more careful treatment of interrupts stemming from nested multi-exceptions etc.; simplified Toplevel.error_msg;

tuned messages: discontinued spurious full-stops (messages are occasionally composed unexpectedly);

more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;

tuned;

Command.results: ordered by serial number;

message serial number indicates physical order;

tuned;

tuned;

merged

what is hidden is hidden

hide all-too-popular constant name eq

merged

formerly unnamed infix equality now named HOL.eq

code checking: compiler invocation happens in same directory as generated file -- avoid problem with different path representations on cygwin

Quotient Package: dont unfold mem_def, use rsp and prs instead

Quotient Package: added respectfulness and preservation lemmas for mem.

quotient package: added a list of pre-simplification rules for Ball, Bex and mem

quotient package: lemmas to be lifted and descended can be pre-simplified

merged

renamed class/constant eq to equal; tuned some instantiations

improved deresolving of implicits

Document_View.text_area_extension: do not insist in crashing if (weak) assertion is violated;

Isabelle/jEdit property for global tooltip dismiss delay;

External_Hyperlink: proper error dialog;

Document_Mode.Line_Context: proper semantic equality/hash code avoids memory leak due to interning in org.gjt.sp.jedit.syntax.TokenMarker;

JEDIT_JAVA_OPTIONS: actors.enableForkJoin=false is supposed to enable ResizableThreadPoolScheduler, to avoid starvation of excessive amounts of future tasks etc.;

session_actor: ignore spurious TIMEOUT (again) -- probably stemming from earlier use of receiveWithin;

session_actor: await state assigment of previous change before signalling current change, and avoid crash in overrun situations;

use Future.get_finished where this is the intended meaning -- prefer immediate crash over deadlock due to promises that are never fulfilled; clarified session signalling;

Swing_Thread.now: volatile result to make double-sure;

Document_Model.token_marker: misc tuning and simplification;

added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.; Markup_Tree.select: plain Iterator; misc tuning and simplification;

XML.Cache: intern property keys once and for all (again);

more careful locking of jEdit buffer;

avoid application crash due to wrong requirement -- result is joined, but change not necessarily finished due to extra map;

include Document.History in Document.State -- just one universal session state maintained by main actor; Session.command_change_buffer: thread actor ensures asynchronous dispatch; misc tuning;

volatile variables (in Scala);

non-critical output primitives -- depending on thread-safe TextIO, while races wrt. flushing should not matter;

modernized specifications;

discontinued separate Pure-ProofGeneral keywords session -- protocol commands are already defined in Pure;

discontinued broken no_warnings_CRITICAL -- global output channels must not be changed after startup initialization;

eliminated broken Output.no_warnings_CRITICAL -- context visibility does the job; modernized attribute setup;

more careful treatment of context visibility flag wrt. spurious warnings; misc tuning;

eliminated obsolete Output.no_warnings, where no warnings were produced anyway;

eliminated broken Output.no_warnings_CRITICAL -- context visibility does the job;

more careful treatment of context visibility flag wrt. spurious warnings;

merged

merged

turn off experimental feature per default + avoid exception on "theory constant"

extended relevance filter with first-order term matching

drop chained facts

rename and simplify

cosmetics

renaming + treat "TFree" better in "pattern_for_type"

fix threshold computation + remove "op =" from relevant constants

avoid needless "that" fact

add nameless chained facts to the pool of things known to Sledgehammer

if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem

improve SPASS hack, when a clause comes from several facts

fix Vampire version numbers

lower penalty for Skolem constants

merged

official support for Scala

updated generated files

tuned whitespace

more xsymbols

re-added accidental omission

proper namespace administration for hierarchical modules

more antiquotations;

eliminated Unsynchronized.ref in favour of configuration option; proper naming of thy: theory vs. ctxt: Proof.context; recovered some Isabelle/ML indendation style;

more appropriate name for configuration option "meson_max_clauses" (cf. output of 'pront_configs');

Sum_Of_Squares: proper configuration options;

tuned printed type names, according to ML;

eliminated unnecessary ref;

clarified iter_deepen_limit vs meson (cf. 7c5896919eb8) -- eliminated global ref;

disposed some old debugging tools;

proper configuration option "show_proofs"; modernized syntax translation;

structure Unsynchronized is never opened and set/reset/toggle have been discontinued; retain Unsynchronized.change alias for Proof General;

expanded some aliases from structure Unsynchronized;

merged, resolving some minor conflicts in src/HOL/Tools/Predicate_Compile/code_prolog.ML;

merged

formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj

tuned fact reference

merged

added support for yet another prolog system (yap); generate has only one option ensure_groundness; added one example of yap invocation in example theory

adapted examples; tuned

moving options; tuned

added generation of predicates for size-limited enumeration of values

NEWS

merged

formerly unnamed infix impliciation now named HOL.implies

merged

proper passing of optional module name

For sublocale it is sufficient to reconsider ancestors of the target.

only print qualified implicits

merged

stub for (later) correct deresolving of class method names

tuned serializer interface

private version of commas, cf. printmode

merged

merged

re-added accidental omission

tuned includes

prevent line breaks after Scala symbolic operators

corrected semantics of presentation_stmt_names; do not print includes on presentation selection

code_include Scala: qualify module nmae

merged

preliminary implementation of hierarchical module name space

tuned

proper context for various Thy_Output options, via official configuration options in ML and Isar;

Thy_Output: options based on proper context, although Thy_Output.add_wrapper still allows to maintain old-style wrapper combinators (setmp_CRITICAL etc.);

eliminated old 'local' command;