less verbose inductive invocation

tuned

absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned

merged

recovered from 7a1f597f454e, simplified imports;

merged

merged

adjusted to changes in theory Divides

moved some lemmas to theory Int

moved some dvd [int] facts to Int

moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly

eliminated some old folds;

eliminated some old folds;

eliminated some old folds;

less aggressive tracing;

DEEPEN: less aggressive tracing, subject to trace_DEEPEN;

merged

merged

removing ancient predicate compiler files

merged

encapsulating records with datatype constructors and adding type annotations to make SML/NJ happy

improved mode parser; added mode annotations to examples

moved datatype mode and string functions to the auxillary structure

improving mode parsing in the predicate compiler

improved handling of alternative rules; added test cases for alternative rules; normalized tracing in the predicate compiler

merged

Tidied up some very ugly proofs

small fixes

merged

join entries properly on theory merge

moved some dvd [int] facts to Int

moved algebraic classes to Ring_and_Field

moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly

standardized filter/filter_out;

modernized some structure names;

eliminated obsolete/unused Thm.kind_internal/is_internal etc.;

modernized functor/structures Interpretation;

tuned whitespace;

unregister: eliminated unused status;

proper header;

proper header; tuned whitespace;

proper header; adapted ResBlacklist -- eliminated inefficient hash table; eliminated some old folds;

separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;

Named_Thms is not scalable;

replaced slightly odd Thm.is_internal by Facts.is_concealed -- as provided by the name space; tuned;

tuned;

tuned proof;

separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;

removed unused file;

less hermetic ML; parse_pattern: apply Consts.intern only once (Why is this done anyway?); modernized structure names;

removed slightly exotic symbol abbreviations for now -- achieves a coherent (unique) mapping; (NB: in principle symbol abbreviations could well be ambigous);

simplified method syntax of "smt", full normalization of binders, corrected translation of patterns into intermediate format, ignore empty lines in Z3 output

merged

adjusted import to changed HOL theory graph

moved theory Divides after theory Nat_Numeral; tuned some proof texts

proper nested quotes; give up unposixly < <(...) for now -- it needs to be exportable through the global environment (e.g. via make or sh);

components: ensure that the last line is read, even if it lacks EOL;

updated Isar.goal;

renamed raw Proof.get_goal to Proof.raw_goal;

back to Proof.raw_goal;

renamed Proof.flat_goal to Proof.simple_goal;

Isar.goal: Proof.simple_goal, not raw version;

replaced slightly odd get_goal/flat_goal by explicit goal views that correspond to the usual method categories;

provide SpecParse.constdecl/constdef, e.g. for quotient_definition;

slightly more robust error message;

tuned;

merged

merged

misc tuning;

let naming transform binding beforehand -- covering only the "conceal" flag for now; export LocalTheory.standard_morphism;

tuned;

simplified default binding; conceal internal bindings;

conceal internal bindings;

Drule.store: proper binding; conceal internal bindings;

added restore_naming;

load Product_Type before Nat; dropped junk

moved lemmas for dvd on nat to theories Nat and Power

Probability tweaks

merged

New theory Probability, which contains a development of measure theory

merged

New theory SupInf of the supremum and infimum operators for sets of reals.

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

tuned initial session setup;

merged

proper headers;

reactivated sun-poly, as parallel test;

merged

merged

merged

merged

merged

disabled test case for predicate compiler due to an problem in the inductive package

added examples for quickcheck prototype

adding a prototype of a counter-example generator based on the predicate compiler to HOL/ex

adding test case for inlining of predicate compiler

hiding randompred definitions

changes to example file

print retrieved specification when printing intermediate results

added option show_modes to predicate compiler

including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck

removed unused file smt_builtin.ML, made negative pattern polymorphic (similar to positve pattern)

included description for sledgehammer options in Mirabelle script

measure runtime of ATPs only if requested

eliminated some old folds;

eliminated some old folds;

Datatype.read_typ: standard argument order; eliminated some old folds;

normalized basic type abbreviations;

misc tuning and simplification;

merged

merged

merged

merged

tuned

tuned

dropped obsolete comment

added implode and explode

added friendly error message when Kodkodi is not available

internal renaming in Nitpick and fixed Kodkodi invokation on Linux; renamed Nitpick's ML structures from NitpickXxx to Nitpick_Xxx and added KODKODI_JAVA_LIBRARY_PATH to LD_LIBRARY_PATH before invoking Kodkodi

merged