Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
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.
working snapshot
19990910, by paulson
new theorem image_image_eq_UN
19990910, by paulson
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
19990910, by wenzelm
added no_prems;
19990909, by wenzelm
minor change to smp_tac
19990909, by oheimb
fixed url;
19990909, by wenzelm
AddXDs [bspec];
19990909, by wenzelm
tuned;
19990909, by wenzelm
AddXIs [disjI1, disjI2];
19990909, by wenzelm
removed obsolete comment;
19990909, by wenzelm
lemma less_add;
19990908, by wenzelm
(un)fold: ignore facts;
19990908, by wenzelm
more rational theorem names (?)
19990908, by paulson
tidied
19990908, by paulson
more rational theorem names (?)
19990908, by paulson
ensures_tac now handles leadsTo as well as LeadsTo
19990908, by paulson
new theorem single_Diff_lessThan
19990908, by paulson
now uses the identity function
19990908, by paulson
simplification of relations involving 0, Suc and naturalnumber numerals
19990908, by paulson
generalized the theorem zless_zero_nat to zless_nat_eq_int_zless, and
19990908, by paulson
generalized the theorem bin_add_BIT_Min to bin_add_Min_right
19990908, by paulson
moved identity theorems to Fun.ML
19990908, by paulson
comments
19990908, by paulson
images and preimages of the identity function
19990908, by paulson
new example HOL/UNITY/TimerArray
19990908, by paulson
rule option;
19990907, by wenzelm
\indexisarmeth: "Methods";
19990907, by wenzelm
tuned (then_)apply;
19990907, by wenzelm
url;
19990907, by wenzelm
\url;
19990907, by wenzelm
induct method: rule option;
19990907, by wenzelm
Method.refine_no_facts;
19990907, by wenzelm
read_def_termT: dummyT;
19990907, by wenzelm
then_tac = refine;
19990907, by wenzelm
read_typ/term: context_of;
19990907, by wenzelm
tuned;
19990907, by wenzelm
added context_of;
19990907, by wenzelm
logtypes: pretend "dummy" is one;
19990907, by wenzelm
isatool expandshort;
19990907, by wenzelm
expandshort usage: forward_tac;
19990906, by wenzelm
strengthened card_seteq
19990906, by oheimb
added theorems subset_insertD, singleton_insert_inj_eq, subset_singletonD
19990906, by oheimb
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
19990906, by oheimb
added theorems le_maxI1 and le_maxI2, also in claset
19990906, by oheimb
added theorem dvd_reduce
19990906, by oheimb
*** empty log message ***
19990906, by oheimb
added ftac, eatac, datac, fatac
19990906, by oheimb
added smp_tac
19990906, by oheimb
added;
19990906, by wenzelm
isabellepdfdocs;
19990906, by wenzelm
close_block: removed ProofContext.transfer_used_names;
19990906, by wenzelm
removed thms_closure (unused);
19990906, by wenzelm
removed thms_closure (unused);
19990906, by wenzelm
added README;
19990906, by wenzelm
tuned;
19990906, by wenzelm
working snapshot
19990906, by paulson
goal_nonempty: Ex goal for newstyle version;
19990904, by wenzelm
replaced ?? by ?;
19990904, by wenzelm
eliminated Syntax.binding;
19990904, by wenzelm
deactivated ProofContext.transfer_used_names;
19990904, by wenzelm
less
more

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