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

deftab: only process theorems on demand
2009-07-20, by haftmann
no SAME exceptions in uncritical code
2009-07-20, by krauss
merged
2009-07-20, by haftmann
less digestible
2009-07-20, by haftmann
refined outline structure
2009-07-20, by haftmann
replaced usedir option -Q by more fine-grained -q;
2009-07-20, by wenzelm
merged
2009-07-20, by wenzelm
merged
2009-07-20, by haftmann
closer relation of sets and complete lattices; corresponding consts, defs and syntax at similar places in theory text
2009-07-20, by haftmann
merged
2009-07-15, by haftmann
merged
2009-07-20, by haftmann
simplification of locale interfaces
2009-07-15, by haftmann
additional preprocessor rule
2009-07-15, by haftmann
added code_unfold_post attribute
2009-07-14, by haftmann
more accessors to unfold simpset
2009-07-14, by haftmann
clarified code
2009-07-14, by haftmann
prefer code_inline over code_unfold; use code_unfold_post where appropriate
2009-07-14, by haftmann
tuned code annotations
2009-07-14, by haftmann
more canonical import
2009-07-14, by haftmann
merged
2009-07-14, by haftmann
merged
2009-07-14, by haftmann
refinement of lattice classes
2009-07-14, by haftmann
removed outdated comment
2009-07-13, by haftmann
Proof.future_proof: declare all assumptions as well;
2009-07-20, by wenzelm
parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
2009-07-19, by wenzelm
cancel_proofs: some attempts at reworking group management (based on body promises only);
2009-07-19, by wenzelm
support for arbitrarity nested future proofs -- replaced crude order by explicit normalization (which might loop for bad dependencies);
2009-07-19, by wenzelm
more abstract Future.is_worker;
2009-07-19, by wenzelm
tuned;
2009-07-19, by wenzelm
future_result: explicitly impose Variable.sorts_of again;
2009-07-19, by wenzelm
recovered a version of dequeue_towards (cf. bb7b5a5942c7);
2009-07-19, by wenzelm
added join_bodies;
2009-07-18, by wenzelm
scheduler: tuned tracing (status);
2009-07-18, by wenzelm
added group_id;
2009-07-18, by wenzelm
synchronized: tuned tracing;
2009-07-18, by wenzelm
tuned;
2009-07-18, by wenzelm
tuned prf_subst: use structure Same;
2009-07-18, by wenzelm
merged
2009-07-17, by wenzelm
Changed fact_Suc_nat back to fact_Suc
2009-07-17, by avigad
merged
2009-07-17, by wenzelm
merged
2009-07-17, by berghofe
merged
2009-07-15, by berghofe
commit merge
2009-07-14, by avigad
Repairs regarding new Fact.thy.
2009-07-14, by avigad
merged
2009-07-14, by berghofe
merged
2009-07-14, by berghofe
Use term antiquotation to refer to constant names in subsection title.
2009-07-14, by berghofe
Repaired uses of factorial.
2009-07-10, by avigad
Automated merge with http://isabelle.in.tum.de/repos/isabelle
2009-07-10, by avigad
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
2009-07-10, by avigad
tuned/modernized Envir.subst_XXX;
2009-07-17, by wenzelm
tuned/modernized subst: Same.operation;
2009-07-17, by wenzelm
tuned;
2009-07-17, by wenzelm
tuned/modernized Envir operations;
2009-07-17, by wenzelm
major cleanup, simplification, modernization;
2009-07-17, by wenzelm
eq_type: special case for empty environment;
2009-07-17, by wenzelm
compare types directly -- no need to invoke Type.eq_type with empty environment;
2009-07-17, by wenzelm
incr_indexes (from Proofterm);
2009-07-16, by wenzelm
tuned incr_indexes;
2009-07-16, by wenzelm
tuned incr_tvar_same;
2009-07-16, by wenzelm

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

isabelle