Thu, 14 Apr 2005 08:52:46 +0200 added Makefile and generated files to make document available for makedist
kleing [Thu, 14 Apr 2005 08:52:46 +0200] rev 15728
added Makefile and generated files to make document available for makedist
Wed, 13 Apr 2005 20:20:14 +0200 Locales: proper static binding of attribute syntax;
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;
Wed, 13 Apr 2005 18:51:39 +0200 *** MESSAGE REFERS TO PREVIOUS VERSION ***
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);
Wed, 13 Apr 2005 18:51:28 +0200 *** MESSAGE REFERS TO PREVIOUS VERSION ***
wenzelm [Wed, 13 Apr 2005 18:51:28 +0200] rev 15725
*** MESSAGE REFERS TO PREVIOUS VERSION *** added read_tyname/const;
Wed, 13 Apr 2005 18:50:08 +0200 *** MESSAGE REFERS TO PREVIOUS VERSION ***
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;
Wed, 13 Apr 2005 18:49:42 +0200 *** MESSAGE REFERS TO PREVIOUS VERSION ***
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;
Wed, 13 Apr 2005 18:49:22 +0200 *** MESSAGE REFERS TO PREVIOUS VERSION ***
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;
Wed, 13 Apr 2005 18:49:07 +0200 *** MESSAGE REFERS TO PREVIOUS VERSION ***
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;
Wed, 13 Apr 2005 18:48:52 +0200 *** MESSAGE REFERS TO PREVIOUS VERSION ***
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;
Wed, 13 Apr 2005 18:48:39 +0200 *** MESSAGE REFERS TO PREVIOUS VERSION ***
wenzelm [Wed, 13 Apr 2005 18:48:39 +0200] rev 15719
*** 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;
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip