Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
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.
more operations: for testing purposes;
19 months ago, by wenzelm
provide naproche-20220910 (inactive);
19 months ago, by wenzelm
clarified directory names (e.g. for multi-platform remote execution): avoid being deleted via isabelle.Components.purge;
19 months ago, by wenzelm
unused;
19 months ago, by wenzelm
update for release;
19 months ago, by wenzelm
tuned: prefer Scala Regex operations;
19 months ago, by wenzelm
tuning and updates for release;
19 months ago, by wenzelm
NEWS;
19 months ago, by wenzelm
discontinued somewhat pointless option: Proof_Display.pretty_goal_inst should always work smoothly (and not crash unexpectedly);
19 months ago, by wenzelm
give up show_main_goal (despite 922e3f9251ac): show_goal_inst is sufficient, even for final results;
19 months ago, by wenzelm
merged
19 months ago, by wenzelm
discontinue fragile operations;
19 months ago, by wenzelm
proper context option: change of underlying Options.default will not survive PIDE "Prover.options" (e.g. change of Isabelle/jEdit plugin options);
19 months ago, by wenzelm
enable show_goal_inst by default: match failure is merely a warning (see 730638d4e37a);
19 months ago, by wenzelm
updated documentation;
19 months ago, by wenzelm
support multiple sessions, with cumulative errors;
19 months ago, by wenzelm
support regex patterns on messages;
19 months ago, by wenzelm
support Pretty.unformatted, similar to ML version;
19 months ago, by wenzelm
removed odd TODO item (see 3391a493f39a);
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
tuned output: more Pretty.item;
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
clarified failure: warning for logical error, exception for program breakdown;
19 months ago, by wenzelm
print goal instantiation for global qed (and variations);
19 months ago, by wenzelm
clarified output;
19 months ago, by wenzelm
more robust: capture corner case seen in line 631 of "$AFP/Automatic_Refinement/Autoref_Bindings_HOL.thy" (AFP/6c87f24bb773);
19 months ago, by wenzelm
clarified message channel for 'print_state' (NB: the command was originally for TTY or Proof General);
19 months ago, by wenzelm
updated to postgresql-42.5.0;
19 months ago, by wenzelm
tool to build Isabelle component for PostgreSQL JDBC;
19 months ago, by wenzelm
clarified goal structure with proper instantiation of main goal, to support "show_goal_inst";
19 months ago, by wenzelm
option "show_states" for more verbosity of batch-builds;
19 months ago, by wenzelm
tuned --- avoid warnings;
19 months ago, by wenzelm
proper antiquotations;
19 months ago, by wenzelm
inline markup for Output.state (in contrast to c94bba7906d2): make messages available via Rendering.text_messages and thus "isabelle log" (see cb0c407fbc6e), while Rendering.output_messages of Isabelle/jEdit/VSCode is unaffected;
19 months ago, by wenzelm
proper antiquotations;
19 months ago, by wenzelm
clarified options, following e.g. "show_consts";
19 months ago, by wenzelm
proper Envir.subst operations: env is already normalized, using Envir.norm may lead to non-termination;
19 months ago, by wenzelm
unused (see 15758fced053);
19 months ago, by wenzelm
clarified modules;
19 months ago, by wenzelm
show goal instantiation, notably for 'schematic_goal' command (inactive by default);
19 months ago, by wenzelm
proper umlauts;
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
tuned;
19 months ago, by wenzelm
tuned;
19 months ago, by wenzelm
tuned error message;
19 months ago, by wenzelm
merged
19 months ago, by desharna
merged
20 months ago, by desharna
moved antimono to Fun and redefined it as an abbreviation
22 months ago, by desharna
moved mono and strict_mono to Fun and redefined them as abbreviations
22 months ago, by desharna
clarified generic euclidean relation
19 months ago, by haftmann
added a bound in SMT on the number of schematic constants considered -- the code (in for_schematics) is exponential in that number
19 months ago, by blanchet
tuned signature;
20 months ago, by wenzelm
check imports more strictly, e.g. reject ".../Pure" or ".../HOL-Library.Multiset";
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
tuned --- more robust syntax;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
back to more traditional import_name (reverting cceb10dcc9f9), e.g. relevant for "isabelle jedit -l CTT src/CTT/ex/Elimination.thy" to produce proper error "Cannot update finished theory CTT.Elimination";
20 months ago, by wenzelm
unused (see 347ed6219dab);
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
tip