2006-01-19 ago wenzelm tuned comments;
2006-01-19 ago wenzelm setup: theory -> theory;
2006-01-19 ago wenzelm setup: theory -> theory;
2006-01-19 ago berghofe Use generic Simplifier.simp_add attribute instead
2006-01-19 ago berghofe Re-inserted consts_code declaration accidentally deleted
2006-01-19 ago paulson strengthened some lemmas; simplified some proofs
2006-01-18 ago haftmann substantial improvement in serialization handling
2006-01-18 ago urbanc fixed one proof that broke because of the changes
2006-01-17 ago haftmann substantial improvements in code generator
2006-01-17 ago paulson these hacks are no longer needed
2006-01-17 ago paulson improved SPASS support
2006-01-16 ago wenzelm case_result: drop_schematic, i.e. be permissive about illegal binds;
2006-01-16 ago wenzelm put_facts: do not pretend local thms were named;
2006-01-16 ago wenzelm declare the1_equality [elim?];
2006-01-15 ago wenzelm tuned;
2006-01-15 ago wenzelm tuned;
2006-01-15 ago wenzelm * Classical: optional weight for attributes;
2006-01-15 ago wenzelm guess: used fixed inferred_type of vars;
2006-01-15 ago wenzelm export add_args;
2006-01-15 ago wenzelm attributes: optional weight;
2006-01-15 ago wenzelm classical attributes: optional weight;
2006-01-15 ago wenzelm prefer ex1I over ex_ex1I in single-step reasoning;
2006-01-14 ago wenzelm generic attributes;
2006-01-14 ago wenzelm tuned;
2006-01-14 ago wenzelm * ML/Isar: simplified treatment of user-level errors;
2006-01-14 ago wenzelm sane ERROR vs. TOPLEVEL_ERROR handling;
2006-01-14 ago wenzelm added Isar.toplevel;
2006-01-14 ago wenzelm Output.error_msg;
2006-01-14 ago wenzelm removed special ERROR handling stuff (transform_error etc.);
2006-01-14 ago wenzelm added exception ERROR, error, cat_error, sys_error, assert, deny, assert_all;
2006-01-14 ago wenzelm Output.debug;
2006-01-14 ago wenzelm generated code: raise Match instead of ERROR;
2006-01-14 ago wenzelm sane ERROR handling;
2006-01-13 ago paulson blacklist experiments
2006-01-13 ago paulson more readable divide ops
2006-01-13 ago paulson more practical time limit
2006-01-13 ago nipkow *** empty log message ***
2006-01-13 ago wenzelm mixfix: added Structure;
2006-01-13 ago wenzelm uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
2006-01-13 ago wenzelm uniform handling of fixes;
2006-01-13 ago wenzelm uniform handling of fixes;
2006-01-13 ago wenzelm uniform handling of fixes;
2006-01-13 ago wenzelm uniform handling of fixes;
2006-01-13 ago wenzelm tuned;
2006-01-13 ago wenzelm generic_setup: optional argument, defaults to Context.setup();
2006-01-13 ago wenzelm added map_theory, map_proof;
2006-01-13 ago wenzelm removed obsolete sign_of;
2006-01-13 ago wenzelm implicit setup, which admits exception_trace;
2006-01-13 ago wenzelm ProofContext.def_export;
2006-01-11 ago urbanc updated to new induction principle
2006-01-11 ago urbanc cahges to use the new induction-principle (now proved in
2006-01-11 ago urbanc changes to make use of the new induction principle proved by
2006-01-11 ago berghofe Implemented proof of (strong) induction rule.
2006-01-11 ago berghofe Added theorem at_finite_select.
2006-01-11 ago urbanc added lemmas perm_empty, perm_insert to do with
2006-01-11 ago urbanc merged the silly lemmas into the eqvt proof of subtype
2006-01-11 ago urbanc tuned proofs
2006-01-11 ago urbanc tuned the eqvt-proof
2006-01-11 ago urbanc rolled back the last addition since these lemmas were already
2006-01-11 ago urbanc added the thms-collection "pt_id" (collection of all pt_<ak>1 lemmas)