markup for formal entities, with "def" or "ref" occurrences;

handle Sorts.CLASS_ERROR instead of arbitrary exceptions;

reactivated isatest on macbroy6 -- 3h later to avoid overlap with backup daemon;

merged

turned off old quickcheck

pat_completeness gets its own file

ignore error messages produced by ATPs

merged

renamed f_inv_onto_f to f_inv_into_f (cf. 764547b68538)

restored accidentally deleted submultiset

multiset operations with canonical argument order

arg_types_of auxiliary function; using multiset operations

merged

close thm derivations explicitly

Fix a duplicate abbreviation || in etc/symbols.

made SML/NJ happy;

updated session name;

renamed f_inv_onto_f to f_inv_into_f (cf. 764547b68538);

merged

merged

merged

use plain Scan.repeat (NB: Scan.bulk is for cascading sources -- mostly interna use);

merged

explicit close_derivation

merged

map_range (and map_index) combinator

dropped Datatype.distinct_simproc

use Synchronized.assign to achieve actual immutable results;

support single-assigment variables -- based on magic RTS operations by David Matthews;

merged

fixed permissions -- this is a script, not an executable

inv_onto -> inv_into

renamed "nitpick_const_xxx" attributes to "nitpick_xxx" and "nitpick_ind_intros" to "nitpick_intros"

merged

fixed the "expect" mechanism of Refute in the face of timeouts

removed "nitpick_const_simp" attribute from Record's "simps"; Nitpick has its own notion of a record and doesn't need those.

merged

more accurate removal

merged

curried inter as canonical list operation (beware of argument order)

merged

proper handling of single literal case, added explicit exception, unfolding of distinct respects equal elements, made SML/NJ happy

Removed the hard-wired white list of theorems for sledgehammer

merged

Some new lemmas concerning sets

merged

curried union as canonical list operation

tuned ML import

removed old-style \ and \\ infixes

merged

dropped redundant gen_ prefix

replaced old_style infixes eq_set, subset, union, inter and variants by generic versions

find_theorems: better handling of abbreviations (by Timothy Bourke)

standardized basic operations on type option;

eliminated THENL -- use THEN RANGE; eliminated TRY' -- use TRY with op o; observe naming convention ctxt: Proof.context; tuned whitespace;

tuned;

fixed SML/NJ toplevel pp; tuned;

backpatching of structure Proof and ProofContext -- avoid odd aliases; renamed transfer_proof to raw_transfer; indicate firm naming conventions for theory, Proof.context, Context.generic;

tuned;

uniform use of Integer.min/max;

modernized session SET_Protocol;

modernized session Metis_Examples;

modernized session Isar_Examples;

tuned header;

more accurate dependencies for HOL-SMT, which is a session with image; misc cleanup;

removed unused map_force;

Removal of the unused atpset concept, the atp attribute and some related code.

additional schematic rules for Z3's rewrite rule

merged

added Hilbert_Choice section

merged

eliminated extraneous wrapping of public records, replaced simp_tac by best_tac (simplifier failed), less strict condition for rewrite (can also handle equations with single literal on left-hand side)

proper exceptions instead of unhandled partiality

footnote: inv via inv_onto

added inv_def for compatibility as a lemma

slightly less context-sensitive settings;

merged

corrected paths to certificates, added note how to re-generate the certificates

added proof reconstructon for Z3, added certificates for simpler re-checking of proofs (no need to invoke external solvers), added examples and certificates for all examples, removed Unsynchronized.ref (in smt_normalize.ML)

merged

merged

more accurate checkpoints

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;

aliases for Thomas Sewell;

modernized Balanced_Tree;

replaced meta_iffD2 by existing Drule.equal_elim_rule2; replaced SymSymTab by existing Symreltab; more antiquotations; eliminated old-style Library.foldl, Library.foldl_map; tuned;

tuned header;

Thomas Sewell, NICTA: more efficient HOL/record implementation;

