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 tidying; killing of old Watcher loops
2005-09-20, by paulson
added a number of lemmas
2005-09-20, by nipkow
uniform handling of interrupts
2005-09-20, by paulson
algebra method added.
2005-09-20, by chaieb
improved eq_fst and eq_snd, removed some deprecated stuff
2005-09-20, by haftmann
added make and find
2005-09-20, by haftmann
slight adaptions to library changes
2005-09-20, by haftmann
infix operator precedence
2005-09-20, by haftmann
using curried Inttab.update_new function now
2005-09-20, by webertj
SAT solver interface modified to support proofs of unsatisfiability
2005-09-19, by webertj
shrink: compress terms and types;
2005-09-19, by wenzelm
added String.isSuffix;
2005-09-19, by wenzelm
maybe the last bug fix (sigh)?
2005-09-19, by obua
Removed superfluous HOL/Matrix/cplex/ROOT.ML.
2005-09-19, by obua
further simplification of the Isabelle-ATP linkup
2005-09-19, by paulson
added make function
2005-09-19, by haftmann
removed some deprecated assocation list functions
2005-09-19, by haftmann
introduced AList module
2005-09-19, by haftmann
simplification of the Isabelle-ATP code; hooks for batch generation of problems
2005-09-19, by paulson
update usage message
2005-09-19, by kleing
obsolete;
2005-09-19, by wenzelm
converted to Isar theory format;
2005-09-18, by wenzelm
converted to Isar theory format;
2005-09-18, by wenzelm
converted to Isar theory format;
2005-09-17, by wenzelm
tuned;
2005-09-17, by wenzelm
converted to Isar theory format;
2005-09-17, by wenzelm
moved quick_and_dirty to Pure/ROOT.ML;
2005-09-17, by wenzelm
pretty_thm_aux: ora masked by quick_and_dirty;
2005-09-17, by wenzelm
added quick_and_dirty (from Isar/skip_proofs.ML);
2005-09-17, by wenzelm
manually generated from Isabelle/HOLCF/IOA/Complex/Import;
2005-09-17, by wenzelm
tuned document;
2005-09-17, by wenzelm
tuned;
2005-09-17, by wenzelm
added with_charset: string -> ('a -> 'b) -> 'a -> 'b;
2005-09-17, by wenzelm
tuned comments;
2005-09-17, by wenzelm
pretty_thm_aux: aconv hyps;
2005-09-17, by wenzelm
removed obsolete BasisLibrary;
2005-09-17, by wenzelm
Hebrew: HTML.with_charset;
2005-09-17, by wenzelm
removed obsolete BasisLibrary;
2005-09-17, by wenzelm
added quickcheck_params (from Main.thy);
2005-09-17, by wenzelm
removed spurious PolyML.exception_trace;
2005-09-17, by wenzelm
moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories);
2005-09-17, by wenzelm
minor cleanup, moved stuff in its proper place;
2005-09-17, by wenzelm
generate: added HOL-Complex-Generate-HOLLight;
2005-09-17, by wenzelm
added code generator setup (from Main.thy);
2005-09-17, by wenzelm
lemmas [code] = imp_conv_disj (from Main.thy) -- Why does it need Datatype?
2005-09-17, by wenzelm
HTML.with_charset;
2005-09-17, by wenzelm
converted to Isar theory format;
2005-09-17, by wenzelm
tuned document;
2005-09-17, by wenzelm
obsolete;
2005-09-17, by wenzelm
plain test session, includes example;
2005-09-17, by wenzelm
theory_to_proof: check theory of initial proof state, which must not be changed;
2005-09-17, by wenzelm
added auto_fix (from proof.ML);
2005-09-17, by wenzelm
export put_facts;
2005-09-17, by wenzelm
interpretation: use goal commands without target -- no storing of results;
2005-09-17, by wenzelm
theorem(_i): empty target;
2005-09-17, by wenzelm
pretty_thm_aux: observe asms context;
2005-09-17, by wenzelm
tuned;
2005-09-17, by wenzelm
Cube: converted to Isar, use locales;
2005-09-17, by wenzelm
1) mapped .. and == constants
2005-09-17, by obua
use interpretation command
2005-09-17, by huffman

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

isabelle