isabelle: Graph

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

enable_interrupt is back!
2002-03-01, by wenzelm
tuned;
2002-02-28, by wenzelm
renamed mask_interrupt to ignore_interrupt;
2002-02-28, by wenzelm
renamed mask_interrupt to ignore_interrupt;
2002-02-28, by wenzelm
renamed mask_interrupt to ignore_interrupt;
2002-02-28, by wenzelm
use ignore_interrupt, raise_interrupt;
2002-02-28, by wenzelm
delete .cvsignore;
2002-02-28, by wenzelm
export THIS_IS_ISABELLE_ADMIN=true;
2002-02-28, by wenzelm
fixed date;
2002-02-28, by wenzelm
more stuff;
2002-02-28, by wenzelm
moved match_bvs, match_bvars, renAbs to term.ML;
2002-02-28, by wenzelm
added match_bvars, rename_abs (from thm.ML);
2002-02-28, by wenzelm
rewrite_term: Term.rename_abs;
2002-02-28, by wenzelm
decomp_simp': use lhs instead of elhs (preserves more bound variable names);
2002-02-28, by wenzelm
included LBVSpec again
2002-02-28, by kleing
updated;
2002-02-28, by wenzelm
contexts, locales, sym(metric);
2002-02-28, by wenzelm
fixing nat_combine_numerals simprocs (again)
2002-02-28, by paulson
enforce positive branch targets
2002-02-28, by kleing
fixed missing label
2002-02-28, by kleing
fixed document
2002-02-28, by kleing
tuned feedback of goal forms;
2002-02-27, by wenzelm
improved messages;
2002-02-27, by wenzelm
tuned local goal forms;
2002-02-27, by wenzelm
'declare': and_list1;
2002-02-27, by wenzelm
tuned;
2002-02-27, by wenzelm
'using' command;
2002-02-27, by wenzelm
renamed 'uses' to 'includes';
2002-02-27, by wenzelm
tuned;
2002-02-27, by wenzelm
Some simple properties of dynamic accessibility added.
2002-02-27, by schirmer
Cleaning up the definition of static overriding.
2002-02-27, by schirmer
tuned;
2002-02-26, by wenzelm
quote "includes" (now a keyword);
2002-02-26, by wenzelm
clarified localized multi statements;
2002-02-26, by wenzelm
added smart_have_thmss (global storage);
2002-02-26, by wenzelm
clarified multi statements;
2002-02-26, by wenzelm
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
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