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

updates
2007-11-12, by nipkow
updated
2007-11-12, by haftmann
reactivated default paragraph formatting for ``proof documents'';
2007-11-12, by wenzelm
fixed typo;
2007-11-12, by schirmer
added signatures;
2007-11-12, by schirmer
abbrev: bypass full term check via ProofContext.standard_infer_types (prevents forced expansion);
2007-11-11, by wenzelm
simplified Consts.dest;
2007-11-11, by wenzelm
simplified Consts.dest;
2007-11-11, by wenzelm
simplified Consts.dest;
2007-11-11, by wenzelm
updates
2007-11-11, by nipkow
avoid ML print in production code;
2007-11-11, by wenzelm
updated;
2007-11-11, by wenzelm
auto quickcheck: reduced messages;
2007-11-11, by wenzelm
notation works with any known constant (including fixes/abbrevs);
2007-11-11, by wenzelm
HOL-Statespace;
2007-11-11, by wenzelm
* HOL-Statespace;
2007-11-11, by wenzelm
restore interrupt handler on init;
2007-11-11, by wenzelm
abbrev: back to PrintMode.internal, which works at least half-way;
2007-11-11, by wenzelm
syntax operations: turned extend'' into update'' (absorb duplicates);
2007-11-11, by wenzelm
replaced extend_prtabs by update_prtabs (absorb duplicates);
2007-11-11, by wenzelm
abbrev: PrintMode.input instead of PrintMode.internal for global version!
2007-11-11, by wenzelm
renamed update_list to cons_list;
2007-11-11, by wenzelm
syntax operations: turned extend'' into update'' (absorb duplicates);
2007-11-11, by wenzelm
renamed Symtab.update_list to Symtab.cons_list;
2007-11-11, by wenzelm
tuned specifications of 'notation';
2007-11-11, by wenzelm
added update_const_gram (avoids duplicates);
2007-11-10, by wenzelm
remove_prtabs: tuned, avoid excessive garbage;
2007-11-10, by wenzelm
update_modesyntax: based on Syntax.update_const_gram (avoids duplicates);
2007-11-10, by wenzelm
similar_types: uniform treatment of TFrees/TVars;
2007-11-10, by wenzelm
notation: based on Syntax.update_const_gram (avoids duplicates);
2007-11-10, by wenzelm
tuned specifications of 'notation';
2007-11-10, by wenzelm
removed LocalTheory.target_naming/name;
2007-11-10, by wenzelm
put_inductives: be permissive about multiple versions
2007-11-10, by wenzelm
tuned proofs;
2007-11-10, by wenzelm
tuned document;
2007-11-10, by wenzelm
Orderings.min/max: no need to qualify consts;
2007-11-10, by wenzelm
auto_quickcheck ref: set default in ProofGeneral/preferences only
2007-11-10, by wenzelm
ProofGeneral/preferences: auto_quickcheck=true;
2007-11-10, by wenzelm
qualified Proofterm.proofs;
2007-11-10, by wenzelm
@{const}: improved ProofContext.read_const does the job;
2007-11-10, by wenzelm
locale_const: suppress in class body as well (prevents qualified printing);
2007-11-10, by wenzelm
notation: improved ProofContext.read_const does the job;
2007-11-10, by wenzelm
updated;
2007-11-10, by wenzelm
replaced @{const} (allows name only) by proper @{term};
2007-11-10, by wenzelm
proper implementation of check phase; non-qualified names for class operations
2007-11-09, by haftmann
explicit message for failed autoquickcheck
2007-11-09, by haftmann
tyabbr/syntax/consts: replaced obsolete read_typ by Syntax.parse_typ/certify_typ;
2007-11-09, by wenzelm
avoid obsolete Sign.read_prop;
2007-11-09, by wenzelm
tuned proofs -- avoid implicit prems;
2007-11-09, by wenzelm
fixed imports path;
2007-11-09, by wenzelm
tuned proofs -- avoid open cases;
2007-11-09, by wenzelm
function package: using the names of the equations as case names turned out to be impractical => disabled
2007-11-09, by krauss
avoid name clashes when generating code for union, inter
2007-11-09, by krauss
oops -- avoid vacous goal message;
2007-11-08, by wenzelm
tuned messages;
2007-11-08, by wenzelm
avoid "import" as identifier, which is a keyword in Alice;
2007-11-08, by wenzelm
tuned presentation;
2007-11-08, by wenzelm
avoid implicit use of prems;
2007-11-08, by wenzelm
where/of: do not allow schematic variables here!
2007-11-08, by wenzelm
removed unused read_termTs_schematic, read/cert_vars_legacy, add_fixes_legacy;
2007-11-08, by wenzelm

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

isabelle