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

clarified general_statement syntax;
2002-02-26, by wenzelm
renamed "uses" to "includes";
2002-02-26, by wenzelm
updated;
2002-02-26, by wenzelm
markup commands: proper theory/proof transactions!
2002-02-26, by wenzelm
tuned long_statement;
2002-02-26, by wenzelm
introduces SystemClasses and BVExample
2002-02-26, by kleing
*** empty log message ***
2002-02-26, by nipkow
Fixed the natxx_cancel_numerals simprocs so that they pull out Sucs and
2002-02-26, by paulson
*** empty log message ***
2002-02-26, by nipkow
*** empty log message ***
2002-02-26, by nipkow
Isar_examples/W_correct moved to W0;
2002-02-26, by wenzelm
tuned;
2002-02-26, by wenzelm
converted;
2002-02-26, by wenzelm
added check_text;
2002-02-25, by wenzelm
export locale_target, locale_keyword;
2002-02-25, by wenzelm
markup commands moved to isar_cmd.ML;
2002-02-25, by wenzelm
updated markup commands;
2002-02-25, by wenzelm
export eval_antiquote;
2002-02-25, by wenzelm
markup commands (from isar_thy.ML) with proper check of antiquotations;
2002-02-25, by wenzelm
clarified syntax of ``long'' statements: fixes/assumes/shows;
2002-02-25, by wenzelm
clarify module dependencies;
2002-02-25, by wenzelm
updated;
2002-02-25, by wenzelm
Clarification wrt. use of polymorphic variants of Hoare logic rules
2002-02-25, by oheimb
Introduced variants of operators + * ~ constrained to type int
2002-02-25, by berghofe
updated debugging output
2002-02-25, by nipkow
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

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

isabelle