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.
tweaked proofs to handle new freeness reasoning for data c onstructors
19990721, by paulson
more existing theorems renamed to use #0; also new results
19990721, by paulson
now exports mk_bin
19990721, by paulson
a more robust proof
19990721, by paulson
tweaked proof after removal of diff_is_0_eq RS iffD2
19990721, by paulson
better error message for curried recdefs, etc.
19990721, by paulson
Mod by Norber Voelcker
19990721, by nipkow
checkpoint;
19990720, by wenzelm
Eliminated addDistinct.
19990720, by berghofe
facts: no statement_binds;
19990719, by wenzelm
Datatype package now handles arbitrarily branching datatypes.
19990719, by berghofe
skeleton only;
19990719, by wenzelm
added isarref;
19990719, by wenzelm
Documented usage of function types in datatype specifications.
19990719, by berghofe
added attdx, methdx;
19990719, by wenzelm
added isabelle_isar logo;
19990719, by wenzelm
updated;
19990719, by wenzelm
renamed 'with' to 'using';
19990719, by wenzelm
*** empty log message ***
19990719, by wenzelm
NatBin: binary arithmetic for the naturals
19990719, by paulson
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
less
more

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