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 -96 +96 +100 +300 +1000 +3000 +10000 +30000 tip

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
introduces some modern-style AList operations
2005-09-08, by haftmann
added the_list, the_default
2005-09-08, by haftmann
yet more tidying of Isabelle-ATP link
2005-09-08, by paulson
converted to Isar theory format;
2005-09-07, by wenzelm
converted to Isar theory format;
2005-09-07, by wenzelm
converted to Isar theory format;
2005-09-07, by wenzelm
removed TLA/Inc/Pcount.thy;
2005-09-07, by wenzelm
elimination of watcher.sig
2005-09-07, by paulson
Progress on eprover linkup, also massive tidying
2005-09-07, by paulson
axioms now included in tptp files, no /bin/cat and various tidying
2005-09-07, by paulson
consolidation of watcher.ML and watcher.sig
2005-09-07, by paulson
generalized types more
2005-09-07, by huffman
generalized types
2005-09-07, by huffman
added theorem hypreal_inverse2
2005-09-07, by huffman
replace type hcomplex with complex star
2005-09-07, by huffman
replace type hypnat with nat star
2005-09-07, by huffman
replace type hypreal with real star
2005-09-06, by huffman
add Hyperreal dependencies
2005-09-06, by huffman
class instances for nonstandard types
2005-09-06, by huffman
transfer principle tactic
2005-09-06, by huffman
generic nonstandard type constructor
2005-09-06, by huffman
converted to Isar theory format;
2005-09-06, by wenzelm
fix proof
2005-09-06, by huffman
converted to Isar theory format;
2005-09-06, by wenzelm
reimplement Filter.thy with locales
2005-09-06, by huffman
converted to Isar theory format;
2005-09-06, by wenzelm
converted to Isar theory format;
2005-09-06, by wenzelm
removed some ML files in Modelcheck/;
2005-09-06, by wenzelm
updated;
2005-09-06, by wenzelm
axclass: no longer bind "cI";
2005-09-06, by wenzelm
deprecated old-style infix declarations, which mix name and syntax;
2005-09-06, by wenzelm
tuned msg;
2005-09-06, by wenzelm
AList.defined;
2005-09-06, by wenzelm
name space prefix is now "c_class" instead of just "c";
2005-09-06, by wenzelm
proper treatment of polymorphic sets;
2005-09-06, by wenzelm
tuned comments;
2005-09-06, by wenzelm
converted to Isar theory format;
2005-09-06, by wenzelm
make LocalesTest last, because it sets funny flags;
2005-09-06, by wenzelm
avoid old-style infixes;
2005-09-06, by wenzelm
axclass: name space prefix is now "c_class" instead of just "c";
2005-09-06, by wenzelm
axclass: name space prefix is now "c_class" instead of just "c";
2005-09-06, by wenzelm
unnecessary parentheses removed
2005-09-06, by webertj
converted to Isar theory format;
2005-09-06, by wenzelm
introduced some new-style AList operations
2005-09-06, by haftmann
eliminated 1 call to polyEq
2005-09-06, by haftmann
tuned;
2005-09-05, by wenzelm
updated;
2005-09-05, by wenzelm
obsolete;
2005-09-05, by wenzelm
added assert, command;
2005-09-05, by wenzelm
tuned check_text;
2005-09-05, by wenzelm
chapter/section/subsection/subsubsection/text: optional locale specification;
2005-09-05, by wenzelm
markup commands: optional locale specification;
2005-09-05, by wenzelm
add_chapter/section/subsection/subsubsection/text: optional locale specification;
2005-09-05, by wenzelm
curried_lookup/update;
2005-09-05, by wenzelm
tuned;
2005-09-05, by wenzelm
Markup commands 'chapter' .. 'text' support optional locale specification;
2005-09-05, by wenzelm
removed duplicate theorems;
2005-09-05, by wenzelm
introduced binding priority 1 for linear combinators etc.
2005-09-05, by haftmann
converted to Isar theory format;
2005-09-03, by wenzelm
tuned method;
2005-09-03, by wenzelm
tuned;
2005-09-03, by wenzelm
obsolete;
2005-09-03, by wenzelm
converted to Isar theory format;
2005-09-03, by wenzelm
obsolete (see Cube.thy);
2005-09-03, by wenzelm
tuned msg;
2005-09-03, by wenzelm
uses ("LCF_lemmas.ML");
2005-09-03, by wenzelm
converted to Isar theory format;
2005-09-03, by wenzelm
tuned;
2005-09-03, by wenzelm
removed fix.thy, pair.thy, simpdata.ML;
2005-09-03, by wenzelm
converted to Isar theory format;
2005-09-03, by wenzelm
converted to Isar theory format;
2005-09-03, by wenzelm
setmp print_mode []; more robust outer syntax; tuned;
2005-09-03, by wenzelm
tuned;
2005-09-03, by wenzelm
simplified oracle;
2005-09-03, by wenzelm
use Check.ML;
2005-09-03, by wenzelm

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

isabelle