Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-64
+64
+100
+300
+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.
tuned names
9 months ago, by nipkow
merged
9 months ago, by paulson
Reversed my brain-dead stupid change to divide_left_mono and divide_left_mono_neg
9 months ago, by paulson
merged
9 months ago, by nipkow
time_function T_map can now be generated automatically.
9 months ago, by nipkow
Further divide_mono fixes
9 months ago, by paulson
Fix for simplified divide_mono theorem
9 months ago, by paulson
Migration of new material mostly about exp, ln
9 months ago, by paulson
More simplification of a nominal example
9 months ago, by paulson
merged
9 months ago, by paulson
More simplification of apply proofs
9 months ago, by paulson
less ambitious parallelism: avoid exhaustion of memory (64GB total);
9 months ago, by wenzelm
tuned names;
9 months ago, by wenzelm
merged
9 months ago, by paulson
Adjusting the precedences to reduce syntactic ambiguity
9 months ago, by paulson
disable thy_cache for now (amending 0b8922e351a3): avoid crash of AFP/Ramsey-Infinite due to exception THEORY "Duplicate theory name";
9 months ago, by wenzelm
A lot of new material from the Ramsey development, including a couple of new simprules.
9 months ago, by paulson
A massive reduction of some truly horrible proofs
9 months ago, by paulson
merged
9 months ago, by paulson
More simplification of proofs. Trying to fix the syntax too
9 months ago, by paulson
clarified export: replaced Proofterm.standard_vars by ZTerm.standard_vars;
9 months ago, by wenzelm
tuned;
9 months ago, by wenzelm
clarified order of operations: no_thm_names first;
9 months ago, by wenzelm
more operations;
9 months ago, by wenzelm
tuned;
9 months ago, by wenzelm
more operations;
9 months ago, by wenzelm
more operations;
9 months ago, by wenzelm
clarified signature: more robust operations;
9 months ago, by wenzelm
merged
9 months ago, by wenzelm
clarified modules (see also e063c0403650);
9 months ago, by wenzelm
more operations;
9 months ago, by wenzelm
tuned;
9 months ago, by wenzelm
tuned: more direct Name.context for bounds;
9 months ago, by wenzelm
Got rid of another 250 apply-lines
9 months ago, by paulson
merged
9 months ago, by paulson
more proof tidying
9 months ago, by paulson
more predictable proof id;
9 months ago, by wenzelm
more conservative cache: retain concurrent value;
9 months ago, by wenzelm
clarified thm_header command_pos vs. thm_pos;
9 months ago, by wenzelm
clarified signature, following zterm.ML;
9 months ago, by wenzelm
tuned whitespace;
9 months ago, by wenzelm
merged
9 months ago, by wenzelm
uniform export via ztyp/zterm/zproof;
9 months ago, by wenzelm
clarified signature;
9 months ago, by wenzelm
tuned;
9 months ago, by wenzelm
more operations;
9 months ago, by wenzelm
clarified scope of cache: avoid nested typ_cache;
9 months ago, by wenzelm
clarified scope of cache: per theory body;
9 months ago, by wenzelm
tuned module structure;
10 months ago, by wenzelm
clarified signature: more operations;
10 months ago, by wenzelm
merged
9 months ago, by nipkow
tuned
9 months ago, by nipkow
added nicer proof
9 months ago, by nipkow
better poller: don't start job when same version is already running;
9 months ago, by Fabian Huch
clarified: more uniform;
9 months ago, by Fabian Huch
merged
9 months ago, by desharna
added lemmas wfp_on_antimono_stronger and wf_on_antimono_stronger
10 months ago, by desharna
More streamlining
10 months ago, by paulson
merged
10 months ago, by paulson
Revised mixfix and streamlined proofs
10 months ago, by paulson
clarified Isabelle/Haskell type Term, following Isabelle/Scala (see 446b887e23c7);
10 months ago, by wenzelm
tuned output, following Isabelle/Scala;
10 months ago, by wenzelm
clarified data representation: prefer explicit OFCLASS constructor, following datatype zterm;
10 months ago, by wenzelm
clarified signature, following Isabelle/Scala;
10 months ago, by wenzelm
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-64
+64
+100
+300
+1000
tip