isabelle: Graph

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

new theorem single_Diff_lessThan
1999-09-08, by paulson
now uses the identity function
1999-09-08, by paulson
simplification of relations involving 0, Suc and natural-number numerals
1999-09-08, by paulson
generalized the theorem zless_zero_nat to zless_nat_eq_int_zless, and
1999-09-08, by paulson
generalized the theorem bin_add_BIT_Min to bin_add_Min_right
1999-09-08, by paulson
moved identity theorems to Fun.ML
1999-09-08, by paulson
comments
1999-09-08, by paulson
images and preimages of the identity function
1999-09-08, by paulson
new example HOL/UNITY/TimerArray
1999-09-08, by paulson
rule option;
1999-09-07, by wenzelm
\indexisarmeth: "Methods";
1999-09-07, by wenzelm
tuned (then_)apply;
1999-09-07, by wenzelm
url;
1999-09-07, by wenzelm
\url;
1999-09-07, by wenzelm
induct method: rule option;
1999-09-07, by wenzelm
Method.refine_no_facts;
1999-09-07, by wenzelm
read_def_termT: dummyT;
1999-09-07, by wenzelm
then_tac = refine;
1999-09-07, by wenzelm
read_typ/term: context_of;
1999-09-07, by wenzelm
tuned;
1999-09-07, by wenzelm
added context_of;
1999-09-07, by wenzelm
logtypes: pretend "dummy" is one;
1999-09-07, by wenzelm
isatool expandshort;
1999-09-07, by wenzelm
expandshort usage: forward_tac;
1999-09-06, by wenzelm
strengthened card_seteq
1999-09-06, by oheimb
added theorems subset_insertD, singleton_insert_inj_eq, subset_singletonD
1999-09-06, by oheimb
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
1999-09-06, by oheimb
added theorems le_maxI1 and le_maxI2, also in claset
1999-09-06, by oheimb
added theorem dvd_reduce
1999-09-06, by oheimb
*** empty log message ***
1999-09-06, by oheimb
added ftac, eatac, datac, fatac
1999-09-06, by oheimb
added smp_tac
1999-09-06, by oheimb
added;
1999-09-06, by wenzelm
isabelle-pdfdocs;
1999-09-06, by wenzelm
close_block: removed ProofContext.transfer_used_names;
1999-09-06, by wenzelm
removed thms_closure (unused);
1999-09-06, by wenzelm
removed thms_closure (unused);
1999-09-06, by wenzelm
added README;
1999-09-06, by wenzelm
tuned;
1999-09-06, by wenzelm
working snapshot
1999-09-06, by paulson
goal_nonempty: Ex goal for new-style version;
1999-09-04, by wenzelm
replaced ?? by ?;
1999-09-04, by wenzelm
eliminated Syntax.binding;
1999-09-04, by wenzelm
deactivated ProofContext.transfer_used_names;
1999-09-04, by wenzelm
removed text vars;
1999-09-04, by wenzelm
PureThy.have_thmss: "" replaces None;
1999-09-04, by wenzelm
Library.equal_lists;
1999-09-04, by wenzelm
removed Syntax.binding;
1999-09-04, by wenzelm
removed "_BIND" translation;
1999-09-04, by wenzelm
removed binding;
1999-09-04, by wenzelm
removed "_BIND" syntax;
1999-09-04, by wenzelm
eliminated default_name (thms no longer stored for name "");
1999-09-04, by wenzelm
ProtoPure: fake empty scope;
1999-09-04, by wenzelm
equal_lists: ('a * 'b -> bool) -> 'a list * 'b list -> bool;
1999-09-04, by wenzelm
handle Bind!!
1999-09-04, by wenzelm
updated;
1999-09-04, by wenzelm
added \indexisarvar;
1999-09-04, by wenzelm
removed \VVar;
1999-09-04, by wenzelm
usage: tell OPTIONS;
1999-09-03, by wenzelm
added welcome;
1999-09-03, by wenzelm

less more | (0) -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle