2000-03-01 wenzelm tuned;
2000-03-01 paulson expandshort
2000-03-01 paulson added a reference
2000-03-01 paulson new theorems from Sidi Ould Ehmety
2000-02-29 wenzelm tuned;
2000-02-29 wenzelm add_cases_induct: project_rules accomodates mutual induction;
2000-02-29 wenzelm tuned msgs;
2000-02-29 paulson even Alloc works again, using "rename"
2000-02-29 paulson replaced UN_constant, INT_constant by unconditional versions that rewrite
2000-02-28 wenzelm add_cases_induct: accomodate no_elim and no_ind flags;
2000-02-28 paulson new mostly working version; Alloc nearly converted to "Rename"
2000-02-28 paulson new thm vimage_Collect_eq
2000-02-28 paulson more bijection theorems
2000-02-27 wenzelm cases/induct attributes;
2000-02-27 wenzelm add_cases_induct: induct_method setup;
2000-02-27 wenzelm HOLogic.dest_conj;
2000-02-27 wenzelm HOLogic.dest_conj;
2000-02-27 wenzelm even better induct setup;
2000-02-27 wenzelm early setup of induct_method;
2000-02-27 wenzelm added dest_conj;
2000-02-27 wenzelm theorems [trans] = rev_mp mp;
2000-02-27 wenzelm use NetRules;
2000-02-27 wenzelm added major_prem_of;
2000-02-27 wenzelm added Isar/net_rules.ML;
2000-02-24 wenzelm simplified induct method;
2000-02-24 wenzelm tuned;
2000-02-24 wenzelm induct method: implicit rule;
2000-02-24 wenzelm rN = "record";
Loading...
(0) -3000 -1000 -300 -100 -50 -28 +28 +50 +100 +300 +1000 +3000 +10000 +30000 tip