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;

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';

Specification.pretty_consts;

gen_names: preserve empty names;

added Isar/specification.ML;

updated;

another change for the new induct-method

RuleCases.make_nested;

support nested cases; tuned apply_case;

support nested cases; added apply_case; replaced make/simple by make_common/nested/simple;

RuleCases.make_common;

pretty_locale: backquote notes;

RuleCases.make_simple;

tuned order;

added backquote;

RuleCases.make_common/nested;

* Provers/induct: improved simultaneous goals -- nested cases;

added private datatype nprod (copy of prod) to be used in the induction rule

changed PRO_RED proof to conform with the new induction rules

prep_meta_eq: reuse mk_rews of local simpset; adapted ML code to common conventions; tuned;

removed obsolete eqrule_HOL_data.ML;

removed obsolete eqrule_FOL_data.ML;

simplified EqSubst setup;

obsolete, reuse mk_rews of local simpset;

Toplevel.theory_to_proof;

transactions now always see quasi-functional intermediate checkpoint; removed obsolete theory_theory_to_proof; added

tuned EqSubst setup;

Pure/Isar: Toplevel.theory_to_proof admits transactions that modify the theory;

hide type datatype node; added theory_node, proof_node, is_theory, is_proof, proof_position_of, checkpoint, copy; no_body_context: no history; transaction: test save = true;

tuned print_theorems_theory;

Toplevel.proof_position_of;

store_thm: transfer to current context, i.e. the target theory;

replaced swap by contrapos_np;

added setminus; tuned;

proper handling of simultaneous goals and mutual rules;

provide projections of induct_weak, induct_unsafe;

added strict_mutual_rule;

RuleCases.strict_mutual_rule; export internalize;

changed the name of the type "nOption" to "noption".

added "fresh_singleton" lemma

added more documentation; will now try out a modification of the ok-predicate

Reversed Larry's option/iff change.

substantial additions using locales

exported read|cert_arity interfaces

trace_simp_depth_limit is 1 by default

removed pointless trace msg.

preservation of names

a few more named lemmas

fix: reintroduced pred_ctxt in gen_add_locale

tuned;

* Pure/Isar: Toplevel.theory_theory_to_proof;

added unlocalize_mfix;

added unlocalize_mixfix;

added theory_to_theory_to_proof, which may change theory before entering the proof; added forget_proof (from isar_thy.ML);

tuned;

moved forget_proof to toplevel.ML;

Toplevel.forget_proof;

adapted Toplevel.Proof;

removed dead code;

more stuff;

Provers/classical: stricter checks to ensure that supplied intro, dest and elim rules are well-formed

added explicit paths to required theories

added implementation manual;

more stuff;

fixed LaTeX source;

class now a keyword

class now an keyword, quoted where necessary

add_local_context now yields imported and body elements seperatly; additional slight clenup in code

rearranged burrow_split to fold_burrow to allow composition with fold_map

added unfolding(_i); renamed using_thmss(_i) to using_i;

unparse String/AltString: escape quotes;

tuned;

avoid hardwired Trueprop; local proof: static refererence to Pure.thy;

added 'using' command;

updated;

added IsarImplementation;

updated -- lost update!?

* Pure/Isar: new command 'unfolding'; * ML/Provers: more generic wrt. syntax of object-logics; tuned;

ISABELLE_USER for remote cvs access;

outline;

"The Isabelle/Isar Implementation" manual;

* Provers/classical: removed obsolete classical version of elim_format;

tuned forall_intr_vars;

added classical_rule, which replaces Data.make_elim; removed obsolete Data.make_elim and classical elim_format attribute; tuned;

explicitly reject consts *Goal*, *False*;

elim rules: Classical.classical_rule;

removed obsolete cla_dist_concl;

removed classical elim_format;

removed obsolete Provers/make_elim.ML;

obsolete, see classical_rule in Provers/classical.ML;

more robust phantomsection;

require cla_dist_concl, avoid assumptions about concrete syntax;

avoid implicit assumptions about consts Not, op =, *Goal*, *False*;

provide equality_name, not_name;

fixed final_consts;

provide cla_dist_concl;

non-PDF: phantomsection;

added atom keyword

changes in code generator keywords

adaptions to changes in code generator

slight improvements

slightly improved serialization

substantial improvements in code generating

added map_index