isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 +30000 tip

theorems [trans] = rev_mp mp;
2000-02-27, by wenzelm
use NetRules;
2000-02-27, by wenzelm
added major_prem_of;
2000-02-27, by wenzelm
added Isar/net_rules.ML;
2000-02-27, by wenzelm
simplified induct method;
2000-02-24, by wenzelm
tuned;
2000-02-24, by wenzelm
induct method: implicit rule;
2000-02-24, by wenzelm
rN = "record";
2000-02-24, by wenzelm
all_cases / all_inducts;
2000-02-24, by wenzelm
workaround res_inst_tac/lift_inst_rule bug by explicit type contraint;
2000-02-24, by wenzelm
capply, cabs: Sign.nodup_vars;
2000-02-24, by wenzelm
nodup_vars: fixed omission of 2 minor cases; account for Frees as well;
2000-02-24, by wenzelm
tuned generated TeX code;
2000-02-24, by wenzelm
renamed a lemma
2000-02-24, by nipkow
Added and renamed a lemma.
2000-02-24, by nipkow
not working yet. partial conversion to use "rename" instead of "extend"
2000-02-23, by paulson
new theorems inj_iff, surj_iff
2000-02-23, by paulson
new reference korf85
2000-02-23, by paulson
* Pure now provides its own version of intro/elim/dest attributes;
2000-02-22, by wenzelm
tuned syntax wrapper;
2000-02-22, by wenzelm
tuned "induct" syntax;
2000-02-22, by wenzelm
"cases" method;
2000-02-22, by wenzelm
added cases_tac;
2000-02-22, by wenzelm
induct: tuned syntax;
2000-02-22, by wenzelm
added cases_of, cases;
2000-02-22, by wenzelm
removed case_split thm binding;
2000-02-22, by wenzelm
added boolN;
2000-02-22, by wenzelm
proper variant names (admit field "r");
2000-02-22, by wenzelm
three easy new examples
2000-02-22, by paulson
tuned footnote;
2000-02-21, by wenzelm

less more | (0) -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle