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

made smlnj happy;
2006-05-23, by wenzelm
pretty_full_theory: tuned output of definitions;
2006-05-23, by wenzelm
export plain_args;
2006-05-23, by wenzelm
Defs.specifications_of: lhs/rhs now use typargs;
2006-05-22, by wenzelm
removed unchecked'';
2006-05-22, by wenzelm
pretty_full_theory: defs;
2006-05-22, by wenzelm
specifications_of: lhs/rhs represented as typargs;
2006-05-22, by wenzelm
export raw_unifys, could_unifys;
2006-05-22, by wenzelm
made smlnj happy;
2006-05-20, by wenzelm
export raw_matches;
2006-05-20, by wenzelm
tuned Defs interfaces;
2006-05-20, by wenzelm
yet another re-implementation:
2006-05-20, by wenzelm
removed obsolete partition (cf. List.partition);
2006-05-20, by wenzelm
class axiomatization: finals;
2006-05-20, by wenzelm
abs: precise typing;
2006-05-20, by wenzelm
added syntax for 'unchecked';
2006-05-20, by wenzelm
primrec (unchecked);
2006-05-20, by wenzelm
List.partition;
2006-05-20, by wenzelm
ax_derivs: precise typing;
2006-05-20, by wenzelm
pow: unchecked;
2006-05-20, by wenzelm
removed obsolete 'finalconsts';
2006-05-20, by wenzelm
* Pure: syntax 'CONST name' produces a fully internalized constant;
2006-05-17, by wenzelm
added CONST syntax;
2006-05-17, by wenzelm
export generic term_syntax;
2006-05-17, by wenzelm
consts: replaced early'' flag by inverted authentic'';
2006-05-17, by wenzelm
added mapping;
2006-05-17, by wenzelm
replaced early'' flag by inverted authentic'';
2006-05-17, by wenzelm
renamed CONST to CONSTANT;
2006-05-17, by wenzelm
removing the string array from the result of get_clasimp_atp_lemmas
2006-05-17, by paulson
const_syntax;
2006-05-17, by wenzelm
always preserve authentic consts -- removed Syntax.mixfix_const;
2006-05-17, by wenzelm
tuned;
2006-05-17, by wenzelm
removed outdated/redundant comments;
2006-05-17, by wenzelm
prefer 'definition' over low-level defs;
2006-05-17, by wenzelm
tuned source/document;
2006-05-17, by wenzelm
hide const subst;
2006-05-16, by wenzelm
tuned;
2006-05-16, by wenzelm
const_syntax;
2006-05-16, by wenzelm
* Isar/locale: 'const_syntax';
2006-05-16, by wenzelm
added const_syntax(_i);
2006-05-16, by wenzelm
export consts_of;
2006-05-16, by wenzelm
replaced abbrevs by term_syntax, which is both simpler and more general;
2006-05-16, by wenzelm
added syntax interface;
2006-05-16, by wenzelm
added add_modesyntax;
2006-05-16, by wenzelm
added 'const_syntax';
2006-05-16, by wenzelm
added add_const_syntax, add_consts_authentic;
2006-05-16, by wenzelm
added syntax interface;
2006-05-16, by wenzelm
tuned concrete syntax -- abbreviation/const_syntax;
2006-05-16, by wenzelm
updated;
2006-05-16, by wenzelm
updated;
2006-05-16, by wenzelm
* Pure/library: divide_and_conquer;
2006-05-16, by wenzelm
replaced references to the robot by the mailing list page
2006-05-16, by paulson
added a much simpler proof for the iteration and
2006-05-16, by urbanc
Amine Chaieb: Ferrante and Rackoff Algorithm;
2006-05-16, by wenzelm
Sign.certify_sort;
2006-05-16, by wenzelm
tuned;
2006-05-16, by wenzelm
removed low-level str_of_sort/typ/term (use Display.raw_string_of_sort/typ/term instead, or even PolyML.print -- for debugging purposes);
2006-05-16, by wenzelm
avoid low-level Term.str_of_term;
2006-05-16, by wenzelm
abstract interfaces for type algebra;
2006-05-16, by wenzelm
added divide_and_conquer combinator (by Amine Chaieb);
2006-05-16, by wenzelm

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

isabelle