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;
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;
wenzelm [Wed, 13 Apr 2005 18:48:19 +0200] rev 15718
*** MESSAGE REFERS TO PREVIOUS VERSION ***
ISABELLE_DOC_FORMAT;
tuned;
wenzelm [Wed, 13 Apr 2005 18:48:05 +0200] rev 15717
*** MESSAGE REFERS TO PREVIOUS VERSION ***
ISABELLE_DOC_FORMAT;
wenzelm [Wed, 13 Apr 2005 18:47:53 +0200] rev 15716
*** MESSAGE REFERS TO PREVIOUS VERSION ***
Sign.prep_ext_merge;
wenzelm [Wed, 13 Apr 2005 18:47:43 +0200] rev 15715
*** MESSAGE REFERS TO PREVIOUS VERSION ***
added datatype interval, improved thm selections;
wenzelm [Wed, 13 Apr 2005 18:47:01 +0200] rev 15714
*** MESSAGE REFERS TO PREVIOUS VERSION ***
removed uterm, added 'maybe';
Attrib.src;
improved thm_sel;
wenzelm [Wed, 13 Apr 2005 18:46:52 +0200] rev 15713
*** MESSAGE REFERS TO PREVIOUS VERSION ***
type src = Args.src;
Drule.add_used;
wenzelm [Wed, 13 Apr 2005 18:46:39 +0200] rev 15712
*** MESSAGE REFERS TO PREVIOUS VERSION ***
removed uterm;
tuned;
wenzelm [Wed, 13 Apr 2005 18:46:30 +0200] rev 15711
*** MESSAGE REFERS TO PREVIOUS VERSION ***
Attrib.src;
ISABELLE_DOC_FORMAT;