modernized structure XML_Syntax;

structure Thm_Deps;

modernized structure Proof_Node;

modernized structure Proof_Display;

modernized structure Proof_Syntax;

modernized structure Local_Syntax;

modernized structure AutoBind;

modernized structure Primitive_Defs;

modernized structure Simple_Syntax;

modernized structure Context_Position;

observe usual naming conventions;

find_theorems: respect conceal flag

DEEPEN: all tracing is subject to trace_DEEPEN (NB: Proof General tends to "popup" tracing output);

back to warning -- Proof General tends to "popup" tracing output;

split parsing of counterexamples from translation into terms (avoids Term.dummyT and ill-typed terms)

merged

predicate compiler creates code equations for predicates with full mode

renamed rpred to random

Rules that characterize functional/relational specifications.

adapted Item_Net; tuned;

allow multi-index; more scalable merge; renamed delete to remove, and insert to update (standard naming conventions); tuned;

added insert_safe, delete_safe variants;

tuned signature;

modernized structure Context_Rules;

modernized structure Rule_Cases;

merged

dedicated theory for loading numeral simprocs

set Pure theory name properly

tuned code setup

some notes on SPASS 3.0 distribution;

merged

combined former theories Divides and IntDiv to one theory Divides

tuned variable names of bindings; conceal predicate constants

dedicated theory for loading numeral simprocs

moved some div/mod lemmas to theory Divides

tuned proof

moved Commutative_Ring into session Decision_Procs

abstract over variables in reversed order (application uses given order)

disable printing of unparsed counterexamples for CVC3 and Yices

pattern are separated only by spaces (no comma)

back to polyml-svn -- performance impact is minimal, slowdown was caused by accumulated cruft of long-running Mac OS;

less verbose termination tactics

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