Mercurialisabelle / shortlog
summary | shortlog | changelog | graph | tags | branches | files | gz

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