Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
30000
10000
3000
1000
300
100
60
+60
+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 JavaScriptenabled browsers.
Merge and get rid of closed_segmentI
19 months ago, by paulson
Moved or deleted some out of place material, also eliminating obsolete naming conventions
19 months ago, by paulson
Line_Segment is independent of Convex_Euclidean_Space
19 months ago, by immler
the division between Starlike and Convex_Euclidean_Space is artificial, therefore include Starlike
19 months ago, by immler
betweenness is a property on line segments
19 months ago, by immler
reduce dependencies of Ordered_Euclidean_Space; move more general material from Cartesian_Euclidean_Space
19 months ago, by immler
proper message (amending 94442fce40a5);
19 months ago, by wenzelm
more robust Thm.expose_theory  ensure that PIDE export happens in the proper theory context;
19 months ago, by wenzelm
uniform "prune_proofs" for Thm_Node / PThm, but it is in conflict with export_proofs of reused nodes;
19 months ago, by wenzelm
tuned;
19 months ago, by wenzelm
updated xml_size;
19 months ago, by wenzelm
prefer named result;
19 months ago, by wenzelm
more robust expose_proofs corresponding to register_proofs/consolidate_theory;
19 months ago, by wenzelm
expose derivations more thoroughly, notably for locale/class reasoning;
19 months ago, by wenzelm
clarified errors;
19 months ago, by wenzelm
determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
19 months ago, by wenzelm
more operations;
19 months ago, by wenzelm
tuned whitespace;
19 months ago, by wenzelm
more robust;
19 months ago, by wenzelm
clarified modules;
19 months ago, by wenzelm
clarified signature  more options;
19 months ago, by wenzelm
merged
19 months ago, by paulson
moved line segments to Convex_Euclidean_Space
19 months ago, by paulson
proper theory for export_proofs;
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
merged
19 months ago, by paulson
just tidied one proof
19 months ago, by paulson
proper graph traversal  avoid exponential blowup (amending 71d1971d67ad);
19 months ago, by wenzelm
oops — fixed symbols!!
19 months ago, by paulson
reorganisation to eliminate Brouwer_Fixpoint from complex analysis
19 months ago, by paulson
merged
19 months ago, by paulson
Inverse function theorem + lemmas
19 months ago, by paulson
back to more elementary Buffer.T  less intermediate garbage;
19 months ago, by wenzelm
unused;
19 months ago, by wenzelm
unused;
19 months ago, by wenzelm
more direct output of XML material  bypass Buffer.T;
19 months ago, by wenzelm
clarified signature;
19 months ago, by wenzelm
tuned;
19 months ago, by wenzelm
more direct output of XML material  bypass Buffer.T;
19 months ago, by wenzelm
more scalable protocol_message: use XML.body directly (Output.output hook is not required);
19 months ago, by wenzelm
clarified signature;
19 months ago, by wenzelm
tuned;
19 months ago, by wenzelm
updated to polyml5.8.120191101 test version;
20 months ago, by wenzelm
merged
20 months ago, by wenzelm
more operations;
20 months ago, by wenzelm
proper export of unnamed proof boxes for unnamed toplevel declarations, e.g. rulify/defn rules in theory IFOL and HOL;
20 months ago, by wenzelm
clarified signature (again);
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
make doublesure that internal proof boxes are exported, e.g. in Pure;
20 months ago, by wenzelm
avoid redundant proof boxes for application sessions;
20 months ago, by wenzelm
clarified modules (again);
20 months ago, by wenzelm
more detailed proof term output;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
clarified error;
20 months ago, by wenzelm
more accurate proof_boxes  from actual proof body;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
more lemmas
20 months ago, by haftmann
merged
20 months ago, by immler
linear is not needed
20 months ago, by immler
less
more

(0)
30000
10000
3000
1000
300
100
60
+60
+100
+300
+1000
tip