Mercurial
Mercurial
>
repos
>
testboard
/ 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.
examples of arithmetic on the naturals
19990719, by paulson
deleted a reference to "nat", now erroneous because "nat" is a function
19990719, by paulson
many new laws about div and mod
19990719, by paulson
new theorem zless_zero_nat
19990719, by paulson
removal of rewrites for Suc(Suc(Suc...)))
19990719, by paulson
NatBin: binary arithmetic for the naturals
19990719, by paulson
getting rid of qed_goal
19990719, by paulson
getting rid of qed_goal
19990719, by paulson
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
19990719, by paulson
Modifid length_tl
19990718, by nipkow
adapted to dest_keywords, dest_parsers;
19990716, by wenzelm
separate command tokens;
19990716, by wenzelm
tuned dest_lexicon;
19990716, by wenzelm
tuned;
19990716, by wenzelm
removed break;
19990716, by wenzelm
removed BREAK, ROLLBACK;
19990716, by wenzelm
structure LocalDefs = LocalDefs;
19990716, by wenzelm
Exported function unify_consts (workaround to avoid inconsistently
19990716, by berghofe
Added new example (infinitely branching trees).
19990716, by berghofe
Infinitely branching trees.
19990716, by berghofe
Replaced datatype_info by datatype_info_err.
19990716, by berghofe
 Now also supports arbitrarily branching datatypes.
19990716, by berghofe
 Datatype package now also supports arbitrarily branching datatypes
19990716, by berghofe
Added some definitions and theorems needed for the
19990716, by berghofe
Some rather large datatype examples (from John Harrison).
19990716, by berghofe
improved print_thms;
19990715, by wenzelm
export init_state;
19990715, by wenzelm
more renaming of theorems from _nat to _int (corresponding to a function that
19990715, by paulson
more renaming of theorems from _nat to _int (corresponding to a function that
19990715, by paulson
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
19990715, by paulson
qed_goal > Goal
19990715, by paulson
tuned;
19990714, by wenzelm
tuned comments;
19990714, by wenzelm
tuned contradiction method;
19990714, by wenzelm
improved comment;
19990714, by wenzelm
more marg_comments;
19990714, by wenzelm
Deriving rules in Isabelle;
19990714, by wenzelm
rewrite add1_zle_eq is no longer in the default simpset
19990714, by paulson
optimization for division by powers of 2
19990714, by paulson
new montonicity theorems
19990714, by paulson
new constant folding rewrites
19990714, by paulson
handle cgoal;
19990713, by wenzelm
added mk_cgoal, assume_goal;
19990713, by wenzelm
same_tac;
19990713, by wenzelm
change to force (m div 0 = 0)
19990713, by paulson
many new theorems
19990713, by paulson
renamed inj_nat to inj_int
19990713, by paulson
new monotonicity theorems
19990713, by paulson
new theorem zmult_eq_0_iff
19990713, by paulson
renamed sort "numeral" to "number"
19990713, by paulson
simplified the <= monotonicity proof
19990713, by paulson
local qeds: print rule;
19990712, by wenzelm
added show_hyps flag;
19990712, by wenzelm
local qed; print rule;
19990712, by wenzelm
term/prop: include number;
19990712, by wenzelm
added show_hyps flag;
19990712, by wenzelm
export assumption_tac;
19990712, by wenzelm
removed merge_theories;
19990712, by wenzelm
removed metacuts_tac;
19990712, by wenzelm
tmp_path: *add* path;
19990712, by wenzelm
less
more

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