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;
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;
wenzelm [Wed, 13 Apr 2005 18:46:22 +0200] rev 15710
*** MESSAGE REFERS TO PREVIOUS VERSION ***
Scan.peek;
Args.global/local_const/tyname (static binding!);
wenzelm [Wed, 13 Apr 2005 18:46:12 +0200] rev 15709
*** MESSAGE REFERS TO PREVIOUS VERSION ***
use args.ML, attrib.ML earlier;
wenzelm [Wed, 13 Apr 2005 18:46:04 +0200] rev 15708
*** MESSAGE REFERS TO PREVIOUS VERSION ***
Scan.peek;
Args.local_tyname, Args.local_const;
wenzelm [Wed, 13 Apr 2005 18:45:52 +0200] rev 15707
*** MESSAGE REFERS TO PREVIOUS VERSION ***
Method.src;
wenzelm [Wed, 13 Apr 2005 18:45:38 +0200] rev 15706
*** MESSAGE REFERS TO PREVIOUS VERSION ***
Args.global_const (static binding!);
wenzelm [Wed, 13 Apr 2005 18:45:25 +0200] rev 15705
*** MESSAGE REFERS TO PREVIOUS VERSION ***
Attrib.src;
wenzelm [Wed, 13 Apr 2005 18:45:09 +0200] rev 15704
*** MESSAGE REFERS TO PREVIOUS VERSION ***
Attrib.src;
Args.maybe;
wenzelm [Wed, 13 Apr 2005 18:34:22 +0200] rev 15703
*** empty log message ***
paulson [Wed, 13 Apr 2005 09:48:41 +0200] rev 15702
new signalling primmitives for sml/nj compatibility
nipkow [Tue, 12 Apr 2005 13:38:08 +0200] rev 15701
*** empty log message ***
paulson [Tue, 12 Apr 2005 11:08:25 +0200] rev 15700
tweaks mainly to achieve sml/nj compatibility
paulson [Tue, 12 Apr 2005 11:07:42 +0200] rev 15699
fixing an incompatibility with Posix.IO.mkTextReader
paulson [Mon, 11 Apr 2005 16:25:53 +0200] rev 15698
auto update
paulson [Mon, 11 Apr 2005 16:25:31 +0200] rev 15697
removal of Main and other tidying up
ballarin [Mon, 11 Apr 2005 12:34:34 +0200] rev 15696
First release of interpretation commands.
nipkow [Mon, 11 Apr 2005 12:18:27 +0200] rev 15695
tuned
nipkow [Mon, 11 Apr 2005 12:14:48 +0200] rev 15694
added \restriction
nipkow [Mon, 11 Apr 2005 12:14:23 +0200] rev 15693
tuned Map, renamed lex stuff in List.
nipkow [Sun, 10 Apr 2005 17:20:03 +0200] rev 15692
Added lots of AMS harpoons
nipkow [Sun, 10 Apr 2005 17:19:03 +0200] rev 15691
_(_|_) is now override_on
nipkow [Sun, 10 Apr 2005 11:42:07 +0200] rev 15690
tuned
nipkow [Sun, 10 Apr 2005 11:41:29 +0200] rev 15689
section on qmark
paulson [Sat, 09 Apr 2005 16:27:11 +0200] rev 15688
fixed the syntax of infix declarations
wenzelm [Sat, 09 Apr 2005 15:36:02 +0200] rev 15687
thmref: selection syntax;
wenzelm [Sat, 09 Apr 2005 15:35:37 +0200] rev 15686
update syntax of 'where' and 'of';
wenzelm [Sat, 09 Apr 2005 15:34:38 +0200] rev 15685
added PDF_VIEWER, ISABELLE_DOC_FORMAT;
paulson [Fri, 08 Apr 2005 18:43:39 +0200] rev 15684
Reconstruction code, now packaged to avoid name clashes
paulson [Fri, 08 Apr 2005 10:50:02 +0200] rev 15683
temporarily removed ATP code
paulson [Thu, 07 Apr 2005 18:44:45 +0200] rev 15682
removed bad code
quigley [Thu, 07 Apr 2005 18:35:21 +0200] rev 15681
Changed prob1.dfg to prob_1.dfg
quigley [Thu, 07 Apr 2005 18:33:56 +0200] rev 15680
Got rid of Main.thy reference
quigley [Thu, 07 Apr 2005 18:20:04 +0200] rev 15679
Integrating the reconstruction files into the building of HOL
quigley [Thu, 07 Apr 2005 17:45:51 +0200] rev 15678
Reconstruction.thy and IsaMakefile updated
nipkow [Thu, 07 Apr 2005 14:07:40 +0200] rev 15677
*** empty log message ***
paulson [Thu, 07 Apr 2005 13:29:41 +0200] rev 15676
new meta-level rules
nipkow [Thu, 07 Apr 2005 10:22:55 +0200] rev 15675
*** empty log message ***
wenzelm [Thu, 07 Apr 2005 09:51:17 +0200] rev 15674
reverted renaming of Some/None in comments and strings;
wenzelm [Thu, 07 Apr 2005 09:28:16 +0200] rev 15673
added term_8;
wenzelm [Thu, 07 Apr 2005 09:28:03 +0200] rev 15672
added get_axiom_i, invoke_oracle_i;