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 -15 +15 +100 +300 +1000 +3000 +10000 +30000 tip

Tactic.prove, Tactic.prove_standard;
2002-08-08, by wenzelm
* Pure: improved error reporting of simprocs;
2002-08-08, by wenzelm
tuned;
2002-08-07, by wenzelm
mk_left_commute: proper instantiation avoids expensive unification;
2002-08-07, by wenzelm
tuned;
2002-08-07, by wenzelm
Simplifier.simproc(_i);
2002-08-07, by wenzelm
Added time example at the end.
2002-08-07, by nipkow
section on "Rule declarations and methods";
2002-08-07, by wenzelm
Removed (now unneeded) declaration of realizer for induction on datatype b.
2002-08-07, by berghofe
Removed (now unneeded) declarations of realizers for induction on lists and letters.
2002-08-07, by berghofe
Added file Tools/datatype_realizer.ML
2002-08-07, by berghofe
Removed (now unneeded) declaration of realizers for induction on natural numbers.
2002-08-07, by berghofe
Module for defining realizers for induction and case analysis theorems
2002-08-07, by berghofe
Added calls to add_dt_realizers.
2002-08-07, by berghofe
Exported function make_tnames.
2002-08-07, by berghofe

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

isabelle