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.
updated;
2002-06-20, by wenzelm
tuned;
2002-06-20, by wenzelm
0 -> key
2002-06-19, by nipkow
added the Constructible target
2002-06-19, by paulson
LBV instantiantion refactored, streamlined
2002-06-19, by kleing
new theory of inner models
2002-06-19, by paulson
conversion of Cardinal to Isar script
2002-06-19, by paulson
conversion of Cardinal, CardinalArith
2002-06-19, by paulson
tidying
2002-06-18, by paulson
new lemma
2002-06-18, by paulson
conversion of Fixedpt to Isar script
2002-06-18, by paulson
new theorems
2002-06-18, by paulson
conversion of CardinalArith to Isar script
2002-06-16, by paulson
LBV instantiated for JVM
2002-06-15, by kleing
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
2002-06-14, by kleing
IsarTut;
2002-06-14, by wenzelm
better proof of ord_iso_restrict_pred
2002-06-14, by paulson
BUG FIX in inst_thm: use current context instead of that of thm!!!
2002-06-13, by wenzelm
extra copy to sk
2002-06-12, by paulson
stronger strong soundness
2002-06-11, by kleing
added the usual file headers
2002-06-11, by oheimb
included strong soundness (sound + s0 <= phi!0)
2002-06-11, by kleing
updated;
2002-06-06, by wenzelm
examples;
2002-06-06, by wenzelm
updated;
2002-06-06, by wenzelm
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
2002-06-05, by paulson
initial setup;
2002-06-05, by wenzelm
*** empty log message ***
2002-06-03, by nipkow
Added ex/MergeSort
2002-06-03, by nipkow
Added constants for Hyp, Oracle and MinProof.
2002-05-31, by berghofe
Changed interface of Pattern.rewrite_term.
2002-05-31, by berghofe
Changed interface of MetaSimplifier.rewrite_term.
2002-05-31, by berghofe
Changed interface of rewrite_term.
2002-05-31, by berghofe
Changes to rewrite_term:
2002-05-31, by berghofe
conversion of Finite to Isar format
2002-05-31, by paulson
finished an incomplete proof
2002-05-31, by paulson
fixed a proof near the end
2002-05-31, by paulson
*** empty log message ***
2002-05-31, by nipkow
*** empty log message ***
2002-05-31, by nipkow
Now arith can deal with div/mod arbitrary nat numerals.
2002-05-31, by nipkow
*** empty log message ***
2002-05-30, by nipkow
Modifications due to enhanced linear arithmetic.
2002-05-30, by nipkow
Big update. Allows case splitting on ~= now (trying both < and >).
2002-05-30, by nipkow
deleted some useless ML bindings
2002-05-28, by paulson
added <-> and ~
2002-05-28, by paulson
conversion of IntDiv.thy to Isar format
2002-05-28, by paulson
Eps -> Hilbert_Choice.Eps
2002-05-28, by berghofe
*** empty log message ***
2002-05-27, by nipkow
tidied; stronger lemmas about functions
2002-05-24, by paulson
strong lemmas about functions
2002-05-24, by paulson
new quantifier lemmas
2002-05-24, by paulson
converted Update to Isar
2002-05-24, by paulson
conversion of Perm to Isar. Strengthening of comp_fun_apply
2002-05-24, by paulson
new definition of "apply" and new simprule "beta_if"
2002-05-23, by paulson
more tidying
2002-05-22, by paulson
new version of nat_case, nat_case3
2002-05-22, by paulson
tidying up
2002-05-22, by paulson
conversion of Nat to Isar
2002-05-22, by paulson
tidied
2002-05-22, by paulson
conversion of OrdQuant.ML to Isar
2002-05-21, by paulson
less
more
|
(0)
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
+30000
tip