Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-3000
-1000
-224
+224
+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.
*** empty log message ***
2002-07-01, by nipkow
*** empty log message ***
2002-07-01, by nipkow
*** empty log message ***
2002-07-01, by nipkow
fixed problem with linear arith.
2002-07-01, by nipkow
new splitting rules for zdiv, zmod
2002-06-29, by paulson
conversion of many files to Isar format
2002-06-29, by paulson
*** empty log message ***
2002-06-28, by nipkow
Additional rule for rewriting on ==.
2002-06-28, by berghofe
Added function prop_of' taking assumption context as an argument.
2002-06-28, by berghofe
new theorems, tidying
2002-06-28, by paulson
class quantifiers (some)
2002-06-28, by paulson
added class quantifiers
2002-06-28, by paulson
tweaked
2002-06-28, by paulson
new treatment of wfrec, replacing wf[A](r) by wf(r)
2002-06-26, by paulson
*** empty log message ***
2002-06-26, by nipkow
*** empty log message ***
2002-06-26, by nipkow
new theorems
2002-06-26, by paulson
towards absoluteness of wfrec-defined functions
2002-06-26, by paulson
email sending
2002-06-24, by isatest
development and tweaks
2002-06-24, by paulson
moving some results around
2002-06-24, by paulson
new lemmas
2002-06-24, by paulson
towards absoluteness of wf
2002-06-24, by paulson
tweaks
2002-06-24, by paulson
conversion of Sum, pair to Isar script
2002-06-23, by paulson
converted Bool, Trancl, Rel to Isar format
2002-06-22, by paulson
*** empty log message ***
2002-06-21, by nipkow
cleanup old isabelle-* dirs before test start
2002-06-21, by isatest
included masterlog file
2002-06-21, by isatest
fail not so early, but produce correct exit code in the end
2002-06-21, by kleing
tuned
2002-06-20, by isatest
tuned
2002-06-20, by kleing
tuned
2002-06-20, by kleing
for nightly test builds
2002-06-20, by kleing
fail more gracefully, return proper exit codes, allow preset DISTPREFIX
2002-06-20, by kleing
fail early
2002-06-20, by kleing
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
converted domrange to Isar and merged with equalities
2002-05-21, by paulson
conversion of WF to Isar format
2002-05-20, by paulson
conversion of equalities to Isar
2002-05-20, by paulson
conversion of equalities and WF to Isar
2002-05-20, by paulson
converted Epsilon to Isar
2002-05-18, by paulson
converted Arith, Univ, func to Isar format!
2002-05-18, by paulson
New theorems from Constructible, and moving some Isar material from Main
2002-05-17, by paulson
unsymbolize
2002-05-17, by paulson
deleting the obsolete theorem lt_succ_iff
2002-05-17, by paulson
Turned into Isar theories.
2002-05-17, by nipkow
*** empty log message ***
2002-05-17, by nipkow
allowed more general split rules to cope with div/mod 2
2002-05-17, by nipkow
Used to be Divides.ML
2002-05-17, by nipkow
converting Ordinal.ML to Isar format
2002-05-16, by paulson
Set up arith to deal with div 2 and mod 2.
2002-05-15, by nipkow
arith can now deal with div 2 and mod 2.
2002-05-15, by nipkow
Divides.ML -> Divides_lemmas.ML
2002-05-15, by nipkow
Removed superfluous thm
2002-05-15, by nipkow
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
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
tuned;
2002-03-10, by wenzelm
canonical start state
2002-03-09, by kleing
in wellformed programs, exceptions are classes
2002-03-09, by kleing
tuned;
2002-03-08, by wenzelm
tuned;
Isabelle2002
2002-03-08, by wenzelm
tuned;
2002-03-08, by wenzelm
tuned;
2002-03-08, by wenzelm
removed Stanford mirror;
2002-03-08, by wenzelm
drop Stanford mirror;
2002-03-08, by wenzelm
for rail v 1.2
2002-03-08, by paulson
renamed nat_number_of to nat_number (avoid clash with separate theorem);
2002-03-07, by wenzelm
tuned;
2002-03-07, by wenzelm
*** empty log message ***
2002-03-07, by wenzelm
less
more
|
(0)
-10000
-3000
-1000
-224
+224
+1000
+3000
+10000
+30000
tip