Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-480
+480
+1000
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.
lsp: added State and Dynamic Output html_output and margin handling;
17 months ago, by Thomas Lindae
lsp: added vscode_html_output option;
17 months ago, by Thomas Lindae
tuned formatting;
17 months ago, by Thomas Lindae
lsp: partially revert c0388fbd8096 to get decorations for all keywords;
17 months ago, by Thomas Lindae
lsp: added State_Init_Response message;
17 months ago, by Thomas Lindae
lsp: removed change_document normalization because it causes desyncs;
16 months ago, by Thomas Lindae
clarified inner-syntax markup, notably for enumerations: prefer "notation=mixfix" over "entity" via 'syntax_consts' (see also 70076ba563d2);
12 months ago, by wenzelm
less markup: prefer "notatation" over "entity";
12 months ago, by wenzelm
clarify comparison of output: ignore token positions, which are somewhat accidental;
12 months ago, by wenzelm
clarified order of markup: more uniform input vs. output;
12 months ago, by wenzelm
misc tuning;
12 months ago, by wenzelm
clarified parse tree: always provide root node;
12 months ago, by wenzelm
tuned signature;
12 months ago, by wenzelm
tuned markup;
12 months ago, by wenzelm
clarified markup: avoid conflict of "notation" with "entity", e.g. in "[x,y,z]" without spaces;
12 months ago, by wenzelm
more flexible command syntax;
12 months ago, by wenzelm
less markup (amending 07ad0b407d38): const = "" is mainly for parentheses syntax -- avoid entity_markup here;
12 months ago, by wenzelm
more markup reports: notably "notation=..." within pretty blocks;
12 months ago, by wenzelm
more parse tree positions;
12 months ago, by wenzelm
more operations;
12 months ago, by wenzelm
clarified order for 'print_syntax' command;
12 months ago, by wenzelm
more accurate parse tree: retain all tokens (and thus positions);
12 months ago, by wenzelm
more thorough markup reports (amending 0c6a600c8939 and 7f9e8516ca05): descend into vacuous nodes;
12 months ago, by wenzelm
clarified comparison: prefer authentic nonterminal context, instead of somewhat accidental "const";
12 months ago, by wenzelm
more detailed parse tree: retain nonterminal context as well;
12 months ago, by wenzelm
clarified persistent data;
12 months ago, by wenzelm
clarified input and output: support markup blocks via Bg/En;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
more operations;
12 months ago, by wenzelm
clarified output: count Tip entries;
12 months ago, by wenzelm
tuned signature;
12 months ago, by wenzelm
tuned whitespace;
12 months ago, by wenzelm
clarified signature: more explicit type "output";
12 months ago, by wenzelm
clarified signature;
12 months ago, by wenzelm
tuned: more uniform;
12 months ago, by wenzelm
tuned: more uniform;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
minor performance tuning;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
minor performance tuning;
12 months ago, by wenzelm
partial revert of d97fdabd9e2b, to build old documentation more reliably;
12 months ago, by wenzelm
tuned signature;
12 months ago, by wenzelm
tuned signature;
12 months ago, by wenzelm
tuned signature;
12 months ago, by wenzelm
clarified signature;
12 months ago, by wenzelm
minor performance tuning: proper table for parsetree list;
12 months ago, by wenzelm
unused (see 954e9d6782ea);
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
unused (see 7c1e73540990);
12 months ago, by wenzelm
minor performance tuning (NB: order of prods / states does not matter);
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
tuned comments;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
pro-forma support for markup blocks, without any change of result yet;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
merged
12 months ago, by wenzelm
proper 'no_syntax' declarations (amending 8e72f55295fd);
12 months ago, by wenzelm
tuned, following make_symbs in src/Pure/Syntax/printer.ML;
12 months ago, by wenzelm
clarified use of Lexicon.dummy;
12 months ago, by wenzelm
unused (see 584828fa7a97);
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
tuned: prefer ML over prose;
12 months ago, by wenzelm
eliminated redundant nt_count: rely on Symtab.size;
12 months ago, by wenzelm
eliminate unused prod_count (see also 7afca3218b65);
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
more markup;
12 months ago, by wenzelm
minor performance tuning: prefer static values;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
more markup;
12 months ago, by wenzelm
clarified persistent datatype: more direct literal_markup, which also serves as a flag;
12 months ago, by wenzelm
tuned signature;
12 months ago, by wenzelm
clarified signature;
12 months ago, by wenzelm
add comments to rendering, e.g. to collect them from build database;
13 months ago, by Fabian Huch
To tiny but maybe useful lemmas (moved in from the AFP, Word_Lib)
12 months ago, by paulson
tuned;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
minor performance tuning for blocks without markup;
12 months ago, by wenzelm
more markup <expression kind="item"> in Isabelle/Scala, with pro-forma Markup_Kind.setup in Isabelle/ML;
12 months ago, by wenzelm
clarified signature;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
minor performance tuning: more direct blocks without markup;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
tuned signature;
12 months ago, by wenzelm
proper 'no_syntax' (amending 8e72f55295fd);
12 months ago, by wenzelm
more inner syntax markup: HOL;
12 months ago, by wenzelm
misc tuning and clarification;
12 months ago, by wenzelm
standardize mixfix annotations via "isabelle update -u mixfix_cartouches -l Pure HOL" --- to simplify systematic editing;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
minor performance tuning: more concise tuples;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
misc tuning and clarification;
12 months ago, by wenzelm
more antiquotations;
12 months ago, by wenzelm
tuned comments;
12 months ago, by wenzelm
more specific markup for "judgment";
12 months ago, by wenzelm
remove specific support for "expression" block markup: prefer "notation";
12 months ago, by wenzelm
clarified inner syntax markup: use "notation" uniformly;
12 months ago, by wenzelm
more uniform treatment of Markup.notation and Markup.expression: manage kinds via context;
12 months ago, by wenzelm
clarified modules and signature;
12 months ago, by wenzelm
proper fbreaks (amending 53f12ab896e6);
12 months ago, by wenzelm
more inner syntax markup: minor object-logics;
12 months ago, by wenzelm
more inner syntax markup: Pure;
12 months ago, by wenzelm
more markup elements;
12 months ago, by wenzelm
standardize mixfix annotations via "isabelle update -a -u mixfix_cartouches" --- to simplify systematic editing;
12 months ago, by wenzelm
proper Haskell setup, following 406a85a25189;
12 months ago, by wenzelm
support more markup elements;
12 months ago, by wenzelm
block markup for specific notation, notably infix and binder;
12 months ago, by wenzelm
clarified signature: more explicit operations;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
no need to suppress positions (see ff3b8e4079bd) thanks to Context_Position.set_visible false (see 5328d67ec647);
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
support for Markup.expression properties in pretty-blocks;
12 months ago, by wenzelm
more positions;
12 months ago, by wenzelm
more operations;
12 months ago, by wenzelm
more operations;
12 months ago, by wenzelm
minor performance tuning: avoid vacuous update of context;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
proper Context_Position.report, following 5328d67ec647;
12 months ago, by wenzelm
more operations;
12 months ago, by wenzelm
more explicit context for syn_ext/mixfix operations, but it often degenerates to background theory;
12 months ago, by wenzelm
obsolete --- superseded by Local_Theory.syntax_cmd;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
unused (see 39261908e12f);
12 months ago, by wenzelm
clarified signature;
12 months ago, by wenzelm
tuned comments;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
more detailed markup;
12 months ago, by wenzelm
more formal Markup.expression;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
clarified name space: no theory qualifier here --- treat like global datatype constructors;
12 months ago, by wenzelm
discontinued "isabelle build -k": superseded by admin-tool "isabelle check_keywords";
12 months ago, by wenzelm
clarified signature;
12 months ago, by wenzelm
tuned signature;
12 months ago, by wenzelm
obsolete (see also b93cc7d73431);
12 months ago, by wenzelm
performance tuning: cache for highly redundant markup (types and sorts);
12 months ago, by wenzelm
more operations;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
tuned signature and module structure;
12 months ago, by wenzelm
less ambitious Bytes.chunk_size for potentially more stable Poly/ML GC (see f0d8f659b19a, but also java.io.InputStream.DEFAULT_BUFFER_SIZE);
12 months ago, by wenzelm
tuned signature: more operations;
12 months ago, by wenzelm
clarified signature;
12 months ago, by wenzelm
prefer Pretty.pure_string_of to produce output without markup, instead of cleaning output afterwards;
12 months ago, by wenzelm
clarified signature: more explicit operations;
12 months ago, by wenzelm
tuned: trim message before formatting;
12 months ago, by wenzelm
tuned signature: more operations;
12 months ago, by wenzelm
clarified signature;
12 months ago, by wenzelm
clarified print_mode (again, amending 9de19e3a7231): support e.g. 'thm ("") symmetric' for formatting in ML and without markup;
12 months ago, by wenzelm
more robust reports: ensure that markup is actually present;
12 months ago, by wenzelm
tuned signature;
12 months ago, by wenzelm
clarified internal tool output: prefer Pretty.pure_string_of over manipulation of print_mode;
12 months ago, by wenzelm
unused;
12 months ago, by wenzelm
misc tuning and clarification (see also 86a31308a8e1);
12 months ago, by wenzelm
tuned signature: more operations;
12 months ago, by wenzelm
clarified modules;
12 months ago, by wenzelm
dismantle print_mode operations for Markup/Pretty: hardwired check of "print_mode_active Print_Mode.PIDE";
12 months ago, by wenzelm
clarified YXML bootstrap;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
more robust: global ML name space for markup elements;
12 months ago, by wenzelm
clarified properties;
12 months ago, by wenzelm
clarified signature and modules;
12 months ago, by wenzelm
further clarification of print_mode: PIDE markup depends on "isabelle_process" alone, Latex is stateless;
12 months ago, by wenzelm
misc tuning and clarification;
12 months ago, by wenzelm
minor performance tuning, notably for Bytes.add (e.g. YXML output);
12 months ago, by wenzelm
revert 90f6e541e926, which has become pointless thanks to df85df6315af;
12 months ago, by wenzelm
clarified signature and modules;
12 months ago, by wenzelm
clarified files;
12 months ago, by wenzelm
drop pointless print_mode operations Output.output / Output.escape;
12 months ago, by wenzelm
clarified signature: prefer explicit type Bytes.T;
12 months ago, by wenzelm
clarified signature, roughly following Isabelle/Scala;
12 months ago, by wenzelm
clarified print mode "latex": no longer impact Output/Markup/Pretty operations;
12 months ago, by wenzelm
tuned comments, following Isabelle/ML;
12 months ago, by wenzelm
tuned module structure;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
clarified unbreakable latex output: Pretty.unformatted and (Pretty.string_of o Pretty.unbreakable) should coincide, but are produced by quite different means;
12 months ago, by wenzelm
clarified signature;
12 months ago, by wenzelm
tuned signature;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
minor performance tuning, following Isabelle/Scala;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
tuned signature;
12 months ago, by wenzelm
more scalable;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
eliminate print mode "code_presentation" thanks to value-oriented Pretty.T operations;
12 months ago, by wenzelm
NEWS: value-oriented Pretty.T;
12 months ago, by wenzelm
proper formal sections;
12 months ago, by wenzelm
tuned signature: more options;
12 months ago, by wenzelm
clarified Pretty.markup_block: use value-oriented YXML.output_markup, with final re-interpretation via print_mode in output_tree;
12 months ago, by wenzelm
minor performance tuning;
12 months ago, by wenzelm
unused;
12 months ago, by wenzelm
prefer static YXML.output_markup_only (without print_mode): Output.status is only relevant for PIDE (with print_mode "isabelle_process");
12 months ago, by wenzelm
clarified signature: more explicit type output_ops: default via print_mode;
12 months ago, by wenzelm
discontinued unused global variable (see also following bf465f335e85);
12 months ago, by wenzelm
tuned signature;
12 months ago, by wenzelm
clarified modules (see also ea7c2ee8a47a);
12 months ago, by wenzelm
clarified signature: more explicit type "ops";
12 months ago, by wenzelm
more thorough Protocol_Message.clean_output, following Isabelle/Scala;
12 months ago, by wenzelm
more accurate output, following 3f02bc5a5a03;
12 months ago, by wenzelm
clarified signature;
12 months ago, by wenzelm
clarified signature;
12 months ago, by wenzelm
misc tuning and clarification;
12 months ago, by wenzelm
proper signature (amending 0f820da558f9);
12 months ago, by wenzelm
more accurate output: observe depth as in "prune" operation;
12 months ago, by wenzelm
clarified signature, following 1f718be3608b: Pretty.str is now value-oriented;
12 months ago, by wenzelm
clarified signature and modules;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
clarified Pretty.T vs. output tree (following Isabelle/Scala): Output.output_width (via print_mode) happens during formatting, instead of construction;
12 months ago, by wenzelm
clarified signature: type ML_Pretty.pretty coincides with PolyML.pretty;
12 months ago, by wenzelm
clarified signature (see also 8bef51521f21);
13 months ago, by wenzelm
tuned signature;
13 months ago, by wenzelm
more accurate Default_Metric;
13 months ago, by wenzelm
tuned signature;
13 months ago, by wenzelm
clarified output_spaces, based on Output.output_width;
13 months ago, by wenzelm
clarified modules: enable pretty.ML to use XML/YXML more directly;
13 months ago, by wenzelm
removed unused operation (reverting 4660b0409096);
13 months ago, by wenzelm
clarified modules;
13 months ago, by wenzelm
clarified signature;
13 months ago, by wenzelm
tuned: prefer Symbol.spaces;
13 months ago, by wenzelm
tuned whitespace;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
more NEWS;
13 months ago, by wenzelm
proper string syntax (amending 70076ba563d2);
13 months ago, by wenzelm
avoid redundant XML.blob: Bytes.contents consist of larger chunks;
13 months ago, by wenzelm
minor performance tuning: avoid many small strings, notably in File_Stream.output;
13 months ago, by wenzelm
A bit of tidying
13 months ago, by paulson
merged
13 months ago, by paulson
More tidying of old proofs
13 months ago, by paulson
more scalable pretty printing: avoid exception String.Size at command "value" (line 33 of "$AFP/Iptables_Semantics/Examples/SQRL_Shorewall/Analyze_SQRL_Shorewall.thy") in AFP/c69af9cd3390;
13 months ago, by wenzelm
more specific "args" syntax, to support more markup for syntax consts;
13 months ago, by wenzelm
more direct notation;
13 months ago, by wenzelm
more specific "args" syntax, to support more markup for syntax consts;
13 months ago, by wenzelm
proper definition to avoid failure of HOL-Codegenerator_Test (amending 3d9e7746d9db);
13 months ago, by wenzelm
further attempts at markup for monad notation;
13 months ago, by wenzelm
more markup for syntax consts;
13 months ago, by wenzelm
stop web server on close;
13 months ago, by Fabian Huch
better results for terminated jobs;
13 months ago, by Fabian Huch
more robust: clean up unfinished jobs on init, e.g. if build_manager process was forcefully terminated;
13 months ago, by Fabian Huch
manage runner state properly (amending be4c1fbccfe8);
13 months ago, by Fabian Huch
merged
13 months ago, by paulson
More tidying of old proofs
13 months ago, by paulson
more precise bound
13 months ago, by nipkow
merged
13 months ago, by nipkow
get rid of manual T_f defs
13 months ago, by nipkow
NEWS and documentation;
13 months ago, by wenzelm
merged
13 months ago, by wenzelm
use nicer notation, following 783406dd051e;
13 months ago, by wenzelm
merged
13 months ago, by paulson
A bit more tidying
13 months ago, by paulson
more markup for syntax consts;
13 months ago, by wenzelm
clarified Syntax.is_const (after 43c4817375bf): exclude logical consts from 'syntax_consts' / 'syntax_types', e.g. relevant for @{syntax_const} antiquotation;
13 months ago, by wenzelm
use nicer notation, following 783406dd051e;
13 months ago, by wenzelm
proper translation for "_qprod", following "_qsum" (see also e14b89d6ef13 and fa7d27ef7e59);
13 months ago, by wenzelm
tuned: prefer notation for Pure.type;
13 months ago, by wenzelm
tuned whitespace;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
tuned, following be8c0e039a5e;
13 months ago, by wenzelm
more markup for syntax consts;
13 months ago, by wenzelm
proper flags (amending 1319c729c65d): abbrevs are allowed, free variables are disallowed;
13 months ago, by wenzelm
Some tidying
13 months ago, by paulson
merged
13 months ago, by paulson
Tidied some messy old proofs
13 months ago, by paulson
merged
13 months ago, by wenzelm
more markup for syntax consts;
13 months ago, by wenzelm
more markup for syntax consts;
13 months ago, by wenzelm
clarified concrete syntax;
13 months ago, by wenzelm
more accurate markup (amending 43c4817375bf): only consider primitive syntax consts, avoid extra Markup.intensify e.g. due to "\<^const>Pure.all_binder";
13 months ago, by wenzelm
more concrete syntax and more checks;
13 months ago, by wenzelm
clarified signature: more operations;
13 months ago, by wenzelm
support for syntax const dependencies, with minimal integrity checks;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
clarified markup: more uniform treatment of parse/print phase;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
clarified markup: more uniform;
13 months ago, by wenzelm
tuned signature: separate markup vs. extern;
13 months ago, by wenzelm
clarified signature;
13 months ago, by wenzelm
tuned: prefer configuration options via context;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
tuned signature: more operations;
13 months ago, by wenzelm
tuned comments
13 months ago, by nipkow
merged
13 months ago, by paulson
Partial tidying of old proofs
13 months ago, by paulson
merged
13 months ago, by nipkow
new version of time_fun that works for classes; define T_length automatically now
13 months ago, by nipkow
merged
13 months ago, by paulson
revised/generalised some lemmas
13 months ago, by paulson
remove terminated jobs, even if futures do not complete;
13 months ago, by Fabian Huch
terminate jobs properly;
13 months ago, by Fabian Huch
clarified signature: eliminate clones;
13 months ago, by wenzelm
tuned: more antiquotations;
13 months ago, by wenzelm
tuned: more antiquotations;
13 months ago, by wenzelm
misc tuning;
13 months ago, by wenzelm
tuned: eliminate clone (with change of internal exceptions);
13 months ago, by wenzelm
tuned: more antiquotations;
13 months ago, by wenzelm
tuned comments and whitespace (see also 589645894305);
13 months ago, by wenzelm
tuned: more antiquotations;
13 months ago, by wenzelm
tuned: more antiquotations;
13 months ago, by wenzelm
proper const (see also 759bffe1d416 and b2800da9eb8a);
13 months ago, by wenzelm
tuned: inline constants;
13 months ago, by wenzelm
tuned: eliminate clone;
13 months ago, by wenzelm
tuned: more antiquotations;
13 months ago, by wenzelm
prefer host that is less likely to be down;
13 months ago, by wenzelm
adapt and activate congprocs examples, following the current Simplifier implementation;
13 months ago, by wenzelm
original Congproc_Ex.thy by Norbert Schirmer: still inactive;
13 months ago, by wenzelm
provide Simplifier.set_mksimps_context (roughly following Norbert Schirmer): allow update of context when premises are added to the local simpset;
13 months ago, by wenzelm
clarified signature;
13 months ago, by wenzelm
more direct access to Simplifier.mk_cong, to avoid odd Simpdata.mk_meta_cong seen in the wild;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
support for congprocs in the Simplifier, closely following Norbert Schirmer et-al, but with only one "simproc" name space and "simproc_setup" command / ML antiquotation;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
tuned: anticipate congprocs;
13 months ago, by wenzelm
clarified signature;
13 months ago, by wenzelm
tuned signature (again): anticipate different kinds of procs;
13 months ago, by wenzelm
clarified context data;
13 months ago, by wenzelm
tuned: prefer canonical argument order;
13 months ago, by wenzelm
tuned: more antiquotations;
13 months ago, by wenzelm
tuned: prefer canonical argument order;
13 months ago, by wenzelm
clarified signature: less redundant types;
13 months ago, by wenzelm
clarified signature;
13 months ago, by wenzelm
unused (see d12c58e12c51);
13 months ago, by wenzelm
tuned signature: support more general procedures;
13 months ago, by wenzelm
merged
13 months ago, by wenzelm
tuned: more antiquotations;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
tuned: more antiquotations;
13 months ago, by wenzelm
tuned whitespace;
13 months ago, by wenzelm
more robust (amending 8f53fa93d5f0): R could be anything and Thm.instantiate' involves some type-checks, e.g. relevant for lemma fset_simps in theory Quotient_Examples.Quotient_FSet;
13 months ago, by wenzelm
tuned modules;
13 months ago, by wenzelm
misc tuning;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
tuned: more antiquotations;
13 months ago, by wenzelm
misc tuning;
13 months ago, by wenzelm
misc tuning and clarification;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
misc tuning and clarification: proper context, proper exception;
13 months ago, by wenzelm
tuned: eliminate odd clones;
13 months ago, by wenzelm
tuned: more antiquotations;
13 months ago, by wenzelm
unused;
13 months ago, by wenzelm
tuned: more antiquotations;
13 months ago, by wenzelm
tuned: more antiquotations;
13 months ago, by wenzelm
tuned: more antiquotations;
13 months ago, by wenzelm
tuned proofs;
13 months ago, by wenzelm
tuned signature: more operations;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
tuned: more antiquotations;
13 months ago, by wenzelm
clarified signature;
13 months ago, by wenzelm
Two little lemmas
13 months ago, by paulson
merged
13 months ago, by wenzelm
more uniform Type_Infer_Context.infer_types_finished, despite subtle differences of Type_Infer.fixate vs. Proof_Context.standard_term_check_finish;
13 months ago, by wenzelm
tuned, following cdae621613da;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
more robust: only type inference with its finish/fixate phase (on contrast to dc387e3999ec), e.g. avoid accidental "improvement" of type class operations (free vs. const);
13 months ago, by wenzelm
tuned: more antiquotations;
13 months ago, by wenzelm
tuned: more abstract access to datatype typ;
13 months ago, by wenzelm
tuned (see also db120661dded);
13 months ago, by wenzelm
tuned: more antiquotations;
13 months ago, by wenzelm
tuned signature: eliminate aliases;
13 months ago, by wenzelm
removed odd clone (amending 100c0eaf63d5);
13 months ago, by wenzelm
clarified: more robust (dest_Type_name o body_type), which may fail in both parts;
13 months ago, by wenzelm
tuned: more antiquotations, more abstract access to datatype typ;
13 months ago, by wenzelm
recover lost update (see 11b8f2e4c3d2 and 4041e7c8059d);
13 months ago, by wenzelm
prefer host that is less likely to be down;
13 months ago, by wenzelm
tuned: more antiquotations, avoid re-certification;
13 months ago, by wenzelm
Rearranged a couple of theorems
13 months ago, by paulson
New library material; also fixed the spelling error powr_ge_pzero -> powr_ge_zero
13 months ago, by paulson
merged
13 months ago, by paulson
tidied more apply proofs
14 months ago, by paulson
build_manager: change colors;
13 months ago, by Fabian Huch
build_manager: display more info;
14 months ago, by Fabian Huch
add tables to web_app;
14 months ago, by Fabian Huch
tuned and clarified;
14 months ago, by Fabian Huch
build_manager: store submitting user;
14 months ago, by Fabian Huch
build_manager: terminate processes if cancelling does not work;
14 months ago, by Fabian Huch
build_manager: log message when job is cancelled;
14 months ago, by Fabian Huch
branches of case expressions may need to be eta-expanded
14 months ago, by nipkow
tuned;
14 months ago, by wenzelm
tuned: more antiquotations;
14 months ago, by wenzelm
tuned;
14 months ago, by wenzelm
tuned: more standard Isabelle/ML;
14 months ago, by wenzelm
clarified signature: prefer local context;
14 months ago, by wenzelm
tuned: more antiquotations;
14 months ago, by wenzelm
tuned: more explicit dest_Const_name and dest_Const_type;
14 months ago, by wenzelm
tuned signature: more operations;
14 months ago, by wenzelm
tuned: more explicit dest_Type_name and dest_Type_args;
14 months ago, by wenzelm
tuned;
14 months ago, by wenzelm
tuned signature: more operations;
14 months ago, by wenzelm
tuned: more antiquotations;
14 months ago, by wenzelm
got rid of references to system-generated names
14 months ago, by nipkow
tuned names
14 months ago, by nipkow
tuned names
14 months ago, by nipkow
merged
14 months ago, by paulson
Reversed my brain-dead stupid change to divide_left_mono and divide_left_mono_neg
14 months ago, by paulson
merged
14 months ago, by nipkow
time_function T_map can now be generated automatically.
14 months ago, by nipkow
Further divide_mono fixes
14 months ago, by paulson
Fix for simplified divide_mono theorem
14 months ago, by paulson
Migration of new material mostly about exp, ln
14 months ago, by paulson
More simplification of a nominal example
14 months ago, by paulson
merged
14 months ago, by paulson
More simplification of apply proofs
14 months ago, by paulson
less ambitious parallelism: avoid exhaustion of memory (64GB total);
14 months ago, by wenzelm
tuned names;
14 months ago, by wenzelm
merged
14 months ago, by paulson
Adjusting the precedences to reduce syntactic ambiguity
14 months ago, by paulson
disable thy_cache for now (amending 0b8922e351a3): avoid crash of AFP/Ramsey-Infinite due to exception THEORY "Duplicate theory name";
14 months ago, by wenzelm
A lot of new material from the Ramsey development, including a couple of new simprules.
14 months ago, by paulson
A massive reduction of some truly horrible proofs
14 months ago, by paulson
merged
14 months ago, by paulson
More simplification of proofs. Trying to fix the syntax too
14 months ago, by paulson
clarified export: replaced Proofterm.standard_vars by ZTerm.standard_vars;
14 months ago, by wenzelm
tuned;
14 months ago, by wenzelm
clarified order of operations: no_thm_names first;
14 months ago, by wenzelm
more operations;
14 months ago, by wenzelm
tuned;
14 months ago, by wenzelm
more operations;
14 months ago, by wenzelm
more operations;
14 months ago, by wenzelm
clarified signature: more robust operations;
14 months ago, by wenzelm
merged
14 months ago, by wenzelm
clarified modules (see also e063c0403650);
14 months ago, by wenzelm
more operations;
14 months ago, by wenzelm
tuned;
14 months ago, by wenzelm
tuned: more direct Name.context for bounds;
14 months ago, by wenzelm
Got rid of another 250 apply-lines
14 months ago, by paulson
merged
14 months ago, by paulson
more proof tidying
14 months ago, by paulson
more predictable proof id;
14 months ago, by wenzelm
more conservative cache: retain concurrent value;
14 months ago, by wenzelm
clarified thm_header command_pos vs. thm_pos;
14 months ago, by wenzelm
clarified signature, following zterm.ML;
14 months ago, by wenzelm
tuned whitespace;
14 months ago, by wenzelm
merged
14 months ago, by wenzelm
uniform export via ztyp/zterm/zproof;
14 months ago, by wenzelm
clarified signature;
14 months ago, by wenzelm
tuned;
14 months ago, by wenzelm
more operations;
14 months ago, by wenzelm
clarified scope of cache: avoid nested typ_cache;
14 months ago, by wenzelm
clarified scope of cache: per theory body;
14 months ago, by wenzelm
tuned module structure;
14 months ago, by wenzelm
clarified signature: more operations;
14 months ago, by wenzelm
merged
14 months ago, by nipkow
tuned
14 months ago, by nipkow
added nicer proof
14 months ago, by nipkow
better poller: don't start job when same version is already running;
14 months ago, by Fabian Huch
clarified: more uniform;
14 months ago, by Fabian Huch
merged
14 months ago, by desharna
added lemmas wfp_on_antimono_stronger and wf_on_antimono_stronger
14 months ago, by desharna
More streamlining
14 months ago, by paulson
merged
14 months ago, by paulson
Revised mixfix and streamlined proofs
14 months ago, by paulson
clarified Isabelle/Haskell type Term, following Isabelle/Scala (see 446b887e23c7);
14 months ago, by wenzelm
tuned output, following Isabelle/Scala;
14 months ago, by wenzelm
clarified data representation: prefer explicit OFCLASS constructor, following datatype zterm;
14 months ago, by wenzelm
clarified signature, following Isabelle/Scala;
14 months ago, by wenzelm
afford larger example (see also ccf9241af217);
14 months ago, by wenzelm
more scalable operations;
14 months ago, by wenzelm
tuned;
14 months ago, by wenzelm
tuned (see also 4879d0021185);
14 months ago, by wenzelm
tuned signature;
14 months ago, by wenzelm
merged
14 months ago, by wenzelm
clarified signature: afford explicit Scala data types;
14 months ago, by wenzelm
tuned signature;
14 months ago, by wenzelm
tuned signature (again);
14 months ago, by wenzelm
clarified signature: more self-contained paint_chunk_list;
14 months ago, by wenzelm
clarified signature: more arguments;
14 months ago, by wenzelm
tuned;
14 months ago, by wenzelm
clarified popup layer (not relevant yet);
14 months ago, by wenzelm
clarified signature;
14 months ago, by wenzelm
misc tuning and clarification;
14 months ago, by wenzelm
tuned;
14 months ago, by wenzelm
tuned signature;
14 months ago, by wenzelm
tuned website;
14 months ago, by Fabian Huch
proper parse (amending dd86d35375a7);
14 months ago, by Fabian Huch
less
more
|
(0)
-30000
-10000
-3000
-1000
-480
+480
+1000
tip