2005-04-20 gagern 2005-04-20 Allow symlinks to shell scripts
2005-04-20 kleing 2005-04-20 added locale instantiation
2005-04-19 webertj 2005-04-19 refute extended
2005-04-19 paulson 2005-04-19 syntax fix
2005-04-19 paulson 2005-04-19 more tidying of libraries in Reconstruction
2005-04-19 quigley 2005-04-19 Completed integration of reconstruction code. Now finds and displays proofs when used with modified version of Proof General. C.Q.
2005-04-19 paulson 2005-04-19 auto update
2005-04-19 paulson 2005-04-19 restored the target HOL-Complex-Import
2005-04-19 paulson 2005-04-19 fixed presentation
2005-04-19 obua 2005-04-19 Removed mult_commute axiom from comm_semiring axclass.
2005-04-19 webertj 2005-04-19 compilation error fixed
2005-04-18 webertj 2005-04-18 support for recursion over mutually recursive IDTs
2005-04-18 ballarin 2005-04-18 Cleaned up, now use interpretation.
2005-04-18 ballarin 2005-04-18 Cleaned up, now uses interpretation.
2005-04-18 paulson 2005-04-18 deleted obsolete code
2005-04-18 ballarin 2005-04-18 Interpretation supports statically scoped attributes; documentation.
2005-04-17 wenzelm 2005-04-17 updated;
2005-04-17 wenzelm 2005-04-17 added delete_safe, insert, remove, remove_multi; tuned;
2005-04-17 wenzelm 2005-04-17 clarified insert/remove; tuned canonical fold/fold_rev;
2005-04-17 wenzelm 2005-04-17 tuned;
2005-04-17 wenzelm 2005-04-17 binds/thms: do not store options, but delete from table; tuned;
2005-04-17 wenzelm 2005-04-17 tuned comments;
2005-04-17 wenzelm 2005-04-17 removed;
2005-04-16 wenzelm 2005-04-16 expect translations functions to be stamped already; added remove_const_gram;
2005-04-16 wenzelm 2005-04-16 added stamp_trfun, mk_trfun, eq_trfun;
2005-04-16 wenzelm 2005-04-16 tuned extend_prtabs; added remove_prtabs;
2005-04-16 wenzelm 2005-04-16 added make_gram; merge_gram: do not add chain productions to prods;
2005-04-16 wenzelm 2005-04-16 identify binder translations only once (admits remove);
2005-04-16 wenzelm 2005-04-16 Syntax.mk_trfun;
2005-04-16 wenzelm 2005-04-16 tuned (t)inst_tab_elem;
2005-04-16 wenzelm 2005-04-16 added 'no_syntax' command;
2005-04-16 wenzelm 2005-04-16 added del_modesyntax(_i);
2005-04-16 wenzelm 2005-04-16 added del_modesyntax(_i); added print_all_data;
2005-04-16 wenzelm 2005-04-16 added gen_remove, remove; usual arrangement BasicLibrary: BASIC_LIBRARY and Library: LIBRARY;
2005-04-16 wenzelm 2005-04-16 Pure: command 'no_syntax' removes grammar declarations;
2005-04-16 wenzelm 2005-04-16 removed;
2005-04-16 huffman 2005-04-16 speed improvements for the domain package
2005-04-16 huffman 2005-04-16 New file for theorems used by the domain package
2005-04-15 nipkow 2005-04-15 rermoved pointless example
2005-04-15 paulson 2005-04-15 yet more tidying up: removal of some references to Main
2005-04-15 nipkow 2005-04-15 *** empty log message ***
2005-04-15 nipkow 2005-04-15 New
2005-04-15 paulson 2005-04-15 more tidying up of the SPASS interface
2005-04-15 ballarin 2005-04-15 Removed most of the atp interface from Pure.
2005-04-14 aspinall 2005-04-14 Include automatic determination of poly version.
2005-04-14 aspinall 2005-04-14 Add RDISTDIR option used by Isabelle RPM.
2005-04-14 nipkow 2005-04-14 Added thm names
2005-04-14 nipkow 2005-04-14 Removed dir Orderings in Library
2005-04-14 kleing 2005-04-14 fix: added path to garbage
2005-04-14 kleing 2005-04-14 added LaTeXsugar
2005-04-14 kleing 2005-04-14 added Makefile and generated files to make document available for makedist
2005-04-13 wenzelm 2005-04-13 Locales: proper static binding of attribute syntax; Attributes 'induct' and 'cases': support local type or set names;
2005-04-13 wenzelm 2005-04-13 *** MESSAGE REFERS TO PREVIOUS VERSION *** support embedded values and static binding -- via implicit assignment to src tokens (cf. assignable/assign/closure); renamed ident/string/keyword to mk_ident/mk_string/mk_keyword; added mk_name, mk_typ, mk_term, mk_fact, mk_attribute; added type value with map_values etc.; removed name_dummy, added general 'maybe' combinator; added global/local_tyname/const; added pretty_src, pretty_attribs; added thm_sel (from attrib.ML);
2005-04-13 wenzelm 2005-04-13 *** MESSAGE REFERS TO PREVIOUS VERSION *** added read_tyname/const;
2005-04-13 wenzelm 2005-04-13 *** MESSAGE REFERS TO PREVIOUS VERSION *** ISABELLE_DOC_FORMAT setting specifies preferred document format; some cleanup;
2005-04-13 wenzelm 2005-04-13 *** MESSAGE REFERS TO PREVIOUS VERSION *** added declared_tyname/const and read_tyname/const; removed certify_tyname/const; added prep_ext_merge, nontriv_merge kept internal; efficient subsig test;
2005-04-13 wenzelm 2005-04-13 *** MESSAGE REFERS TO PREVIOUS VERSION *** Attrib.src; removed Locale.multi_attribute (pass Attrib.src instead); removed interpret(_i) (use have_i instead); goals: more uniform treatment of after_qed, removed separate thy_mod of global goals;
2005-04-13 wenzelm 2005-04-13 *** MESSAGE REFERS TO PREVIOUS VERSION *** removed type multi_attribute (store Attrib.src instead); datatype elem/element(_i): Attrib.src instead of 'att; removed map_attrib_element etc.; added intern_attrib_elem(_expr); added map_elem, map_values to economize code; static binding of values in Attrib.src (cf. Args.closure, Attrib.crude_closure); prep_facts: transfer internal facts;
2005-04-13 wenzelm 2005-04-13 *** MESSAGE REFERS TO PREVIOUS VERSION *** Attrib.src, Method.src; Sign.declared_tyname/const; no Attrib.multi_attribute, pass Attrib.src directly to locales; register_locally: Proof.interpret_i replaced by Proof.have_i;
2005-04-13 wenzelm 2005-04-13 *** MESSAGE REFERS TO PREVIOUS VERSION *** type src = Args.src; renamed local_attribute' to context_attribute; added _i versions of global/local/context_attribute and separate intern/intern_src; added crude_closure to produce argument closure without knowing facts in advance; added 'attribute' to embed internal attributes into src; removed multi_attribute etc.; moved thm_sel to args.ML; Scan.peek; read_instantiate/'where'/'of': support arbitrary mix of external / internal typ / term args, with proper treatment of static binding;