isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

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

misc tuning;
2013-05-30, by wenzelm
tuned;
2013-05-30, by wenzelm
tuned signature;
2013-05-30, by wenzelm
stay within regular tactic language -- avoid operating on whole proof state;
2013-05-30, by wenzelm
standardized aliases;
2013-05-30, by wenzelm
space between minus sign and number for large negative number literals causes NumberFormatException at run-time
2013-05-30, by Andreas Lochbihler
tuned
2013-05-30, by nipkow
relational version of HoareT
2013-05-30, by kleing
obsolete;
2013-05-29, by wenzelm
resolve_inc_tyvars: back to old behavior before 0fa3b456a267 where types of equal Vars are *not* unified -- recover last example in src/HOL/Metis_Examples/Clausification.thy;
2013-05-29, by wenzelm
more precise "incremented" indication, which might be relevant in corner cases, e.g. instantiation of leading to vars with different types (which is a potential problem nonetheless);
2013-05-29, by wenzelm
tuned signature -- more explicit flags for low-level Thm.bicompose;
2013-05-29, by wenzelm
unify types of schematic variables in non-lifted case (i.e. "compose variants") -- allow schematic polymorphism, without revisiting HO-unification;
2013-05-29, by wenzelm
tuned signature;
2013-05-29, by wenzelm

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

isabelle