tuned error msg: rows counted from 1;

tidied

tidied

function "remove" and new lemmas for Factorization

new theory ex/Factorization

new lemmas

added simple_args; added 'tactic' method;

argument: include verbatim;

moved use_mltext, use_mltext_theory, use_let, use_setup to context.ML;

added use_mltext, use_mltext_theory, use_let, use_setup (from isar_thy.ML);

rsyncd setup; --delete mode (beware!);

switched to mirroring with rsync server

new Poly/ML setup made default;

induct: "stripped" option;

require NatDef;

REPEAT_ALL_NEW;

added REPEAT_ALL_NEW;

tidied

tidied

new theories UNITY/Detects, UNITY/Reachability

added con_elim_s(olved_)tac; added 'simplified' flag;

mk_cases / inductive_cases: use InductMethod.con_elim_(solved_)tac;

added multi_resolveq, resolveq_tac;

Added Tanja's Detects and Reachability theories. Also changed object-quantifiers to meta-quantifiers in ball_constrains_UN/INT...

improved reasoning about {} and UNIV

join_rules: compatibility check;

token_trans: symbol length;

join induct rules;

added 'prolog' method;

added freeze_all; tuned spacing;

polished version of the Allocator using Rename

tidied the proofs of singleton_insert_inj_eq, singleton_insert_inj_eq' and installed them by AddIffs, since they are an important special case of equalityE.

project induct rule;

tuned;

test setup;

proper setup;

tuned;

expandshort

added a reference

new theorems from Sidi Ould Ehmety

tuned;

add_cases_induct: project_rules accomodates mutual induction;

tuned msgs;

even Alloc works again, using "rename"

replaced UN_constant, INT_constant by unconditional versions that rewrite to if-then-else expressions

add_cases_induct: accomodate no_elim and no_ind flags;

new mostly working version; Alloc nearly converted to "Rename"

new thm vimage_Collect_eq

more bijection theorems

cases/induct attributes; use NetRules for storage; tuned rule selection; tuned concrete syntax;

add_cases_induct: induct_method setup; removed cases_of, all_cases, all_inducts;

HOLogic.dest_conj; add_cases_induct: induct_method setup;

HOLogic.dest_conj;

even better induct setup;

early setup of induct_method;

added dest_conj;

theorems [trans] = rev_mp mp;

use NetRules;

added major_prem_of;

added Isar/net_rules.ML;

simplified induct method;

tuned;

induct method: implicit rule;

rN = "record";

all_cases / all_inducts;

workaround res_inst_tac/lift_inst_rule bug by explicit type contraint;

capply, cabs: Sign.nodup_vars;

nodup_vars: fixed omission of 2 minor cases; account for Frees as well;

tuned generated TeX code;

renamed a lemma

Added and renamed a lemma.

not working yet. partial conversion to use "rename" instead of "extend"

new theorems inj_iff, surj_iff

new reference korf85

* Pure now provides its own version of intro/elim/dest attributes; useful for building new logics, but beware of confusion with the Provers/classical ones! * HOL: removed "case_split" thm binding, should use "cases" proof method anyway; * tuned syntax of "induct" method; * new "cases" method for propositions, inductive sets and types; * HOL/records: admit "r" as field name;

tuned syntax wrapper;

tuned "induct" syntax;

"cases" method;

added cases_tac;

induct: tuned syntax; added cases method;

added cases_of, cases;

removed case_split thm binding;

added boolN;

proper variant names (admit field "r");

three easy new examples

tuned footnote;

HOL/record: fixed select-update simplification procedure to handle extended records as well;

var: skolem;

remove *.out;

renamed Univalent to univalent

simplified some proofs

new examples that cannot be done in LEO

A few lemmas and some Adds.

Added global let-simplification rule.

Commenst.

added instance declaration for finite product