Changed codes that call relevance filter.

Relevance filtering. Has replaced the previous version.

interrupt_timeout now raises Interrupt instead of SML90.Interrupt

smaller example to prevent timeout

Fixed bug in code generator for primitive definitions that caused dependencies to get mixed up.

Inductive sets with no introduction rules are now allowed as well.

added definition(_i);

renamed export to export_standard (again!), because it includes Drule.local_standard'; added abs_def (from locale.ML);

ProofContext.export_standard;

tuned atomize_cterm; added reverse_atomize_term/tac;

turned abstract_term into ProofContext.abs_def; ProofContext.export_standard;

added constant definition; tuned interfaces; tuned;

added 'definition'; 'spezification': optional fixes;

tuned comment;

export name_multi;

abs_def: improved error;

ObjectLogic.atomize_cterm;

updated;

works with DPLL solver now

the additional freshness-condition in the one-induction is not needed anywhere.

fixed code_generate syntax;

renamed axiomatize(_i) to axiomatization(_i); LocalTheory;

renamed inferred_type to inferred_param; added inferred_fixes;

ProofContext.inferred_param;

removed the_params;

added actual operations;

axiomatization: optional vars;

LocalTheory.pretty_consts;

tuned;

add_finals: prep_consts, i.e. varify type;

added dest_all;

TimeLimit replaced by interrupt_timeout

TimeLimit replaced by interrupt_timeout

Updated to Isabelle 2006-01-23

made change for ex1

removed problematic keyword 'atom'

more general serializer

slight steps forward

exported after_qed for axclass instance

ResClasimp.get_clasimp_lemmas now takes all subgoals rather than only the first

Clausification now handles some IFs in rewrite rules (if-split did not work)

bugfix: induct_tac no longer raises THM "dest_state"

fixed the <<= notation

replacement of bool by a datatype (making problems first-order). More lemma names

Fixed a bug.

no essential changes

made the change for setup-functions not returning functions anymore

a fixme comments about abs_fun_if, which should be called perm_if and moved to the "bool"-section

Local theory operations, with optional target locale.

added restore_body;

added the_params;

tuned order;

added Isar/local_theory.ML;

Ensure dereference is delayed.

tuned;

* ML: simplified type attribute;

simplified type attribute; removed obsolete tcset operations -- clean data/attribute/method setup;

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;