isabelle: Graph

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

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
13 months ago, by paulson
build_manager: change colors;
13 months ago, by Fabian Huch
build_manager: display more info;
13 months ago, by Fabian Huch
add tables to web_app;
13 months ago, by Fabian Huch
tuned and clarified;
13 months ago, by Fabian Huch
build_manager: store submitting user;
13 months ago, by Fabian Huch
build_manager: terminate processes if cancelling does not work;
13 months ago, by Fabian Huch
build_manager: log message when job is cancelled;
13 months ago, by Fabian Huch
branches of case expressions may need to be eta-expanded
13 months ago, by nipkow
tuned;
13 months ago, by wenzelm
tuned: more antiquotations;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
tuned: more standard Isabelle/ML;
13 months ago, by wenzelm
clarified signature: prefer local context;
13 months ago, by wenzelm
tuned: more antiquotations;
13 months ago, by wenzelm
tuned: more explicit dest_Const_name and dest_Const_type;
13 months ago, by wenzelm
tuned signature: more operations;
13 months ago, by wenzelm
tuned: more explicit dest_Type_name and dest_Type_args;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
tuned signature: more operations;
13 months ago, by wenzelm
tuned: more antiquotations;
13 months ago, by wenzelm
got rid of references to system-generated names
13 months ago, by nipkow
tuned names
13 months ago, by nipkow
tuned names
13 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