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

prefer first constant component on merge
2007-10-15, by haftmann
explicit parameter for class finite
2007-10-15, by haftmann
tuned comment;
2007-10-15, by wenzelm
more on authentic syntax;
2007-10-15, by wenzelm
updated method "ferrack";
2007-10-15, by wenzelm
interpreter for List.append added again
2007-10-15, by webertj
quick_and_dirty (again) not touched anymore
2007-10-15, by webertj
require_thy: read_text *after* checking parents
2007-10-14, by wenzelm
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
2007-10-14, by wenzelm
tuned various Class interfaces;
2007-10-14, by wenzelm
removed obsolete Class.class_of_locale/locale_of_class;
2007-10-14, by wenzelm
tuned;
2007-10-14, by wenzelm
added add_def;
2007-10-14, by wenzelm
added is_class;
2007-10-14, by wenzelm
PolyML.Compiler.maxInlineSize := 80;
2007-10-13, by wenzelm
abbrev: return hypothetical def;
2007-10-13, by wenzelm
renamed def to define;
2007-10-13, by wenzelm
(un)overload: full rewrite;
2007-10-13, by wenzelm
add_abbrevs: unvarify result;
2007-10-13, by wenzelm
replaced obsolete Theory.add_finals_i by Theory.add_deps;
2007-10-13, by wenzelm
Theory.specify_const: added deps argument;
2007-10-13, by wenzelm
renamed LocalTheory.def to LocalTheory.define;
2007-10-13, by wenzelm
typo in comment fixed
2007-10-12, by webertj
significant code overhaul, bugfix for inductive data types
2007-10-12, by webertj
added generic provide_file;
2007-10-12, by wenzelm
pass explicit target record -- more informative peek operation;
2007-10-12, by wenzelm
more informative TheoryTarget.peek operation;
2007-10-12, by wenzelm
fork_mixfix: explicit bool argument;
2007-10-12, by wenzelm
eval_term: moved actual evaluation out of CRITICAL section;
2007-10-12, by wenzelm
preventing eta-redexes in theorems from causing failure
2007-10-12, by paulson
trying to make it run faster
2007-10-12, by paulson
calling the correct interface
2007-10-12, by paulson
replaced syntax/translations by abbreviation;
2007-10-12, by wenzelm
updated
2007-10-12, by haftmann
dropped local_syntax
2007-10-12, by haftmann
tuned
2007-10-12, by haftmann
(intermediate quickfix)
2007-10-12, by haftmann
removed
2007-10-12, by haftmann
added
2007-10-12, by haftmann
metis calls
2007-10-12, by paulson
updated
2007-10-12, by haftmann
moved class power to theory Power
2007-10-12, by haftmann
refined; moved class power to theory Power
2007-10-12, by haftmann
consolidated naming conventions for code generator theories
2007-10-12, by haftmann
class div inherits from class times
2007-10-12, by haftmann
code_include replaces code_moduleprolog
2007-10-12, by haftmann
added subclass command
2007-10-12, by haftmann
enabled Refute_Examples again;
2007-10-11, by wenzelm
local_axioms: impose hyps stemming from local consts as well
2007-10-11, by wenzelm
disabled Refute_Examples temporarily;
2007-10-11, by wenzelm
local_theory: incorporated consts into axioms;
2007-10-11, by wenzelm
removed unused/impure quiet_mode;
2007-10-11, by wenzelm
added export_cterm;
2007-10-11, by wenzelm
local_theory: incorporated consts into axioms;
2007-10-11, by wenzelm
replaced Term.equiv_types by Type.similar_types;
2007-10-11, by wenzelm
replaced Term.equiv_types by Type.similar_types;
2007-10-11, by wenzelm
dest/cert_def: replaced Pretty.pp by explicit Proof.context;
2007-10-11, by wenzelm
added elim_implies (more convenient argument order);
2007-10-11, by wenzelm
removed obsolete flip;
2007-10-11, by wenzelm
moved Drule.unvarify to Thm.unvarify (cf. more_thm.ML);
2007-10-11, by wenzelm

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

isabelle