wenzelm [Sat, 16 Apr 2005 18:57:53 +0200] rev 15751
identify binder translations only once (admits remove);
wenzelm [Sat, 16 Apr 2005 18:57:39 +0200] rev 15750
Syntax.mk_trfun;
wenzelm [Sat, 16 Apr 2005 18:57:18 +0200] rev 15749
tuned (t)inst_tab_elem;
wenzelm [Sat, 16 Apr 2005 18:56:48 +0200] rev 15748
added 'no_syntax' command;
wenzelm [Sat, 16 Apr 2005 18:56:37 +0200] rev 15747
added del_modesyntax(_i);
wenzelm [Sat, 16 Apr 2005 18:56:21 +0200] rev 15746
added del_modesyntax(_i);
added print_all_data;
wenzelm [Sat, 16 Apr 2005 18:55:51 +0200] rev 15745
added gen_remove, remove;
usual arrangement BasicLibrary: BASIC_LIBRARY and Library: LIBRARY;
wenzelm [Sat, 16 Apr 2005 18:55:28 +0200] rev 15744
Pure: command 'no_syntax' removes grammar declarations;
wenzelm [Sat, 16 Apr 2005 18:54:44 +0200] rev 15743
removed;
huffman [Sat, 16 Apr 2005 00:17:52 +0200] rev 15742
speed improvements for the domain package
huffman [Sat, 16 Apr 2005 00:16:44 +0200] rev 15741
New file for theorems used by the domain package
nipkow [Fri, 15 Apr 2005 18:43:35 +0200] rev 15740
rermoved pointless example
paulson [Fri, 15 Apr 2005 18:16:05 +0200] rev 15739
yet more tidying up: removal of some references to Main
nipkow [Fri, 15 Apr 2005 17:03:35 +0200] rev 15738
*** empty log message ***
nipkow [Fri, 15 Apr 2005 14:14:24 +0200] rev 15737
New
paulson [Fri, 15 Apr 2005 13:35:53 +0200] rev 15736
more tidying up of the SPASS interface
ballarin [Fri, 15 Apr 2005 12:00:00 +0200] rev 15735
Removed most of the atp interface from Pure.
aspinall [Thu, 14 Apr 2005 19:30:57 +0200] rev 15734
Include automatic determination of poly version.
aspinall [Thu, 14 Apr 2005 19:16:07 +0200] rev 15733
Add RDISTDIR option used by Isabelle RPM.
nipkow [Thu, 14 Apr 2005 17:57:23 +0200] rev 15732
Added thm names
nipkow [Thu, 14 Apr 2005 17:57:04 +0200] rev 15731
Removed dir Orderings in Library
kleing [Thu, 14 Apr 2005 09:19:55 +0200] rev 15730
fix: added path to garbage
kleing [Thu, 14 Apr 2005 08:56:08 +0200] rev 15729
added LaTeXsugar
kleing [Thu, 14 Apr 2005 08:52:46 +0200] rev 15728
added Makefile and generated files to make document available for makedist
wenzelm [Wed, 13 Apr 2005 20:20:14 +0200] rev 15727
Locales: proper static binding of attribute syntax;
Attributes 'induct' and 'cases': support local type or set names;
wenzelm [Wed, 13 Apr 2005 18:51:39 +0200] rev 15726
*** 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);
wenzelm [Wed, 13 Apr 2005 18:51:28 +0200] rev 15725
*** MESSAGE REFERS TO PREVIOUS VERSION ***
added read_tyname/const;
wenzelm [Wed, 13 Apr 2005 18:50:08 +0200] rev 15724
*** MESSAGE REFERS TO PREVIOUS VERSION ***
ISABELLE_DOC_FORMAT setting specifies preferred document format;
some cleanup;
wenzelm [Wed, 13 Apr 2005 18:49:42 +0200] rev 15723
*** 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;
wenzelm [Wed, 13 Apr 2005 18:49:22 +0200] rev 15722
*** 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;
wenzelm [Wed, 13 Apr 2005 18:49:07 +0200] rev 15721
*** 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;
wenzelm [Wed, 13 Apr 2005 18:48:52 +0200] rev 15720
*** 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;