Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-240
+240
+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.
tuned signature;
23 months ago, by wenzelm
clarified signature: replaced Sessions.Deps by Sessions.Structure from HTML_Context;
23 months ago, by wenzelm
tuned;
23 months ago, by wenzelm
clarified signature: avoid constants from Sessions.Structure within Session.Base;
23 months ago, by wenzelm
clarified signature: avoid object-oriented HTML_Context;
23 months ago, by wenzelm
tuned type signature
23 months ago, by haftmann
tuned type signature
23 months ago, by haftmann
streamlined theorems
23 months ago, by haftmann
more thorough split rules for div and mod on numerals, tuned split rules setup
23 months ago, by haftmann
streamlined simpset building, avoiding duplicated rewrite rules
23 months ago, by haftmann
consolidated attribute name
23 months ago, by haftmann
streamlined theorems
23 months ago, by haftmann
streamlined theorems and sections
23 months ago, by haftmann
streamlined primitive definitions for integer division
23 months ago, by haftmann
reintroduced SPASS to the mix
23 months ago, by blanchet
tweaked generation of Isar proofs
23 months ago, by blanchet
tweak Sledgehammer's slicing mechanism -- updated Zipperposition's slices and make them half as long as other provers' to pack more of them in 30 s
23 months ago, by blanchet
tuned comments;
23 months ago, by wenzelm
updated to sumatra_pdf-3.4.6;
23 months ago, by wenzelm
proper Java/Scala compiler classpath (amending b42e20adaeed): ISABELLE_SETUP_CLASSPATH must not be included prematurely (breaks on Windows), instead use runtime Classpath().jars;
23 months ago, by wenzelm
revived 'try0' and 'smart' Isar proofs in Sledgehammer
23 months ago, by blanchet
Cleanup of NonstandardAnalysis
23 months ago, by paulson
A bit of cleaning up
23 months ago, by paulson
The same, without adding a new simprule
23 months ago, by paulson
moved some material from Sum_of_Powers
23 months ago, by paulson
merged
23 months ago, by wenzelm
clarified signature;
23 months ago, by wenzelm
clarified theory_names with exported content;
23 months ago, by wenzelm
proper export theory_names: theory/parents are not necessarily present (amending 4d27b520622a);
23 months ago, by wenzelm
proper treatment of empty lines (amending 08f89f0e8a62);
23 months ago, by wenzelm
clarified signature: avoid confusing operation name (amending 8cf14d4ebec4);
23 months ago, by wenzelm
merged
23 months ago, by paulson
The right way to formulate card_UNION, plus the old version for compatibility
23 months ago, by paulson
tuned comments;
23 months ago, by wenzelm
tuned signature;
23 months ago, by wenzelm
clarified signature;
23 months ago, by wenzelm
clarified signature;
23 months ago, by wenzelm
clarified signature;
23 months ago, by wenzelm
unused;
23 months ago, by wenzelm
clarified modules;
23 months ago, by wenzelm
clarified signature;
23 months ago, by wenzelm
clarified signature: more explicit types;
23 months ago, by wenzelm
clarified signature --- avoid dependent types;
23 months ago, by wenzelm
tuned whitespace;
23 months ago, by wenzelm
clarified signature: avoid public representation;
23 months ago, by wenzelm
tuned signature;
23 months ago, by wenzelm
clarified signature;
23 months ago, by wenzelm
unused;
23 months ago, by wenzelm
more accurate treatment of option "editor_output_state", e.g. when changed via Isabelle/jEdit Plugin Options panel;
23 months ago, by wenzelm
clarified signature: more explicit types;
23 months ago, by wenzelm
tuned whitespace;
23 months ago, by wenzelm
tuned, following 298707451ec2;
23 months ago, by wenzelm
unused;
23 months ago, by wenzelm
tuned, following hints by IntelliJ IDEA;
23 months ago, by wenzelm
clarified signature: more explicit types;
23 months ago, by wenzelm
tuned whitespace;
23 months ago, by wenzelm
tuned, following hints by IntelliJ IDEA;
23 months ago, by wenzelm
merged
23 months ago, by wenzelm
more GUI elements;
23 months ago, by wenzelm
clarified signature;
23 months ago, by wenzelm
tuned;
23 months ago, by wenzelm
tuned, following hints by IntelliJ IDEA;
23 months ago, by wenzelm
clarified signature --- more operations;
23 months ago, by wenzelm
clarified signature --- simplified types;
23 months ago, by wenzelm
tuned signature;
23 months ago, by wenzelm
proper toString for Content_XML, which is not covered by trait Content;
23 months ago, by wenzelm
clarified output;
23 months ago, by wenzelm
clarified signature: support different document_session, e.g. within running PIDE session;
23 months ago, by wenzelm
unused (despite cf52379c0776);
23 months ago, by wenzelm
tuned, following hints by IntelliJ IDEA;
23 months ago, by wenzelm
unused (see 696819fe2424);
23 months ago, by wenzelm
clarified signature;
23 months ago, by wenzelm
basic setup for document build panel;
23 months ago, by wenzelm
tuned, following hints by IntelliJ IDEA;
23 months ago, by wenzelm
tuned, following hints by IntelliJ IDEA;
23 months ago, by wenzelm
tuned;
23 months ago, by wenzelm
clarified signature;
23 months ago, by wenzelm
tuned, following hints by IntelliJ IDEA;
23 months ago, by wenzelm
tuned, following hints by IntelliJ IDEA;
23 months ago, by wenzelm
tuned signature;
23 months ago, by wenzelm
tuned signature;
23 months ago, by wenzelm
tuned signature, following hints by IntelliJ IDEA;
23 months ago, by wenzelm
added support for cvc5 (whose interface is almost identical to CVC4)
23 months ago, by blanchet
removing the [simp] attribute breaks too many AFP entries severely
23 months ago, by nipkow
nlists is picked up automatically but conflicts with the RBT setup
23 months ago, by nipkow
new lemma
23 months ago, by nipkow
merged
23 months ago, by nipkow
New theory of fixed length lists
23 months ago, by nipkow
Further streamlining of quick-and-dirty evaluation.
23 months ago, by haftmann
more correct approximation (contributed by Achim Brucker)
23 months ago, by Achim D. Brucker
Added tag Isabelle2022-RC0 for changeset b42e20adaeed
23 months ago, by wenzelm
proper Java/Scala compiler classpath for standalone application (see also make_isabelle_app() in Pure/Admin/build_release.scala);
23 months ago, by wenzelm
clarified message;
23 months ago, by wenzelm
provide naproche-20220808 (inactive);
23 months ago, by wenzelm
more robust data representation: notably for Store.read_session_timing with database_server;
23 months ago, by wenzelm
tuned message;
23 months ago, by wenzelm
afford default cache policy, despite 6a29709906c6;
23 months ago, by wenzelm
tuned signature;
23 months ago, by wenzelm
clarified signature: more uniform treatment of cache for Export.read_session vs. Export.read_theory;
23 months ago, by wenzelm
tuned;
23 months ago, by wenzelm
tuned signature;
23 months ago, by wenzelm
clarified signature;
23 months ago, by wenzelm
clarified modules;
23 months ago, by wenzelm
merged
23 months ago, by wenzelm
tuned;
23 months ago, by wenzelm
clarified message;
23 months ago, by wenzelm
clarified signature: prefer Export.Session_Context over Sessions.Database_Context;
23 months ago, by wenzelm
clarified signature: prefer Export.Context;
23 months ago, by wenzelm
clarified signature: find session_database within Session_Context.db_hierarchy;
23 months ago, by wenzelm
clarified signature: prefer Export.Session_Context;
23 months ago, by wenzelm
prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context;
23 months ago, by wenzelm
clarified signature;
23 months ago, by wenzelm
tuned signature, following hints by IntelliJ IDEA;
23 months ago, by wenzelm
clarified signature: more robust treatment of server;
23 months ago, by wenzelm
discontinued Export.Provider in favour of Export.Context and its derivatives;
23 months ago, by wenzelm
clarified signature: less redundant -- Sessions.Base_Info already specifies the main session;
23 months ago, by wenzelm
tuned signature: more operations;
23 months ago, by wenzelm
misc tuning and clarification;
23 months ago, by wenzelm
clarified Document.Snapshot.all_exports: refer to material from this (virtual) session;
23 months ago, by wenzelm
clarified database query: refer to semantic theories;
23 months ago, by wenzelm
clarified signature: more operations;
23 months ago, by wenzelm
clarified signature: persistent theory_names in lexical order;
23 months ago, by wenzelm
proper session_databases for database_server: need to follow precise session_hierarchy;
23 months ago, by wenzelm
redundant;
23 months ago, by wenzelm
clarified signature: more robust close operation;
23 months ago, by wenzelm
more uniform exports: proper encoding of empty parents for Pure;
23 months ago, by wenzelm
clarified signature: more uniform treatment of empty exports;
23 months ago, by wenzelm
clarified session name: treat PIDE session as Sessions.DRAFT with imports from other sessions;
23 months ago, by wenzelm
more robust build_hierarchy: support Resources.empty / Sessions.Structure.empty (required for Build_Job.print_log);
23 months ago, by wenzelm
clarified context for retrieval: more explicit types, with optional close() operation;
23 months ago, by wenzelm
tuned;
23 months ago, by wenzelm
unused;
23 months ago, by wenzelm
retrieve information about used files;
23 months ago, by wenzelm
tuned signature -- more robust;
23 months ago, by wenzelm
tuned signature;
23 months ago, by wenzelm
clarified signature: Export.Provider knows its (accidental) theory_names;
23 months ago, by wenzelm
clarified signature;
23 months ago, by wenzelm
tuned, following hints by IntelliJ IDEA;
23 months ago, by wenzelm
clarified signature: proper session_name for Sessions.Base (like Sessions.Info);
23 months ago, by wenzelm
tuned signature;
23 months ago, by wenzelm
clarified signature;
23 months ago, by wenzelm
clarified signature;
23 months ago, by wenzelm
clarified signature;
23 months ago, by wenzelm
avoid multiple load_commands;
23 months ago, by wenzelm
avoid redundant dependencies.load_commands with potential errors (amending ea4f86914cb2);
23 months ago, by wenzelm
tuned signature -- avoid redundant arguments;
23 months ago, by wenzelm
tuned -- following hints by IntelliJ IDEA;
23 months ago, by wenzelm
tuned signature;
23 months ago, by wenzelm
tuned comments;
23 months ago, by wenzelm
removed somewhat pointless transaction: db is meant to be finished (or updated monotonically);
23 months ago, by wenzelm
tuned signature;
23 months ago, by wenzelm
clarified signature;
23 months ago, by wenzelm
clarified signature: avoid repeated db_context.input_database;
23 months ago, by wenzelm
clarified signature: more robust;
23 months ago, by wenzelm
removed somewhat pointless operations (see a6c69599ab99);
23 months ago, by wenzelm
clarified signature;
23 months ago, by wenzelm
tuned;
23 months ago, by wenzelm
tuned;
23 months ago, by wenzelm
clarified signature;
23 months ago, by wenzelm
clarified names;
23 months ago, by wenzelm
clarified signature;
23 months ago, by wenzelm
clarified names;
23 months ago, by wenzelm
clarified signature;
23 months ago, by wenzelm
clarified signature: more explicit types;
23 months ago, by wenzelm
unused (see 0d30ea76756c);
23 months ago, by wenzelm
tuned;
23 months ago, by wenzelm
clarified signature;
23 months ago, by wenzelm
tuned;
23 months ago, by wenzelm
unused (see 3064e165c660);
23 months ago, by wenzelm
merge
23 months ago, by blanchet
changed the order of Zipperposition slices in Sledgehammer
23 months ago, by blanchet
merged
23 months ago, by paulson
The wellordering instantiation for length-ordered lists
23 months ago, by paulson
show sum_list defn
23 months ago, by nipkow
prettified def
23 months ago, by nipkow
More lemmas.
23 months ago, by haftmann
Some more proofs.
23 months ago, by haftmann
a few new theorems
23 months ago, by paulson
tuned;
23 months ago, by wenzelm
clarified while-loops;
23 months ago, by wenzelm
updated to postgresql-42.4.0;
23 months ago, by wenzelm
updated to flatlaf-2.4;
23 months ago, by wenzelm
updated to pdfjs-2.14.305;
23 months ago, by wenzelm
more robust: retain Classpath value;
23 months ago, by wenzelm
tuned;
23 months ago, by wenzelm
mor robust;
23 months ago, by wenzelm
clarified modules;
23 months ago, by wenzelm
clarified signature;
23 months ago, by wenzelm
update documentation, following 21c1f82e7f5d;
23 months ago, by wenzelm
proper classpath for Scala compiler invocation (amending 14e22b525b13);
23 months ago, by wenzelm
merged
23 months ago, by wenzelm
support for dynamic classpath from exports;
23 months ago, by wenzelm
clarified signature;
23 months ago, by wenzelm
tuned signature;
23 months ago, by wenzelm
Avoid shadowing original List._ namespace.
23 months ago, by haftmann
replaced complicated lemma by a simpler one
23 months ago, by nipkow
clarified signature;
23 months ago, by wenzelm
clarified modules;
23 months ago, by wenzelm
merged
23 months ago, by wenzelm
more documentation;
23 months ago, by wenzelm
tuned;
23 months ago, by wenzelm
removed obsolete commands;
23 months ago, by wenzelm
command 'scala_build_generated_files' with proper management of source dependencies;
23 months ago, by wenzelm
clarified signature;
23 months ago, by wenzelm
tuned messages;
23 months ago, by wenzelm
support more file types;
23 months ago, by wenzelm
support for Java language;
23 months ago, by wenzelm
clarified signature;
24 months ago, by wenzelm
clarified signature;
24 months ago, by wenzelm
support for classpath artifacts within session structure:
24 months ago, by wenzelm
clarified names;
24 months ago, by wenzelm
clarified signature;
24 months ago, by wenzelm
clarified signature;
24 months ago, by wenzelm
clarified signature;
24 months ago, by wenzelm
clarified signature;
24 months ago, by wenzelm
unused;
24 months ago, by wenzelm
clarified signature;
24 months ago, by wenzelm
tuned signature: more explicit types;
24 months ago, by wenzelm
fix document build error
23 months ago, by Lukas Stevens
tuned (some HOL lints, by Yecine Megdiche);
23 months ago, by Fabian Huch
moved lemma fromm AFP
24 months ago, by nipkow
tuned names
24 months ago, by nipkow
refined code equations for characters
24 months ago, by haftmann
prefer non-JNI SAT solvers by default in Nitpick
24 months ago, by blanchet
milder Sledgehammer messages
24 months ago, by blanchet
moved lemmas from AFP
24 months ago, by nipkow
refined code equations for characters
2022-07-09, by haftmann
tuned comments;
2022-07-08, by wenzelm
support for Isabelle/Scala/Java modules in Isabelle/ML;
2022-07-08, by wenzelm
more robust Scala 3 indentation, for the sake of IntelliJ IDEA;
2022-07-08, by wenzelm
clarified signature: read_theory_exports is already ordered;
2022-07-08, by wenzelm
clarified signature;
2022-07-07, by wenzelm
tuned;
2022-07-07, by wenzelm
sketch for word-specific lsb and msb
2022-07-06, by haftmann
switch to Scala 3;
2022-07-05, by wenzelm
minor performance tuning: avoid redundant BigInt construction;
2022-07-06, by wenzelm
added lemmas total_on_trancl and totalp_on_tranclp
2022-07-05, by desharna
Move code lemmas for symbolic computation of bit operations on int to distribution.
2022-07-04, by haftmann
fixed diverging simproc cont_intro
2022-07-05, by desharna
corrections and adjustions for Scala 3
2022-07-04, by haftmann
less
more
|
(0)
-30000
-10000
-3000
-1000
-240
+240
+1000
+3000
tip