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
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
thy_name: be very liberal about file name format (workaround problem with XEmacs on cygwin);
2007-11-15, by wenzelm
isatool version: clarify that this is the *long* form;
2007-11-15, by wenzelm
ISABELLE_IDENTIFIER is filled in automatically, not taken from the *long* form of isatool version!
2007-11-15, by wenzelm
cover ISABELLE_IDENTIFIER;
2007-11-15, by wenzelm
README for E binary distribution;
2007-11-14, by wenzelm
tuned;
2007-11-14, by wenzelm
patching in the latest changes from Hurd
2007-11-13, by paulson
tuned;
2007-11-13, by wenzelm
some more items;
2007-11-13, by wenzelm
updated
2007-11-13, by nipkow
Added JAR paper by Wenzel and Wiedijk.
2007-11-13, by berghofe
Removed some case_names and consumes attributes that are now no longer
2007-11-13, by berghofe
Added TrueE to extraction_expand.
2007-11-13, by berghofe
Added new program extraction examples.
2007-11-13, by berghofe
New case studies for program extraction.
2007-11-13, by berghofe
Moved auxiliary lemmas to separate theory.
2007-11-13, by berghofe
Added new exampes Greatest_Common_Divisor and Euclid.
2007-11-13, by berghofe
Moved nat_eq_dec to Util.thy
2007-11-13, by berghofe
Moved nat_eq_dec and search to Util.thy
2007-11-13, by berghofe
Tuned.
2007-11-13, by berghofe
to_pred and to_set now save induction and case rule tags.
2007-11-13, by berghofe
removed left-over text links from lynx conversion;
2007-11-12, by wenzelm
back to sigusr2, after Poly/ML 5.1 has been adapted;
2007-11-12, by wenzelm
changed Posix.Signal.usr2 to Posix.Signal.usr1 to make it work with Poly/ML 5.1;
2007-11-12, by wenzelm
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
less
more
|
(0)
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
+30000
tip