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 JavaScript-enabled browsers.
better error messages for datatypes not declared Const
2002-05-15, by paulson
better simplification of trivial existential equalities
2002-05-15, by paulson
numerals work again
2002-05-14, by kleing
*** empty log message ***
2002-05-13, by nipkow
*** empty log message ***
2002-05-13, by nipkow
*** empty log message ***
2002-05-13, by nipkow
quotes around types
2002-05-13, by paulson
Deleting two simprules saves 21 seconds!
2002-05-13, by paulson
tuned document;
2002-05-13, by wenzelm
updated X-Symbol URL;
2002-05-13, by wenzelm
converted Order.ML OrderType.ML OrderArith.ML to Isar format
2002-05-13, by paulson
fix for change in nat number simplification
2002-05-11, by kleing
- Tuned function mk_cnstrts
2002-05-11, by berghofe
conversion of AC branch to Isar
2002-05-10, by paulson
obsolete ML files
2002-05-10, by paulson
now-obsolete ML files
2002-05-10, by paulson
converted the AC branch to Isar
2002-05-10, by paulson
A new theory of pointer program examples
2002-05-10, by nipkow
Added Pointers.thy
2002-05-10, by nipkow
*** empty log message ***
2002-05-10, by nipkow
commented out half converted proof
2002-05-10, by nipkow
added dep on IMP/Compiler0
2002-05-10, by nipkow
tidied
2002-05-10, by paulson
Cambridge
2002-05-09, by paulson
fixed simproc bug
2002-05-09, by paulson
ordinal addition now coerces its arguments to ordinals
2002-05-09, by paulson
new thm distinct_conv_nth
2002-05-08, by nipkow
isar conversion
2002-05-08, by paulson
oops;
2002-05-08, by wenzelm
the new predicate "relation"
2002-05-08, by paulson
tidied
2002-05-08, by paulson
better xsymbol syntax
2002-05-08, by paulson
new lemmas
2002-05-08, by paulson
some ex files converted to Isar
2002-05-08, by paulson
converted to Isar
2002-05-08, by paulson
Tidied and converted to Isar by lcp
2002-05-08, by paulson
converted;
2002-05-07, by wenzelm
rev_bexI [intro?];
2002-05-07, by wenzelm
a bit of conversion to structured proofs
2002-05-07, by nipkow
*** empty log message ***
2002-05-07, by nipkow
be liberal about missing types;
2002-05-07, by wenzelm
*** empty log message ***
2002-05-07, by nipkow
tuned;
2002-05-07, by wenzelm
tuned presentation;
2002-05-07, by wenzelm
\documentclass{report};
2002-05-07, by wenzelm
use eq_thm_prop instead of slightly inadequate eq_thm;
2002-05-07, by wenzelm
clarified eq_thm;
2002-05-07, by wenzelm
Added insert_disjoint and disjoint_insert [simp], and simplified proofs
2002-05-06, by nipkow
Added skeletons to speed up rewriting on proof terms.
2002-05-04, by berghofe
tuned
2002-04-30, by kleing
physical location of isabelle repository is now sunbroy2
2002-04-30, by kleing
added abstract;corrected RG_Basic Hoare rule.
2002-04-29, by prensani
Better compiler proof
2002-04-29, by nipkow
Had to update proof for some strange reason
2002-04-29, by nipkow
added rev_take and rev_drop
2002-04-29, by nipkow
New machine architecture and other direction of compiler proof.
2002-04-26, by nipkow
added "m <= n ==> m-n = 0" [simp]
2002-04-25, by nipkow
code generator: wfrec combinator is now implemented by ML function wf_rec.
2002-04-19, by berghofe
Added example for code generation.
2002-04-19, by berghofe
wf is no longer implemented by true (due to change in definition of class_rec).
2002-04-19, by berghofe
less
more
|
(0)
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
+30000
tip