tuned whitespace -- recover basic Isabelle conventions;

merged

Merge with isabelle dev changes.

Replace OldTerm.term_vars with Term.add_vars in named_cterm_instantiate.

Avoid a possible variable name conflict in instantiating a theorem. Instantiating a theorem variable with new variables created a possible variable name conflict if a record was defined with a field named 'f', 'x' etc. Using variable indices of 1 avoids the problem.

Fix unescaped expressions breaking latex output in Record.thy Expressions containing _ and ^ need to be adjusted or antiquoted in text comments for latex compatibility. This is in fact a little annoying, since it makes the comment less readable in both source and HTML form.

Merge record patch with updates from isabelle mainline.

Avoid record-inner constants in polymorphic definitions in Bali The Bali package needs to insert a record extension into a type class and define an associated polymorphic constant. There is no elegant way to do this. The existing approach was to insert every record extension into the type class, defining the polymorphic constant at each layer using inner operations created by the record package. Some of those operations have been removed. They can be replaced by use of record_name.extend if necessary, but we can also sidestep this altogether. The simpler approach here is to use defs(overloaded) once to provide a single definition for the composition of all the type constructors, which seems to be permitted. This gets us exactly the fact we need, with the cost that some types that were admitted to the type class have no definition for the constant at all.

Merge with changes from isabelle dev repository.

Initial response to feedback from Norbert, Makarius on record patch As Norbert recommended, the IsTuple.thy and istuple_support.ML files have been integrated into Record.thy and record.ML. I haven't merged the structures - record.ML now contains Record and IsTupleSupport. Some of the cosmetic changes Makarius requested have been made, including renaming variables with camel-case and run-together names and removing the tab character from the Author: line. Constants are defined with definition rather than constdefs. The split_ex_prf inner function has been cleaned up.

Branch merge for isabelle mainline updates.

Branch merge with updates from mainline isabelle.

Implement previous fix (don't duplicate ext_def) correctly.

There's no particular reason to duplicate the extension constant's definition under the name "ext_def", and it also prevents you having a field called ext.

Merged with mainline changes.

Adjust some documentation.

Simplification of various aspects of the IsTuple component of the new record package. Extensive documentation added in IsTuple.thy - it should now be possible to figure out what's going on from the sources supplied.

Record patch imported and working.

Initial attempt at porting record update to repository Isabelle.

Synchronized and Unsynchronized;

hide "ref" by default, to enforce excplicit indication as Unsynchronized;

explicit indication of Unsynchronized.ref;

open_unsynchronized for interactive Isar loop;

explicit indication of Unsynchronized.ref;

Raw ML references as unsynchronized state variables.

Dummy version of state variables -- plain refs for sequential access.

reactivated at-sml-dev-e;

misc tuning and modernization;

moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);

merged

less auxiliary functions

tuned

shared code between rep_datatype and datatype

further unification of datatype and rep_datatype

avoid compound fields in datatype info record

fold_body_thms: pass pthm identifier; fold_body_thms: dismiss path-etic attempt to check for cycles (cf. e24acd21e60e) -- could be masked by "seen"; fulfill_proof/thm_proof: check for thm cycles at the substitution point;

tuned internal source structure;

added fork_deps_pri;

merged

explicit pointless checkpoint

emerging common infrastructure for datatype and rep_datatype

streamlined rep_datatype further

simplified rep_datatype

more appropriate order of field in dt_info

re-established reasonable inner outline for module

merged

adjusted to changes in datatype package

merged

dropped dead code

registering split rules and projected induction rules; ML identifiers more close to Isar theorem names

fold_body_thms/join_bodies: explicitly check for cyclic theorem references;

tuned;

reachable: recovered reverse post-order (lost in 73ad4884441f), which is expected for all_preds/all_succs and required for topological_order;

merged

New lemmas involving the real numbers, especially limits and series

NEWS; corrected spelling

merged

simplified proof

removed potentially dangerous rules from pred_set_conv

