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.
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
Improved definition of class_rec: no longer mixes algorithm and
2002-04-19, by berghofe
Added proof of Newman's lemma.
2002-04-19, by berghofe
new link to munich group
2002-04-16, by kleing
inserted tutorial
2002-04-16, by kleing
*** empty log message ***
2002-04-16, by nipkow
converted theory ex/Limit to Isar script, but it still needs work!
2002-04-15, by paulson
converted these theories to Isar format
2002-04-15, by paulson
*** empty log message ***
2002-04-12, by nipkow
*** empty log message ***
2002-04-08, by nipkow
*** empty log message ***
2002-04-08, by nipkow
tuned
2002-04-04, by kleing
conversion of Induct/{Slist,Sexp} to Isar scripts
2002-04-04, by paulson
flattened, uses locales
2002-04-04, by kleing
tuned
2002-04-04, by kleing
bugfix concerning claset(), added limited support for ALLGOALS + fast_tac etc.
2002-04-03, by oheimb
conversion of some HOL/Induct proof scripts to Isar
2002-04-02, by paulson
Started to convert to locales
2002-04-02, by nipkow
mk_const_id now checks for clashes with reserved ML identifiers.
2002-03-28, by berghofe
added lbv completeness
2002-03-27, by kleing
finished lbv completeness
2002-03-27, by kleing
merge mono
2002-03-26, by kleing
lub property of ++_f
2002-03-26, by kleing
+_f is associative and commutative
2002-03-26, by kleing
tuned
2002-03-24, by kleing
cleanup + simpler monotonicity
2002-03-24, by kleing
more about match_exception_table
2002-03-24, by kleing
first steps in semilattices..
2002-03-21, by kleing
new_Addr defined in terms of J/State.new_Addr (for compiler)
2002-03-21, by kleing
small refactoring for lbv with semilattices
2002-03-20, by kleing
Fewer premises for restrict_image
2002-03-18, by paulson
cambridge
2002-03-14, by paulson
removed ex/set.ML
2002-03-14, by paulson
converted theory "set" to Isar and added some SET-VAR examples
2002-03-14, by paulson
increased treshold for "this expression could be extremely ambigous" warning
2002-03-14, by kleing
workaround for "ins" bug in sml/nj + code generator
2002-03-12, by kleing
*** empty log message ***
2002-03-12, by nipkow
added Berhard Rumpe, Farhad Mehta;
2002-03-11, by wenzelm
less
more
|
(0)
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
+30000
tip