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

Sequents/LK/Nat: new example of simplification in LK
1999-07-27, by paulson
added gen_inter
1999-07-27, by paulson
expandshort and tidying
1999-07-27, by paulson
expandshort; tidied
1999-07-27, by paulson
tidied
1999-07-27, by paulson
expandshort
1999-07-26, by paulson
HOL/ex/Tarski: new example by Florian Kammueller
1999-07-26, by paulson
new facts about binomials
1999-07-26, by paulson
three new theorems
1999-07-26, by paulson
new cancellation laws
1999-07-26, by paulson
tidied
1999-07-26, by paulson
new simprocs assoc_fold and combine_coeff
1999-07-23, by paulson
removed the combine_coeff simproc because linear arith does not handle
1999-07-23, by paulson
now using correctly-typed constants from HOLogic
1999-07-23, by paulson
heavily revised by Jacques: coercions have alphabetic names;
1999-07-23, by paulson
because intT is now defined in HOLogic
1999-07-23, by paulson
zmult_ac are no longer included by default
1999-07-23, by paulson
zadd_ac and zmult_ac are no longer included by default
1999-07-23, by paulson
added boolean and binary constants
1999-07-23, by paulson
new simprocs assoc_fold and combine_coeff
1999-07-23, by paulson
rail -a;
1999-07-23, by wenzelm
tuned add_term_varnames;
1999-07-23, by wenzelm
replaced assoc lists by Symtab.table;
1999-07-23, by wenzelm
Type.norm_term;
1999-07-23, by wenzelm
replace assoc lists by Symtab.table;
1999-07-23, by wenzelm
require_thy: fixed performance leak;
1999-07-23, by wenzelm
fix occurences of numerals in HOL/ZF terms;
1999-07-23, by wenzelm
New lemmas by Stefan Merz.
1999-07-23, by nipkow
avoid '(0 subgoals)';
1999-07-22, by wenzelm
Toplevel.excursion_error;
1999-07-22, by wenzelm
added exists;
1999-07-22, by wenzelm
Tuned.
1999-07-22, by berghofe
a stronger diff_less and no more le_diff_less
1999-07-21, by paulson
removed 2 qed_goals
1999-07-21, by paulson
tweaked proofs to handle new freeness reasoning for data c onstructors
1999-07-21, by paulson
more existing theorems renamed to use #0; also new results
1999-07-21, by paulson
now exports mk_bin
1999-07-21, by paulson
a more robust proof
1999-07-21, by paulson
tweaked proof after removal of diff_is_0_eq RS iffD2
1999-07-21, by paulson
better error message for curried recdefs, etc.
1999-07-21, by paulson
Mod by Norber Voelcker
1999-07-21, by nipkow
checkpoint;
1999-07-20, by wenzelm
Eliminated addDistinct.
1999-07-20, by berghofe
facts: no statement_binds;
1999-07-19, by wenzelm
Datatype package now handles arbitrarily branching datatypes.
1999-07-19, by berghofe
skeleton only;
1999-07-19, by wenzelm
added isar-ref;
1999-07-19, by wenzelm
Documented usage of function types in datatype specifications.
1999-07-19, by berghofe
added attdx, methdx;
1999-07-19, by wenzelm
added isabelle_isar logo;
1999-07-19, by wenzelm
updated;
1999-07-19, by wenzelm
renamed 'with' to 'using';
1999-07-19, by wenzelm
*** empty log message ***
1999-07-19, by wenzelm
NatBin: binary arithmetic for the naturals
1999-07-19, by paulson
examples of arithmetic on the naturals
1999-07-19, by paulson
deleted a reference to "nat", now erroneous because "nat" is a function
1999-07-19, by paulson
many new laws about div and mod
1999-07-19, by paulson
new theorem zless_zero_nat
1999-07-19, by paulson
removal of rewrites for Suc(Suc(Suc...)))
1999-07-19, by paulson
NatBin: binary arithmetic for the naturals
1999-07-19, by paulson

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

isabelle