explicitly hide empty, inter, union

merged

merged

merged

inf/sup_absorb are no default simp rules any longer

merged

merged

adapted proof

merged

tuned proofs

tuned header

added note on simp rules

merged

tuned proof; tuned headers

merged

tuned proofs; be more cautios wrt. default simp rules

merged

tuned proofs

merged

inter and union are mere abbreviations for inf and sup

merged

lemma relating fold1 and foldl; code_unfold rules for Inf_fin, Sup_fin, Min, Max, Inf, Sup

subsumed by more general setup in List.thy

idempotency case for fold1

added dual for complete lattice

merged

record how many "proof"s are solved by s/h

added quotes for filenames; truncated remaining time (no floats supported by ulimit)

merged; adopted to changes from Code_Evaluation in the predicate compiler

replaced sorry by oops; removed old debug functions in predicate compiler

added first version of quickcheck based on the predicate compiler; added a few quickcheck examples

adapted configuration for DatatypeCase.make_case

added a new example for the predicate compiler

added context free grammar example; removed dead code; adapted to work without quick and dirty mode; fixed typo

added first prototype of the extended predicate compiler

moved predicate compiler to Tools

removed generation of strange tuple modes in predicate compiler

extending predicate compiler and proof procedure to support tuples; testing predicate wirh HOL-MicroJava semantics

modified predicate compiler further to support tuples

changed preprocessing due to problems with LightweightJava; added transfer of thereoms; changed the type of mode to support tuples in the predicate compiler

handling of definitions

experimenting to add some useful interface for definitions

added predicate compile preprocessing structure for definitional thms -- probably is replaced by hooking the theorem command differently

modified handling of side conditions in proof procedure of predicate compiler

merged

Code_Eval(uation)

merged

Added "nitpick_const_simp" tags to lazy list theories. (Will be useful once Nitpick is integrated in Isabelle.)

atbroy101 is long dead, use atbroy99; comment out broken SML test invocation

merged

stripped legacy ML bindings

Undo errornous commit of Statespace change

correct variable order in approximate-method

merged

Correct chasing of type variable instantiations during type unification. The following theory should not raise exception TERM: constdefs somepredicate :: "(('b => 'b) => ('a => 'a)) => 'a => 'b => bool" "somepredicate upd v x == True" lemma somepredicate_idI: "somepredicate id (f v) v" by (simp add: somepredicate_def) lemma somepredicate_triv: "somepredicate upd v x ==> somepredicate upd v x" by assumption lemmas somepredicate_triv [OF somepredicate_idI] lemmas st' = somepredicate_triv[where v="h :: nat => bool"] lemmas st2 = st'[OF somepredicate_idI]

hide newly introduced constants

used standard fold function and type aliases

sos method generates and uses proof certificates

full reserve of worker threads -- for improved CPU utilization;

merged

be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer

tail -n 20: more helpful output if make fails

corrected order of type variables in code equations; more precise certificate for cases

merged

tuned some proofs

merged

added session theory for Bali and Nominal_Examples

added session theory for Nominal_Examples

added session theory for Bali

adjusted to new Number Theory scenario

added session entry point theories

common base for protocols with symmetric keys

tuned header

isarified proof

fixed permissions -- this is a script, not an executable;

tuned;

deleted unused file

merged

entry point theory for examples; reactivated half-dead example

merged

corrected remote SMT solver invocation

theory entry point for session Hoare_Parallel (now also with proper underscore)

merged

tuned author

added new method "smt": an oracle-based connection to external SMT solvers

tuned tracing;

scheduler backdoor: 9999 means 1 worker;

Hilbert_Classical: more precise control of parallel_proofs;

actually observe Multithreading.enabled (cf. d302f1c9e356);

merged

restructured code

merged

rewrite premises in tactical proof also with inf_fun_eq and inf_bool_eq: attempt to allow user to use inf [=>] and inf [bool] in his specs

modified minimization log