isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -10000 -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 +30000 tip

"num" syntax;
2001-10-05, by wenzelm
added axclass "one" and polymorphic const "1";
2001-10-05, by wenzelm
added "num" token;
2001-10-05, by wenzelm
induct: case names;
2001-10-05, by wenzelm
sane spacing of "-";
2001-10-05, by wenzelm
tuned;
2001-10-05, by wenzelm
Thm.major_prem_of part of Logic.strip_assums_concl;
2001-10-04, by wenzelm
major_prem_of: Logic.strip_assums_concl;
2001-10-04, by wenzelm
induct/cases made generic, removed simplified/stripped options;
2001-10-04, by wenzelm
improved proof by cases and induction;
2001-10-04, by wenzelm
removed obsolete comment;
2001-10-04, by wenzelm
generic induct_method.ML;
2001-10-04, by wenzelm
non-oriented infix = and ~= (output only);
2001-10-04, by wenzelm
$(SRC)/Provers/induct_method.ML replaces Tools/induct_method.ML;
2001-10-04, by wenzelm
use "~~/src/Provers/induct_method.ML";
2001-10-04, by wenzelm
removed hol_rewrite_cterm (use full_rewrite_cterm from Pure);
2001-10-04, by wenzelm
added dest_concls;
2001-10-04, by wenzelm
simp_case_tac is back again from induct_method.ML;
2001-10-04, by wenzelm
made generic (see Provers/induct_method.ML);
2001-10-04, by wenzelm
qualify MetaSimplifier;
2001-10-04, by wenzelm
unsymbolized;
2001-10-04, by wenzelm
moved atomize stuff to theory IFOL;
2001-10-04, by wenzelm
atomize stuff from theory FOL;
2001-10-04, by wenzelm
added Provers/induct_method.ML, document/root.tex, ex/Natural_Numbers.thy;
2001-10-04, by wenzelm
theory Natural_Numbers;
2001-10-04, by wenzelm
use "~~/src/Provers/induct_method.ML";
2001-10-04, by wenzelm
Theory of the natural numbers: Peano's axioms, primitive recursion.
2001-10-04, by wenzelm
full_rewrite_cterm_aux (see also tactic.ML);
2001-10-04, by wenzelm
added full_rewrite_cterm;
2001-10-04, by wenzelm
proof by cases and induction on types and sets (used to be specific for HOL);
2001-10-04, by wenzelm

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

isabelle