changed importing introduction rules to fix the same type variables in all introduction rules; improved mode analysis for partially applied relations; added test case; tuned

changed proof method to handle widen predicate in JinjaThreads

added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex

processing of tuples in introduction rules

added a few tricky examples with tuples; added alternative introduction rules for some constants; corrected mode analysis with negation; improved fetching of definitions

developing an executable the operator

generalizing singleton with a default value

changed elimination preprocessing due to an error with a JinjaThread predicate

added test for higher-order function inductification; added debug messages

added filtering of case constants in the definition retrieval of the predicate compiler

extended core of predicate compiler to expand tuples in introduction rules

added tupled versions of examples for the predicate compiler

moved meta_fun_cong lemma into ML-file; tuned

merged

adapted Function_Lib (cf. b8cdd3d73022);

configuration flag "partials"

renamed auto_term.ML -> relation.ML

function package: more standard names for structures and files

renamed FundefDatatype -> Function_Fun

maintain position of formal entities via name space;

maintain explicit name space kind; export Name_Space.the_entry; tuned messages;

renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;

eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already; simplified messages;

eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already; fully authentic merge;

eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;

maintain abstract entry, with position, identity etc.; declare/define: explicit indication of strictness; merge_tables/join_tables: disallow duplicates based on entry identity;

tuned message;

import theory Nat here, which avoids duplicate definition of datatype_realizers (and thus allows to maintain fully authentic fact table);

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