Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
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.
removed dead code
20080804, by krauss
simplified prepare_command;
20080804, by wenzelm
Isar.command: explicitly set transaction position, as required for prepare_command errors;
20080804, by wenzelm
Updated locale tests.
20080804, by ballarin
Generalised polynomial lemmas from cring to ring.
20080801, by ballarin
Removed import and lparams from locale record.
20080801, by ballarin
made setsum executable on int.
20080801, by nipkow
Tuned (for the sake of a meaningless log entry).
20080731, by ballarin
New locales for orders and lattices where the equivalence relation is not restricted to equality.
20080730, by ballarin
added hint about writing "x : set xs".
20080730, by nipkow
simple lifters
20080730, by haftmann
dropped imperative monad bind
20080730, by haftmann
facts_of
20080730, by haftmann
improved morphism
20080730, by haftmann
SML_imp, OCaml_imp
20080730, by haftmann
clarified
20080730, by haftmann
tuned
20080730, by haftmann
Zorn's Lemma for partial orders.
20080729, by ballarin
Definitions and some lemmas for reflexive orderings.
20080729, by ballarin
Lemmas added
20080729, by ballarin
New theory on divisibility.
20080729, by ballarin
Renamed theorems;
20080729, by ballarin
New theorems on summation.
20080729, by ballarin
Unit_inv_l, Unit_inv_r made [simp].
20080729, by ballarin
New theory on divisibility;
20080729, by ballarin
Unit_inv_l, Unit_inv_r made [simp];
20080729, by ballarin
Haskell now living in the RealWorld
20080729, by haftmann
corrected Pure dependency
20080729, by haftmann
added removeAll
20080729, by nipkow
tuned; explicit export of element accessors
20080729, by haftmann
PureThy: dropped note_thmss_qualified, dropped _i suffix
20080729, by haftmann
some steps towards explicit class target for canonical interpretation
20080729, by haftmann
declare
20080729, by haftmann
*** empty log message ***
20080728, by nipkow
simplified a proof
20080727, by urbanc
tuned function name
20080726, by haftmann
tuned bootstrap order
20080726, by haftmann
subclass now also works for subclasses with empty specificaton
20080725, by haftmann
dropped PureThy.note; added PureThy.add_thm
20080725, by haftmann
added class preorder
20080725, by haftmann
dropped locale (open)
20080725, by haftmann
added explicit root theory; some tuning
20080725, by haftmann
tuned
20080725, by haftmann
dropped locale (open)
20080725, by haftmann
(re)added simp rules for (_ + _) div/mod _
20080721, by haftmann
(re)added simp rules for (_ + _) div/mod _
20080721, by haftmann
added explicit purge_data
20080721, by haftmann
added code generation
20080721, by haftmann
fixed code generator setup
20080721, by haftmann
(adjusted)
20080721, by haftmann
Tuned and corrected ideal_tac for algebra.
20080721, by chaieb
Theorems divides_le, ind_euclid, bezout_lemma, bezout_add, bezout, bezout_add_strong, gcd_unique,gcd_eq, bezout_gcd, bezout_gcd_strong, gcd_mult_distrib, gcd_bezout to GCD.thy
20080721, by chaieb
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
20080721, by chaieb
Tuned and simplified proofs
20080721, by chaieb
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy  relevant for algebra
20080721, by chaieb
Relevant rules added to algebra's context
20080721, by chaieb
renamed item to span, renamed contructors;
20080720, by wenzelm
adapted ThyEdit.span;
20080720, by wenzelm
maintain token range;
20080720, by wenzelm
tty loop: do not report status;
20080720, by wenzelm
less
more

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