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

solved the problem that Larry's simproce cancle_numerals(?) returns
2002-02-25, by nipkow
added using_thmss(_i);
2002-02-24, by wenzelm
added using_facts;
2002-02-24, by wenzelm
replaced 'using' keyword by 'to';
2002-02-24, by wenzelm
tuned;
2002-02-24, by wenzelm
'using' command;
2002-02-24, by wenzelm
Added check for field/method access to operational semantics and proved the acesses valid.
2002-02-22, by schirmer
* HOL: removed obsolete theorem "optionE";
2002-02-21, by wenzelm
fixed get_name_tags in order to work with hyps;
2002-02-21, by wenzelm
clarified internal theory dependencies;
2002-02-21, by wenzelm
bind_thms basic_monos;
2002-02-21, by wenzelm
include theory Record (tuned dependencies);
2002-02-21, by wenzelm
removed theory Option;
2002-02-21, by wenzelm
theory Option has been assimilated by Datatype;
2002-02-21, by wenzelm
* HOL: removed obsolete theorem "optionE";
2002-02-21, by wenzelm
updated title;
2002-02-21, by wenzelm
new MicroJava document
2002-02-21, by kleing
fix toc
2002-02-21, by kleing
fixed document;
2002-02-21, by wenzelm
tr: quote argument;
2002-02-21, by wenzelm
new document
2002-02-21, by kleing
Removed superfluous lookup of theorems in Relation.thy
2002-02-20, by berghofe
Moved change_type to proofterm.ML
2002-02-20, by berghofe
New function strip_comb (cterm version of Term.strip_comb).
2002-02-20, by berghofe
New function change_type for changing type assignments of theorems,
2002-02-20, by berghofe
New function for eliminating definitions in proof term.
2002-02-20, by berghofe
Converted to new theory format.
2002-02-20, by berghofe
added is_quasi;
2002-02-20, by wenzelm
removed obscure functions bump_int_list, bump_list, bump_string;
2002-02-20, by wenzelm
Symbol.bump_string;
2002-02-20, by wenzelm
tuned;
2002-02-19, by wenzelm
Paulson:1989;
2002-02-19, by wenzelm
"isatool usedir -D output HOL Test && isatool document Test/output";
2002-02-19, by wenzelm
fixed copy_all
2002-02-16, by kleing
converted/deleted equalities.ML, mono.ML, subset.ML (see Set.thy);
2002-02-16, by wenzelm
removed unused unmask_interrupt;
2002-02-15, by wenzelm
clarified copy_all;
2002-02-15, by wenzelm
moved copy_all to Thy/present.ML;
2002-02-15, by wenzelm
replaced nodups by distinct;
2002-02-15, by wenzelm
tuned;
2002-02-15, by wenzelm
a new definition of "restrict"
2002-02-15, by paulson
made MLWorks happy;
2002-02-14, by wenzelm
*** empty log message ***
2002-02-14, by nipkow
nodups -> distinct
2002-02-14, by nipkow
nodups -> distinct
2002-02-14, by nipkow
deleted some redundant 'addS*Es [equalityC*E]'s
2002-02-13, by paulson
new function lemmas
2002-02-13, by paulson
tidied. no more special simpset (super_ss)
2002-02-13, by paulson
new lemmas for closure under Union
2002-02-13, by paulson
eliminated Pure/Isar/comment.ML;
2002-02-12, by wenzelm
ANTIQUOTE_FAIL;
2002-02-12, by wenzelm
eliminated Isar/comment.ML;
2002-02-12, by wenzelm
tuned;
2002-02-12, by wenzelm
added isabelle-hol-book;
2002-02-12, by wenzelm
* Isar/Pure: marginal comments ``--'' may now occur just anywhere in the text;
2002-02-12, by wenzelm
got rid of explicit marginal comments (now stripped earlier from input);
2002-02-12, by wenzelm
tuned;
2002-02-12, by wenzelm
ML-Systems/smlnj-compiler.ML compatibility tweak;
2002-02-11, by wenzelm
include SVC_Test;
2002-02-11, by wenzelm
Theorems are only "pre-named" if the do not already have names.
2002-02-07, by berghofe

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

isabelle