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

further cleanup of XML signature;
2008-04-03, by wenzelm
output: canonical argument order (as opposed to write);
2008-04-03, by wenzelm
XML.string_of;
2008-04-03, by wenzelm
moved output_markup to xml.ML;
2008-04-03, by wenzelm
XML.output_markup;
2008-04-03, by wenzelm
XML.string_of, XML.parse;
2008-04-03, by wenzelm
replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
2008-04-03, by wenzelm
added output_markup (from Tools/isabelle_process.ML);
2008-04-03, by wenzelm
replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
2008-04-03, by wenzelm
tuned comments;
2008-04-03, by wenzelm
Added skip_mono flag to inductive definition package.
2008-04-03, by berghofe
Added skip_mono flag to inductive definition package.
2008-04-03, by berghofe
Added skip_mono flag and inductive_flags type.
2008-04-03, by berghofe
Deleted code for axiomatic introduction of datatypes. Instead, the package
2008-04-03, by berghofe
Removed QuickAndDirty constructor from simproc_dist datatype.
2008-04-03, by berghofe
- use SkipProof.prove_global instead of Goal.prove_global
2008-04-03, by berghofe
Added prove_global.
2008-04-03, by berghofe
Function package no longer overwrites theorems.
2008-04-03, by krauss
Why XML notation?
2008-04-03, by wenzelm
Symbol.STX, Symbol.DEL;
2008-04-03, by wenzelm
Symbol.SOH;
2008-04-03, by wenzelm
added detect;
2008-04-03, by wenzelm
added some ASCII control symbols;
2008-04-03, by wenzelm
added Pure/General/yxml.ML;
2008-04-03, by wenzelm
added generalised definitions for freshness of sets of atoms
2008-04-03, by urbanc
tuned imports
2008-04-02, by haftmann
tuned
2008-04-02, by haftmann
subst_alias
2008-04-02, by haftmann
improved improvements for instantiaton
2008-04-02, by haftmann
canonical meet_sort operation
2008-04-02, by haftmann
removed obscure "attach" feature
2008-04-02, by haftmann
extended
2008-04-02, by haftmann
tuned towards code generation
2008-04-02, by haftmann
explicit class "eq" for operational equality
2008-04-02, by haftmann
proofs adjusted to new situation in Int.thy/Presburger.thy
2008-04-02, by haftmann
explicit instantiation
2008-04-02, by haftmann
tuned proof
2008-04-02, by haftmann
dropped wrong code lemma
2008-04-02, by haftmann
moved some code lemmas for Numerals to other theories
2008-04-02, by haftmann
moved some code lemmas for Numerals here
2008-04-02, by haftmann
No longer imports InfiniteSet, ATP_Linkup is sufficient.
2008-04-02, by chaieb
Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
2008-03-31, by gagern
before close: Exn.capture/release;
2008-03-31, by wenzelm
discontinued unused hooks explode_platform_path_fn, platform_path_fn, shell_path_fn;
2008-03-31, by wenzelm
added add_substring;
2008-03-31, by wenzelm
discontinued File.explode_platform_path -- use plain Path.explode;
2008-03-31, by wenzelm
*** empty log message ***
2008-03-30, by nipkow
functional theory setup -- requires linear access;
2008-03-29, by wenzelm
simplified print_simpset;
2008-03-29, by wenzelm
purely functional setup of claset/simpset/clasimpset;
2008-03-29, by wenzelm
purely functional setup of claset/simpset/clasimpset;
2008-03-29, by wenzelm
fixed spelling;
2008-03-29, by wenzelm
added exec_file;
2008-03-29, by wenzelm
CRITICAL: further trace levels for 1000ms and 100ms;
2008-03-29, by wenzelm
removed obsolete store_thm(s), cf. functional versions in pure_thy.ML;
2008-03-29, by wenzelm
added generic_theory transaction;
2008-03-29, by wenzelm
commands 'use' and 'ML' now thy_decl;
2008-03-29, by wenzelm
removed obsolete use_XXX;
2008-03-29, by wenzelm
eliminated destructive/critical theorem database;
2008-03-29, by wenzelm
certify wrt. dynamic context;
2008-03-29, by wenzelm

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

isabelle