isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

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

tuned
2008-10-17, by haftmann
filled remaining gaps
2008-10-17, by haftmann
added type antiquotation
2008-10-17, by haftmann
tuned;
2008-10-16, by wenzelm
added dep for Concurrent/ROOT.ML;
2008-10-16, by wenzelm
tuned;
2008-10-16, by wenzelm
removed Locales;
2008-10-16, by wenzelm
goal-directed proof now enforces strict proof irrelevance wrt. sort hypotheses;
2008-10-16, by wenzelm
added translations for SORT_CONSTRAINT
2008-10-16, by wenzelm
conclude_goal: precise goal context, include all sorts from context into statement, check shyps of result;
2008-10-16, by wenzelm
added make;
2008-10-16, by wenzelm
maintain sort occurrences of declared terms;
2008-10-16, by wenzelm
added weaken_sorts;
2008-10-16, by wenzelm
added make, minimal_sorts;
2008-10-16, by wenzelm
added const sort_constraint with syntax SORT_CONSTRAINT -- logically vacous;
2008-10-16, by wenzelm
added check_shyps, which reject pending sort hypotheses;
2008-10-16, by wenzelm
Drule.norm_hhf_eqs;
2008-10-16, by wenzelm
prove_common: include all sorts from context into statement, check shyps of result;
2008-10-16, by wenzelm
added rules for sort_constraint, include in norm_hhf_eqs;
2008-10-16, by wenzelm
tuned;
2008-10-16, by wenzelm
avoid accidental dependency of automated proof on sort equiv;
2008-10-16, by wenzelm
explicit SORT_CONSTRAINT for proofs depending implicitly on certain sorts;
2008-10-16, by wenzelm
avoid CRITICAL with_path;
2008-10-16, by wenzelm
rewrite more proofs in Isar style
2008-10-16, by huffman
Removed ex/Locales.thy.
2008-10-16, by ballarin
More occurrences of 'includes' gone.
2008-10-16, by ballarin
Removed outdated locales tutorial.
2008-10-16, by ballarin
correct rounding
2008-10-16, by haftmann

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

isabelle