isabelle: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -120 +120 tip

more correct lemma name
2 months ago, by haftmann
merged
2 months ago, by desharna
added basic support for persistent prover data to Sledgehammer
2 months ago, by desharna
merged
2 months ago, by wenzelm
tuned comments;
2 months ago, by wenzelm
tuned messages;
2 months ago, by wenzelm
clarified signature: more explicit type Bires.kind;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
proper weight, instead of magic number 1000000 (see b3f190995bc9);
2 months ago, by wenzelm
just one type Bires.netpair, based on Bires.tag with explicit weight;
2 months ago, by wenzelm
misc tuning and clarification;
2 months ago, by wenzelm
tuned signature: do not expose private operation;
2 months ago, by wenzelm
minor performance tuning;
2 months ago, by wenzelm
clarified modules;
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
tuned signature: more explicit types;
2 months ago, by wenzelm
clarified modules: explicit structure Bires;
2 months ago, by wenzelm
minor performance tuning;
3 months ago, by wenzelm
Two lemmas and a comment
2 months ago, by paulson
removed duplicate lemma; added the notion of the kernel of a function
3 months ago, by nipkow
isabelle regenerate_cooper
3 months ago, by haftmann
NEWS;
3 months ago, by wenzelm
obsolete (see 09904d5ef1f0);
3 months ago, by wenzelm
inline errors as "bad" markup;
3 months ago, by wenzelm
more robust result of migrate_file: retain full src_path (in contrast to d5d0e36eda16);
3 months ago, by wenzelm
clarified signature: more explicit operations;
3 months ago, by wenzelm
more robust: avoid crash on session database errors;
3 months ago, by wenzelm
tuned signature: more operations;
3 months ago, by wenzelm
basic support to reload theory markup from session store;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
eliminate odd workaround from Aug-2012 (see 393a37003851);
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
tuned signature;
3 months ago, by wenzelm
clarified signature: avoid Session with accidental Resources.bootstrap, which is mostly undefined;
3 months ago, by wenzelm
clarified signature: prefer private operation (see also 803731b62180);
3 months ago, by wenzelm
tuned (see also 5c7652e9bc01);
3 months ago, by wenzelm
tuned signature: more generic operations;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
clarified signature: omit pointless object-oriented indirection;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
tuned: avoid overlapping scopes;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
typo
3 months ago, by haftmann
append (rather than prepend) code equations: the order within a theory is maintained in the resulting code
3 months ago, by haftmann
scope pending code equations to theories
3 months ago, by haftmann
merged
3 months ago, by nipkow
tuned
3 months ago, by nipkow
enforce rebuild of Isabelle/ML;
3 months ago, by wenzelm
proper build_context.store, instead of circular null value (amending 0e36478a1b6a and e891ff63e6db);
3 months ago, by wenzelm
merged
3 months ago, by wenzelm
more operations (e.g. for testing);
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
tuned signature: more explicit operations;
3 months ago, by wenzelm
more accurate ML_Settings from underlying Session;
3 months ago, by wenzelm
more accurate ML_Settings from underlying Session;
3 months ago, by wenzelm
tuned signature;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
more robust session startup, notably Isabelle/jEdit with session build (amending 0e36478a1b6a);
3 months ago, by wenzelm
clarified signature: more accurate ML_Settings;
3 months ago, by wenzelm
clarified modules;
3 months ago, by wenzelm
clarified signature: avoid duplicate ML_Settings.system;
3 months ago, by wenzelm
clarified signature: general Session.open_session_context;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
clarified modules;
3 months ago, by wenzelm
more uniform options for session build/start (coincides with PIDE.options.value initially);
3 months ago, by wenzelm
clarified signature: Session always provides Store (with Rich_Text.Cache);
3 months ago, by wenzelm
clarified signature: prefer implicit PIDE.options, which correspond to PIDE.session;
3 months ago, by wenzelm
clarified modules;
3 months ago, by wenzelm
tuned signature;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
clarified signature: more explicit subtypes of Session, with corresponding subtypes of Resources;
3 months ago, by wenzelm
re-use cache from Main_Plugin.start;
3 months ago, by wenzelm
clarified signature, following c3793899b880;
3 months ago, by wenzelm
more robust: assertion holds, because session.finished_theories provides Snapshot from Document.State.end_theory;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
tuned comments;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
added lemmas
3 months ago, by nipkow
added lemmas
3 months ago, by nipkow
treat map_filter similar to list_all, list_ex, list_ex1
3 months ago, by haftmann
reinstated intersection of lists as inter_list_set
3 months ago, by nipkow
merged
3 months ago, by nipkow
defined mset in terms of its list-versin count_list instead of the ugly length of filter.
3 months ago, by nipkow
more explicit theorem names for list quantifiers
3 months ago, by haftmann
support for explicit ML platform identifier;
3 months ago, by wenzelm
more robust;
3 months ago, by wenzelm
proper SSH operation (amending 956ecf2c07a0);
3 months ago, by wenzelm
more robust;
3 months ago, by wenzelm
tuned errors;
3 months ago, by wenzelm
merged
3 months ago, by wenzelm
tuned message;
3 months ago, by wenzelm
more NEWS;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
more flexible ML_Settings in Isabelle/Scala, depending on system options and some default settings;
3 months ago, by wenzelm
support dynamic usage_text, after some options have been processed already;
3 months ago, by wenzelm
clarified signature: more modular, avoid adhoc mixins;
3 months ago, by wenzelm
tuned signature: more operations;
3 months ago, by wenzelm
clarified signature: more explicit types;
3 months ago, by wenzelm
proper support for old versions before 0e41f26a0250;
3 months ago, by wenzelm
tuned whitespace;
3 months ago, by wenzelm
proper Java command-line for desktop application (amending a3e7732b0393);
3 months ago, by wenzelm
more robust: inspect true ML environment instead of reconstructing it externally;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
discontinue unused parameter (better done as system option);
3 months ago, by wenzelm
discontinued ML_IDENTIFIER settings variable;
3 months ago, by wenzelm
clarified modules;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
removed pointless leftovers
3 months ago, by nipkow
more minus_list lemmas (incl code via fold instead of foldr)
3 months ago, by nipkow