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.
setup for refined facts handling;
19990921, by wenzelm
setup for refined facts handling;
19990921, by wenzelm
export prems_of;
19990921, by wenzelm
setup_goal: do not insert assumptions;
19990921, by wenzelm
setup for refined facts handling;
19990921, by wenzelm
differ: compare actual props only (hyps may changed due to trivial steps involving assumptions);
19990921, by wenzelm
added bang_facts;
19990921, by wenzelm
Added comments.
19990921, by nipkow
Now distinguishes discrete from nondistrete types.
19990921, by nipkow
moved inf_of(?) to hologic.
19990921, by nipkow
Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
19990921, by nipkow
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
19990921, by nipkow
new proof of drop_prog_correct for new definition of project_act
19990921, by paulson
project_act no longer has a special case to allow identity actions
19990921, by paulson
fixed SOUNDNESS BUG concerning the map from terms like ?f x y to SVC variables
19990921, by paulson
Fixed bug in add_primrec which caused noninformative error message.
19990920, by berghofe
renamed Always_Int to Always_Int_I
19990920, by paulson
new theorem mono_Follows_apply
19990920, by paulson
new theorem Always_INT_distrib; therefore renamed Always_Int
19990920, by paulson
working Safety proof for the system at last
19990920, by paulson
now uses Pattern.aeconv, not aconv, to test equality between the terms
19990920, by paulson
new rule PLam_ensures
19990917, by paulson
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
less
more

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