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.
overloading of perm: adhoc name prevents duplicate fact names;
2008-04-14, by wenzelm
Changed naming scheme for theorems generated by interpretations.
2008-04-14, by ballarin
proper context for induct_scheme method
2008-04-14, by krauss
Isar.toplevel_loop: separate init/welcome flag;
2008-04-14, by wenzelm
Sorts.class_error: produce message only (formerly msg_class_error);
2008-04-13, by wenzelm
tsig: removed unnecessary universal witness;
2008-04-13, by wenzelm
simplified handling of sorts, removed unnecessary universal witness;
2008-04-13, by wenzelm
removed unused minimal_classes;
2008-04-13, by wenzelm
added insert_sorts (from thm.ML);
2008-04-13, by wenzelm
tsig: removed unnecessary universal witness;
2008-04-13, by wenzelm
tuned;
2008-04-13, by wenzelm
removed unnecessary Goal.close_result;
2008-04-12, by wenzelm
replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
2008-04-12, by wenzelm
advance: do not count utf8 trailer bytes (which happen to be undefined or punctuation in iso-latin);
2008-04-12, by wenzelm
added is_utf8_trailer;
2008-04-12, by wenzelm
rep_cterm/rep_thm: no longer dereference theory_ref;
2008-04-12, by wenzelm
obsolete -- Poly/ML images are maximally shared already, home-grown compression wastes space and time;
2008-04-12, by wenzelm
removed obsolete compress.ML
2008-04-12, by wenzelm
replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
2008-04-12, by wenzelm
rep_cterm/rep_thm: no longer dereference theory_ref;
2008-04-12, by wenzelm
rep_cterm/rep_thm: no longer dereference theory_ref;
2008-04-12, by wenzelm
use_text: explicitly print exception, which is no longer done by the new PolyML.compiler setup;
2008-04-10, by wenzelm
transaction/init: ensure stable theory (non-draft);
2008-04-10, by wenzelm
export is_draft, not draftN;
2008-04-10, by wenzelm
simplified isarcmd;
2008-04-10, by wenzelm
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
2008-04-10, by wenzelm
eliminated unused trace, read;
2008-04-10, by wenzelm
eliminated unused Toplevel.print3/three_buffers;
2008-04-10, by wenzelm
tuned;
2008-04-10, by wenzelm
Isar.goal: tactical goal only;
2008-04-10, by wenzelm
eliminated backpatching of load_thy;
2008-04-10, by wenzelm
added read_const_exprs (from Pure/Isar/code_unit.ML);
2008-04-10, by wenzelm
export get_names (formerly names);
2008-04-10, by wenzelm
ThyInfo.get_names;
2008-04-10, by wenzelm
ThyInfo.get_theory;
2008-04-10, by wenzelm
export load_thy -- no backpatching;
2008-04-10, by wenzelm
export subst_alias;
2008-04-10, by wenzelm
load thy_info.ML after outer_syntax.ML -- avoids backpatching of load_thy;
2008-04-10, by wenzelm
val theory = ThyInfo.get_theory;
2008-04-10, by wenzelm
replaced Isar loop variants by generic toplevel_loop;
2008-04-10, by wenzelm
replaced Isar loop variants by generic toplevel_loop;
2008-04-10, by wenzelm
The global Isabelle/Isar state and main read-eval-print loop.
2008-04-10, by wenzelm
replaced Isar.toplevel by Toplevel.program;
2008-04-10, by wenzelm
moved global Toplevel state to structure Isar;
2008-04-10, by wenzelm
made purely value-oriented, moved global state to structure Isar (cf. isar.ML);
2008-04-10, by wenzelm
finish: removed unnecessary Isar.init;
2008-04-10, by wenzelm
moved structure Isar to isar.ML;
2008-04-10, by wenzelm
Context.set_thread_data: non-critical;
2008-04-10, by wenzelm
added Isar/isar.ML;
2008-04-10, by wenzelm
improvements are strict
2008-04-10, by haftmann
check validity of class target improvement
2008-04-10, by haftmann
print_consts only for external specifications;
2008-04-09, by wenzelm
fundef_afterqed: removed unused config, added do_print flag;
2008-04-09, by wenzelm
minimal error handling;
2008-04-09, by wenzelm
replaced ML by ML_val;
2008-04-09, by wenzelm
avoid control symbols in document (\<^fixed>);
2008-04-09, by wenzelm
\usepackage[english]{babel} (required for guillemots);
2008-04-09, by wenzelm
renamed mbind to scomp
2008-04-09, by haftmann
removed syntax from monad combinators; renamed mbind to scomp
2008-04-09, by haftmann
rudimentary user-syntax for terms
2008-04-09, by haftmann
less
more
|
(0)
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
+30000
tip