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;
Wed, 13 Apr 2005 18:48:19 +0200 *** MESSAGE REFERS TO PREVIOUS VERSION ***
wenzelm [Wed, 13 Apr 2005 18:48:19 +0200] rev 15718
*** MESSAGE REFERS TO PREVIOUS VERSION *** ISABELLE_DOC_FORMAT; tuned;
Wed, 13 Apr 2005 18:48:05 +0200 *** MESSAGE REFERS TO PREVIOUS VERSION ***
wenzelm [Wed, 13 Apr 2005 18:48:05 +0200] rev 15717
*** MESSAGE REFERS TO PREVIOUS VERSION *** ISABELLE_DOC_FORMAT;
Wed, 13 Apr 2005 18:47:53 +0200 *** MESSAGE REFERS TO PREVIOUS VERSION ***
wenzelm [Wed, 13 Apr 2005 18:47:53 +0200] rev 15716
*** MESSAGE REFERS TO PREVIOUS VERSION *** Sign.prep_ext_merge;
Wed, 13 Apr 2005 18:47:43 +0200 *** MESSAGE REFERS TO PREVIOUS VERSION ***
wenzelm [Wed, 13 Apr 2005 18:47:43 +0200] rev 15715
*** MESSAGE REFERS TO PREVIOUS VERSION *** added datatype interval, improved thm selections;
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip