removed duplicate type_solver (cf. Tools/typechk.ML);

simplified type attribute; removed rule/declaration (cf. thm.ML); removed obsolete theory/proof/generic/common; removed obsolete global/local/context_attribute(_i); added attribute(_i); renamed attribute to internal;

simplified type attribute; added rule/declaration_attribute (from drule.ML); added theory/proof_attributes; removed apply(s)_attributes;

simplified type attribute; moved rule/declaration_attribute to thm.ML;

rename map_theory/proof to theory/proof_map; added separate map_theory/proof;

tuned proofs;

simplified type attribute; tuned;

simplified type attribute;

type information is now also printed.

added some debugging code.

fixed a bug

quote "atom";

updated;

* ML/Isar: theory setup has type (theory -> theory);

use/use_thy: Output.toplevel_errors;

added basic syntax; removed pure syntax;

moved pure syntax to Syntax/syntax.ML and pure_thy.ML;

keep: disable Output.toplevel_errors; program: Output.ML_errors;

run_thy: removed Output.toplevel_errors;

added ML_errors;

use: Output.ML_errors;

Syntax.basic_syn;

setup: theory -> theory; added syntax (from Syntax/mixfix.ML); added HTML output syntax for _lambda;

tuned setmp;

setup: theory -> theory; use_output: Output.ML_errors;

tuned comments;

setup: theory -> theory; Syntax.appl(C)_syntax;

setup: theory -> theory;

Use generic Simplifier.simp_add attribute instead of Simplifier.simp_add_global.

Re-inserted consts_code declaration accidentally deleted during last commit.

strengthened some lemmas; simplified some proofs

substantial improvement in serialization handling

fixed one proof that broke because of the changes Markus did on the rules ex1I

substantial improvements in code generator

these hacks are no longer needed

improved SPASS support

case_result: drop_schematic, i.e. be permissive about illegal binds;

put_facts: do not pretend local thms were named;

declare the1_equality [elim?];

tuned;

tuned;

* Classical: optional weight for attributes; * HOL: prefer ex1I over ex_ex1I in single-step reasoning;

guess: used fixed inferred_type of vars;

export add_args; tuned;

attributes: optional weight; tuned;

classical attributes: optional weight;

prefer ex1I over ex_ex1I in single-step reasoning;

generic attributes;

tuned;

* ML/Isar: simplified treatment of user-level errors;

sane ERROR vs. TOPLEVEL_ERROR handling; added program;

added Isar.toplevel;

Output.error_msg;

removed special ERROR handling stuff (transform_error etc.); moved plain ERROR/error to library.ML; added toplevel_errors, exception TOPLEVEL_ERROR; error_msg, panic, info, debug no longer pervasive;

added exception ERROR, error, cat_error, sys_error, assert, deny, assert_all; added transform_failure; added prefix;

Output.debug;

generated code: raise Match instead of ERROR;

sane ERROR handling;

blacklist experiments

more readable divide ops

more practical time limit

*** empty log message ***

mixfix: added Structure;

uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag; mixfix: added Structure; renamed type exporter to export; removed obsolete sign_of; tuned signature; tuned;

uniform handling of fixes; mixfix: added Structure; tuned;

uniform handling of fixes;

uniform handling of fixes; mixfix: added Structure;

uniform handling of fixes; tuned;

tuned;

generic_setup: optional argument, defaults to Context.setup();

added map_theory, map_proof;

removed obsolete sign_of;

implicit setup, which admits exception_trace;

ProofContext.def_export;

updated to new induction principle

cahges to use the new induction-principle (now proved in full glory)

changes to make use of the new induction principle proved by Stefan horay (hooraayyy)

Implemented proof of (strong) induction rule.

Added theorem at_finite_select.

added lemmas perm_empty, perm_insert to do with permutations on sets

merged the silly lemmas into the eqvt proof of subtype

tuned proofs

tuned the eqvt-proof

rolled back the last addition since these lemmas were already in the simpset.

added the thms-collection "pt_id" (collection of all pt_<ak>1 lemmas)

tuned

tidied, and added missing thm divide_less_eq_1_neg

tidied, and giving theorems names

add transitivity rules

tuned;

updated;

tuned;

generic attributes;

* ML: generic context, data, attributes;

added context_of -- generic context;

generic attributes; tuned;

print rules: generic context;

Specification.pretty_consts ctxt;

generic data and attributes; tuned;

added rule, declaration; support generic attributes: theory, context, generic, common, generic_attribute(_i); added generic syntax; basic attributes now generic; tuned;

added generic syntax; mk_attribute: generic;

tuned dependencies;

added declaration_attribute;

support for generic contexts with data;

fix_tac: no warning;

generic attributes; added low-level modifiers from Pure/context_rules.ML;

Attrib.rule;

tuned

added the lemmas supp_char and supp_string

added some lemmas to the collection "abs_fresh" the lemmas are of the form finite (supp x) ==> (b # [a].x) = (b=a \/ b # x) previously only lemmas of the form (b # [a].x) = (b=a \/ b # x) with the type-constraint that x is finitely supported were included.

_E suffix for compatibility with AddIffs

tidied

simplified the special-case simprules

theorems need names

commented the transitivity and narrowing proof

Theory specifications --- with type-inference, but no internal polymorphism.

added infer_type, declared_type;

added param, spec, named_spec;

added init; tuned signature;

added 'axiomatization';