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
+3000
+10000
+30000
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.
use 'example_proof' (invisible);
20100426, by wenzelm
command 'example_proof' opens an empty proof body;
20100426, by wenzelm
proofs that are discontinued via 'oops' are treated as relevant  for improved robustness of the final join of all proofs, which is hooked to results that are missing here;
20100426, by wenzelm
eliminanated some unreferenced identifiers;
20100426, by wenzelm
merged
20100426, by wenzelm
add bounded_lattice_bot and bounded_lattice_top type classes
20100426, by Cezary Kaliszyk
merged
20100426, by haftmann
dropped group_simps, ring_simps, field_eq_simps
20100426, by haftmann
class division_ring_inverse_zero
20100426, by haftmann
dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
20100426, by haftmann
line break
20100426, by haftmann
removed unused AxClass.class_intros;
20100426, by wenzelm
updated Sign.add_type_abbrev;
20100426, by wenzelm
merged
20100426, by haftmann
field_simps as named theorems
20100425, by haftmann
merged
20100425, by wenzelm
generalize more constants and lemmas
20100425, by huffman
simplify types of path operations (use real instead of real^1)
20100425, by huffman
add lemmas convex_real_interval and convex_box
20100425, by huffman
generalize more constants and lemmas
20100424, by huffman
generalize constant closest_point
20100424, by huffman
minimize imports
20100424, by huffman
fix imports
20100424, by huffman
document generation for Multivariate_Analysis
20100424, by huffman
move l2norm stuff into separate theory file
20100424, by huffman
convert proofs to Isarstyle
20100424, by huffman
Library/Fraction_Field.thy: ordering relations for fractions
20100424, by huffman
renamed Drule.unconstrainTs to Thm.unconstrain_allTs to accomdate the version by krauss/schropp;
20100425, by wenzelm
more systematic treatment of data  avoid slightly odd nested tuples here;
20100425, by wenzelm
replaced Sorts.rep_algebra by slightly more abstract selectors classes_of/arities_of;
20100425, by wenzelm
misc tuning and simplification;
20100425, by wenzelm
simplified some private bindings;
20100425, by wenzelm
classrel and arity completion by krauss/schropp;
20100425, by wenzelm
removed obsolete/unused Proof.match_bind;
20100425, by wenzelm
modernized naming conventions of main Isar proof elements;
20100425, by wenzelm
goals: simplified handling of implicit variables  removed obsolete warning;
20100425, by wenzelm
updated generated files;
20100423, by wenzelm
cover 'schematic_lemma' etc.;
20100423, by wenzelm
mark schematic statements explicitly;
20100423, by wenzelm
eliminated spurious schematic statements;
20100423, by wenzelm
explicit 'schematic_theorem' etc. for schematic theorem statements;
20100423, by wenzelm
collapse category "schematic goal" in keyword table  Proof General does not know about this;
20100423, by wenzelm
added keyword category "schematic goal", which prevents any attempt to fork the proof;
20100423, by wenzelm
merged
20100423, by wenzelm
merged
20100423, by haftmann
separated instantiation of division_by_zero
20100423, by haftmann
epheremal replacement of field_simps by field_eq_simps; dropped old division_by_zero instance
20100423, by haftmann
adapted to new times_divide_eq simp situation
20100423, by haftmann
epheremal replacement of field_simps by field_eq_simps
20100423, by haftmann
dequalified fact name
20100423, by haftmann
sharpened constraint (c.f. 4e7f5b22dd7d); explicit is better than implicit
20100423, by haftmann
separated instantiation of division_by_zero
20100423, by haftmann
dequalified fact name
20100423, by haftmann
less special treatment of times_divide_eq [simp]
20100423, by haftmann
sharpened constraint (c.f. 4e7f5b22dd7d)
20100423, by haftmann
more localization; tuned proofs
20100423, by haftmann
more localization; factored out lemmas for division_ring
20100423, by haftmann
modernized abstract algebra theories
20100423, by haftmann
merged
20100423, by haftmann
swapped generic code generator and SML code generator
20100422, by haftmann
less
more

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