2000-06-29 wenzelm 2000-06-29 have_thmss: handle multiple lists of arguments;
2000-06-29 paulson 2000-06-29 now freezes Vars in order to prevent errors in cases like these: Goal "Suc (x + i + j) + ?q ?ii ?jj + k + x = xxx"; Goal "Suc (x + i + j) = x + f(?q i j) + k"; Goal "Suc (x + i + j) = x + ?q i j + k"; Goal "Suc (?q ?ii ?jj + i + j) + ?rq ?ii ?jj + k + ?q ?ii ?jj = xxx";
2000-06-29 paulson 2000-06-29 tidied proofs using default rule equalityCE
2000-06-29 paulson 2000-06-29 the default equalityCE simplifies proofs
2000-06-29 paulson 2000-06-29 tidied
2000-06-29 paulson 2000-06-29 fixed proof to cope with the default of equalityCE instead of equalityE
2000-06-29 paulson 2000-06-29 now uses equalityCE, which usually is more efficent than equalityE
2000-06-29 paulson 2000-06-29 weak elimination rules
2000-06-28 wenzelm 2000-06-28 classical 'elimify' attribute;
2000-06-28 kleing 2000-06-28 tuned for ProofGeneral 3.2
2000-06-28 kleing 2000-06-28 tuning, eliminated rev_surj
2000-06-28 paulson 2000-06-28 fixed some weak elim rules, and tidied
2000-06-28 paulson 2000-06-28 tidying and unbatchifying
2000-06-28 paulson 2000-06-28 no longer depends upon a prior "open Ind_Syntax" from elsewhere
2000-06-28 paulson 2000-06-28 fixed some weak elim rules, and tidied
2000-06-28 paulson 2000-06-28 fixed some weak elim rules
2000-06-28 paulson 2000-06-28 simplified slightly by using dependencies better in theories
2000-06-28 paulson 2000-06-28 finally theory Bin (the integers) is included
2000-06-28 paulson 2000-06-28 FORCED TO RENAME "W" DUE TO COMPOSE VARIABLE-CLASH BUG
2000-06-28 paulson 2000-06-28 fixed some weak elim rules
2000-06-28 paulson 2000-06-28 implements a classical version of make_elim
2000-06-28 paulson 2000-06-28 uses a supplied version of make_elim for addDs
2000-06-28 paulson 2000-06-28 warns of weak elim rules and ignores them
2000-06-28 paulson 2000-06-28 tidying and unbatchifying
2000-06-28 paulson 2000-06-28 fixed some abuses of addDs and addEs
2000-06-28 paulson 2000-06-28 got rid of weak elim rule
2000-06-28 paulson 2000-06-28 tidied
2000-06-28 paulson 2000-06-28 fixed some weak elim rules
2000-06-28 paulson 2000-06-28 make_elim -> cla_make_elim; tidied
2000-06-28 paulson 2000-06-28 updated and tidied
2000-06-28 paulson 2000-06-28 tidied a monstrous proof
2000-06-28 paulson 2000-06-28 deleted a redundant bind_thm
2000-06-28 paulson 2000-06-28 using the new theorem wf_not_refl; tidied
2000-06-28 paulson 2000-06-28 rev_notE now makes strong elim rules; tidied the file
2000-06-28 paulson 2000-06-28 declaring and using cla_make_elim
2000-06-28 paulson 2000-06-28 new file Provers/make_elim.ML
2000-06-27 wenzelm 2000-06-27 replaced arities by instance;
2000-06-27 wenzelm 2000-06-27 OuterLex.name_of: include val;
2000-06-27 wenzelm 2000-06-27 excursion_result: transform_error;
2000-06-26 wenzelm 2000-06-26 eq_prop: eta contract;
2000-06-26 wenzelm 2000-06-26 tuned msg;
2000-06-26 wenzelm 2000-06-26 tuned;
2000-06-26 wenzelm 2000-06-26 avoid \< in input;
2000-06-26 wenzelm 2000-06-26 export proper induction rule;
2000-06-26 wenzelm 2000-06-26 bind_thm;
2000-06-26 oheimb 2000-06-26 corrected specifications and simplified proofs
2000-06-26 wenzelm 2000-06-26 isar-strip-terminators;
2000-06-26 wenzelm 2000-06-26 updated;
2000-06-26 wenzelm 2000-06-26 tuned;
2000-06-26 wenzelm 2000-06-26 use with_paths;
2000-06-25 wenzelm 2000-06-25 prefer mp over subst; tuned;
2000-06-25 wenzelm 2000-06-25 tuned;
2000-06-25 wenzelm 2000-06-25 Isar theory output.
2000-06-25 wenzelm 2000-06-25 Theory headers (old and new-style).
2000-06-25 wenzelm 2000-06-25 Text with antiquotations of inner items (terms, types etc.).
2000-06-25 wenzelm 2000-06-25 use Library.change;
2000-06-25 wenzelm 2000-06-25 adapted to improved presentation; no longer mirror items from structure Latex;
2000-06-25 wenzelm 2000-06-25 adapted to improved presentation;
2000-06-25 wenzelm 2000-06-25 excursion_result;
2000-06-25 wenzelm 2000-06-25 added extern_skolem;