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 -56 +56 +100 +300 +1000 +3000 +10000 +30000 tip

final draft
2006-11-22, by haftmann
made SML/NJ happy;
2006-11-21, by wenzelm
theorem(_i): note assms of statement;
2006-11-21, by wenzelm
removed obsolete simple_note_thms;
2006-11-21, by wenzelm
added assmsN;
2006-11-21, by wenzelm
* Isar: the assumptions of a long theorem statement are available as assms;
2006-11-21, by wenzelm
activated x86_64-linux;
2006-11-21, by wenzelm
renamed Proof.put_thms_internal to Proof.put_thms;
2006-11-21, by wenzelm
simplified Proof.theorem(_i);
2006-11-21, by wenzelm
added stmt mode, which affects naming/indexing of local facts;
2006-11-21, by wenzelm
simplified theorem(_i);
2006-11-21, by wenzelm
notes: proper kind;
2006-11-21, by wenzelm
notes: proper kind;
2006-11-21, by wenzelm
removed kind attribs;
2006-11-21, by wenzelm
moved theorem kinds from PureThy to Thm;
2006-11-21, by wenzelm
moved theorem kinds from PureThy to Thm;
2006-11-21, by wenzelm
LocalTheory.notes/defs: proper kind;
2006-11-21, by wenzelm
LocalTheory.axioms/notes/defs: proper kind;
2006-11-21, by wenzelm
simplified Proof.theorem(_i);
2006-11-21, by wenzelm
LocalTheory.axioms/notes/defs: proper kind;
2006-11-21, by wenzelm
Optimized class_pairs for the common case of no subclasses
2006-11-21, by paulson
Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists
2006-11-21, by paulson
New transformation of eliminatino rules: we simply replace the final conclusion variable by False
2006-11-21, by paulson
run poly-4.9.1 as stable and poly-4.2.0 as experimental on at
2006-11-21, by kleing
removed legacy ML setup;
2006-11-21, by wenzelm
converted legacy ML scripts;
2006-11-21, by wenzelm
converted legacy ML scripts;
2006-11-20, by wenzelm
HOL-Prolog: converted legacy ML scripts;
2006-11-20, by wenzelm
start at-sml earlier and on different machine, remove sun-sml test (takes too long)
2006-11-20, by kleing
HOL-Algebra: converted legacy ML scripts;
2006-11-19, by wenzelm
profiling disabled
2006-11-19, by webertj
code thms for classops violating type discipline ignored
2006-11-18, by haftmann
cleanup
2006-11-18, by haftmann
added instance for class size
2006-11-18, by haftmann
added combinators and lemmas
2006-11-18, by haftmann
using class instance
2006-11-18, by haftmann
dvd_def now with object equality
2006-11-18, by haftmann
op div/op mod now named without leading op
2006-11-18, by haftmann
workaround for definition violating type discipline
2006-11-18, by haftmann
moved dvd stuff to theory Divides
2006-11-18, by haftmann
re-eliminated thm trichotomy
2006-11-18, by haftmann
power is now a class
2006-11-18, by haftmann
tuned
2006-11-18, by haftmann
clarified module dependencies
2006-11-18, by haftmann
div is now a class
2006-11-18, by haftmann
reduced verbosity
2006-11-18, by haftmann
adjustments for class package
2006-11-18, by haftmann
added an intro lemma for freshness of products; set up
2006-11-17, by urbanc
more robust syntax for definition/abbreviation/notation;
2006-11-17, by wenzelm
'notation': more robust 'and' list;
2006-11-17, by wenzelm
updated;
2006-11-17, by wenzelm
added Isar.goal;
2006-11-17, by wenzelm
added where_;
2006-11-17, by wenzelm
add lemmas LIM_zero_iff, LIM_norm_zero_iff
2006-11-16, by huffman
Includes type:sort constraints in its code to collect predicates in axiom clauses.
2006-11-16, by paulson
Now includes only types used to instantiate overloaded constants in arity clauses
2006-11-16, by paulson

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

isabelle