2013-11-19 wenzelm 2013-11-19 proper theory name vs. node name;
2013-11-19 wenzelm 2013-11-19 clarified boundary cases of Document.Node.Name;
2013-11-18 wenzelm 2013-11-18 clarified Thy_Load.node_name;
2013-11-18 wenzelm 2013-11-18 inline blobs into command, via SHA1 digest; broadcast all blobs within edit, without storing the result;
2013-11-18 wenzelm 2013-11-18 persistent value;
2013-11-18 wenzelm 2013-11-18 caching of blob; precise file content according to jEdit IO;
2013-11-18 wenzelm 2013-11-18 tuned;
2013-11-18 wenzelm 2013-11-18 maintain document model for all files, with document view for theory only, and special blob for non-theory files;
2013-11-20 nipkow 2013-11-20 tuned
2013-11-19 blanchet 2013-11-19 whitespace tuning
2013-11-19 blanchet 2013-11-19 tuning
2013-11-19 blanchet 2013-11-19 more refactoring to accommodate SMT proofs
2013-11-19 blanchet 2013-11-19 tuning
2013-11-19 blanchet 2013-11-19 tuning
2013-11-19 haftmann 2013-11-19 more correct NEWS
2013-11-19 blanchet 2013-11-19 simplified old code
2013-11-19 blanchet 2013-11-19 refactoring
2013-11-19 blanchet 2013-11-19 refactoring
2013-11-19 hoelzl 2013-11-19 merged
2013-11-18 hoelzl 2013-11-18 BNF/Examples/Stream: rename same to sconst; define same, fromN in terms of siterate
2013-11-18 hoelzl 2013-11-18 add lemmas Suc_funpow and id_funpow to simpset; add lemma map_add_upt
2013-11-19 blanchet 2013-11-19 refactored
2013-11-19 blanchet 2013-11-19 updated docs
2013-11-19 blanchet 2013-11-19 use type suffixes instead of prefixes for 'case', '(un)fold', '(co)rec'
2013-11-19 blanchet 2013-11-19 prefix internal names as well
2013-11-19 blanchet 2013-11-19 case_if -> case_eq_if + docs
2013-11-19 blanchet 2013-11-19 use suffix '_list' etc. instead of prefix 'list_' for constants not present in the old package
2013-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
2013-11-19 blanchet 2013-11-19 more tuning for speed
2013-11-19 blanchet 2013-11-19 tuning
2013-11-19 blanchet 2013-11-19 tuned proofs
2013-11-19 blanchet 2013-11-19 killed more needless theorems
2013-11-19 blanchet 2013-11-19 killed unused lemmas
2013-11-19 blanchet 2013-11-19 optimized more bad apples
2013-11-19 blanchet 2013-11-19 optimized 'bad apple' method calls
2013-11-18 blanchet 2013-11-18 compile
2013-11-18 blanchet 2013-11-18 no need for 3-way split with GFP for a handful of theorems
2013-11-18 blanchet 2013-11-18 moved more theorems out of LFP
2013-11-18 blanchet 2013-11-18 moved theorems out of LFP
2013-11-18 blanchet 2013-11-18 moved theorems out of LFP
2013-11-18 blanchet 2013-11-18 moved theorems out of LFP
2013-11-18 blanchet 2013-11-18 moved theorems out of LFP
2013-11-18 blanchet 2013-11-18 split 'Cardinal_Arithmetic' 3-way
2013-11-18 blanchet 2013-11-18 started three-way split of 'HOL-Cardinals'
2013-11-18 blanchet 2013-11-18 send output of "tptp_translate" to standard output, to simplify Geoff Sutcliffe's life
2013-11-18 traytel 2013-11-18 merged
2013-11-18 traytel 2013-11-18 show all involved subtyping constraints that cause coercion inference to fail
2013-11-18 hoelzl 2013-11-18 additional lemmas in BNF/Examples/Stream
2013-11-18 traytel 2013-11-18 reintroduced e2d08b9c9047, lost in 54e290da6da8 + e13b0c88c798
2013-11-18 nipkow 2013-11-18 comments by Sean Seefried
2013-11-17 wenzelm 2013-11-17 more robust example;
2013-11-17 wenzelm 2013-11-17 tuned proofs;
2013-11-17 wenzelm 2013-11-17 tuned;
2013-11-17 wenzelm 2013-11-17 tuned proofs;
2013-11-17 wenzelm 2013-11-17 explicit indication of thy_load commands;
2013-11-17 wenzelm 2013-11-17 centralized management of pending buffer edits;
2013-11-17 nipkow 2013-11-17 merged
2013-11-16 nipkow 2013-11-16 added functions all and exists to IArray
2013-11-16 wenzelm 2013-11-16 prefer explicit "document" flag -- eliminated stateful Present.no_document;
2013-11-16 wenzelm 2013-11-16 simplified HTML linefeed (again, see 041dc6d8d344);