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

introduces AList.lookup
2005-09-14, by haftmann
removed duplicated lemmas; convert more proofs to transfer principle
2005-09-14, by huffman
add theorem chain_const
2005-09-13, by huffman
tuned;
2005-09-13, by wenzelm
global quick_and_dirty;
2005-09-13, by wenzelm
Printing of Isar proof elements etc.
2005-09-13, by wenzelm
Non-empty stacks.
2005-09-13, by wenzelm
IsarThy.begin_theory;
2005-09-13, by wenzelm
export ml_exts;
2005-09-13, by wenzelm
begin_theory: tuned interface, check uses;
2005-09-13, by wenzelm
replaced TRANSLATION_FAIL by EXCEPTION;
2005-09-13, by wenzelm
added three_buffersN, print3;
2005-09-13, by wenzelm
load before proof.ML;
2005-09-13, by wenzelm
added simple;
2005-09-13, by wenzelm
added add_view, export_view (supercedes adhoc view arguments);
2005-09-13, by wenzelm
major cleanup of interfaces and implementation;
2005-09-13, by wenzelm
added name_facts;
2005-09-13, by wenzelm
tuned Isar proof elements;
2005-09-13, by wenzelm
added cheating, sorry_text (from skip_proofs.ML);
2005-09-13, by wenzelm
load late, after proof.ML;
2005-09-13, by wenzelm
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
2005-09-13, by wenzelm
cleanup parsers and interfaces;
2005-09-13, by wenzelm
Proof.get_thmss;
2005-09-13, by wenzelm
tuned;
2005-09-13, by wenzelm
more self-contained proof elements (material from isar_thy.ML);
2005-09-13, by wenzelm
added cases, rule_contextN;
2005-09-13, by wenzelm
load locale.ML late (after proof.ML);
2005-09-13, by wenzelm
added maps, map_list, lift, lifts;
2005-09-13, by wenzelm
added stack.ML;
2005-09-13, by wenzelm
added simple_fact;
2005-09-13, by wenzelm
Seq.maps;
2005-09-13, by wenzelm
added hide_names(_i) (from isar_thy.ML);
2005-09-13, by wenzelm
added generic_setup, add_oracle (from isar_thy.ML);
2005-09-13, by wenzelm
added exception EXCEPTION of exn * string;
2005-09-13, by wenzelm
replaced DATA_FAIL by EXCEPTION;
2005-09-13, by wenzelm
tuned Isar interfaces;
2005-09-13, by wenzelm
added General/stack.ML, Isar/proof_display.ML;
2005-09-13, by wenzelm
the_list (cf. Pure/library.ML);
2005-09-13, by wenzelm
tuned IsarThy.theorem_i;
2005-09-13, by wenzelm
fixed INST: has same semantic now as INST_TYPE for repetitions
2005-09-13, by obua
list of constants and theorems whose names have been changed or merged
2005-09-12, by huffman
add header
2005-09-12, by huffman
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
2005-09-12, by huffman
updated to work with latest HOL-Complex
2005-09-12, by huffman
add file Hyperreal/transfer.ML
2005-09-12, by huffman
new implementation of transfer principle
2005-09-12, by huffman
removed clutter
2005-09-12, by obua
name conflict with global itrev resolved
2005-09-12, by nipkow
dealt with name clash with List.itrev
2005-09-12, by nipkow
introduced new-style AList operations
2005-09-12, by haftmann
introduced internal function hthm2thm
2005-09-12, by obua
1) Added target HOL-Complex-Generate-HOLLight
2005-09-12, by obua
Added HOLLight support to importer.
2005-09-12, by obua
added interact flag to control mode of excursions;
2005-09-12, by wenzelm
excursion: interactive if debug;
2005-09-11, by wenzelm
updated to work with new HOL-Complex version
2005-09-09, by huffman
starfun, starset, and other functions on NS types are now polymorphic;
2005-09-09, by huffman
Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
2005-09-09, by paulson
fixed printing of locales
2005-09-09, by ballarin
consolidation of duplicate code in Isabelle-ATP linkup
2005-09-08, by paulson

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

isabelle