isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

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

more robust handling of explicit rules;
2000-04-01, by wenzelm
tuned mixfix syntax;
2000-04-01, by wenzelm
added ProofGeneral.undo;
2000-04-01, by wenzelm
isatool document: check output file (workaround PolyML problem with RC);
2000-04-01, by wenzelm
use cong_add_global att;
2000-03-31, by wenzelm
added cong atts;
2000-03-31, by wenzelm
added cong atts;
2000-03-31, by wenzelm
made SML/XL happy;
2000-03-31, by wenzelm
change_global/local_css move to Provers/clasimp.ML;
2000-03-31, by wenzelm
setup cong_attrib_setup;
2000-03-31, by wenzelm
added change_global/local_css;
2000-03-31, by wenzelm
added 'cong' att;
2000-03-31, by wenzelm
tuned;
2000-03-31, by wenzelm
params: preserve case names;
2000-03-31, by wenzelm
fixed indexing of elim rules;
2000-03-31, by wenzelm
use Attrib.add_del_args;
2000-03-31, by wenzelm
added add_del_args;
2000-03-31, by wenzelm
fixed goal syntax;
2000-03-31, by wenzelm
comments modified
2000-03-31, by nipkow
tuned
2000-03-31, by kleing
included new stanford mirror, mirror links now point to source directly
2000-03-31, by kleing
updated recdef
2000-03-31, by nipkow
tuned;
2000-03-30, by wenzelm
recdef
2000-03-30, by nipkow
If all termination conditions are proved automatically,
2000-03-30, by nipkow
recdef.rules -> recdef.simps
2000-03-30, by nipkow
mod in recdef allows to access the correct simpset via simpset().
2000-03-30, by nipkow
the simplification rules returned from TFL are now paired with the row they
2000-03-30, by nipkow
* Isar/Pure: local results and corresponding term bindings are now
2000-03-30, by wenzelm
support Hindley-Milner polymorphisms in results and bindings;
2000-03-30, by wenzelm

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

isabelle