wenzelm [Sat, 23 Apr 2005 19:49:49 +0200] rev 15825
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
wenzelm [Sat, 23 Apr 2005 19:49:39 +0200] rev 15824
tuned proofs;
wenzelm [Sat, 23 Apr 2005 19:49:26 +0200] rev 15823
removed Pure/Syntax/token_trans.ML Pure/Thy/ROOT.ML Pure/Proof/ROOT.ML Pure/Isar/isar.ML;
wenzelm [Sat, 23 Apr 2005 19:49:16 +0200] rev 15822
_gt, _gt: syntax instead of consts;
wenzelm [Sat, 23 Apr 2005 19:49:08 +0200] rev 15821
cover CPure.- and CPure._ as well;
wenzelm [Sat, 23 Apr 2005 19:49:01 +0200] rev 15820
content moved to outer_syntax.ML;
wenzelm [Sat, 23 Apr 2005 19:48:40 +0200] rev 15819
content moved to Pure/ROOT.ML;
wenzelm [Sat, 23 Apr 2005 19:48:15 +0200] rev 15818
removed obsolete xterm token translations;
paulson [Fri, 22 Apr 2005 17:32:46 +0200] rev 15817
removed last occurrences of OS.Process.sleep
paulson [Fri, 22 Apr 2005 17:32:29 +0200] rev 15816
x-symbol syntax
paulson [Fri, 22 Apr 2005 17:32:03 +0200] rev 15815
tidied
dixon [Fri, 22 Apr 2005 15:10:42 +0200] rev 15814
lucas - fixed a big with renaming of bound variables. Other small changes.
isatest [Fri, 22 Apr 2005 14:15:01 +0200] rev 15813
run smlnj devel on sunbroy2 and stable on atbroy51 until faster machines are around
kleing [Fri, 22 Apr 2005 04:12:24 +0200] rev 15812
added PG hang to FAQ
kleing [Fri, 22 Apr 2005 02:09:10 +0200] rev 15811
tuned
kleing [Fri, 22 Apr 2005 02:03:52 +0200] rev 15810
howto for changing web pages, simplified makefile access
kleing [Fri, 22 Apr 2005 01:48:08 +0200] rev 15809
check in Isabelle2004 versions to make web page changes easier
kleing [Fri, 22 Apr 2005 01:38:13 +0200] rev 15808
updated, added Admin/page after-release maintenance
isatest [Fri, 22 Apr 2005 00:34:15 +0200] rev 15807
wakeonlan for macbroy33
kleing [Fri, 22 Apr 2005 00:31:30 +0200] rev 15806
test stable and devel version of smlnj
wenzelm [Thu, 21 Apr 2005 22:10:12 +0200] rev 15805
adapt theories and ML files to new CPure/Pure arrangement;
wenzelm [Thu, 21 Apr 2005 22:06:18 +0200] rev 15804
The CPure theory -- Pure with alternative application syntax.
wenzelm [Thu, 21 Apr 2005 22:06:00 +0200] rev 15803
The Pure theory.
wenzelm [Thu, 21 Apr 2005 22:04:01 +0200] rev 15802
removed;
wenzelm [Thu, 21 Apr 2005 22:02:06 +0200] rev 15801
superceded by Pure.thy and CPure.thy;
wenzelm [Thu, 21 Apr 2005 22:00:28 +0200] rev 15800
adapt theories and ML files to new CPure/Pure arrangement;
berghofe [Thu, 21 Apr 2005 19:16:19 +0200] rev 15799
Adapted use command to new behaviour of Toplevel.node_trans
berghofe [Thu, 21 Apr 2005 19:13:03 +0200] rev 15798
Adapted to new interface of instantiation and unification / matching functions.
berghofe [Thu, 21 Apr 2005 19:12:03 +0200] rev 15797
- Eliminated nodup_vars check.
- Unification and matching functions now check types of term variables / sorts
of type variables when applying a substitution.
- Thm.instantiate now takes (ctyp * ctyp) list instead of (indexname * ctyp) list
as argument, to allow for proper instantiation of theorems containing
type variables with same name but different sorts.
berghofe [Thu, 21 Apr 2005 19:02:54 +0200] rev 15796
Moved cterm_fun from Thm to Drule.
berghofe [Thu, 21 Apr 2005 18:58:44 +0200] rev 15795
Modified variable index in proof (necessary due to changes in the kernel).
berghofe [Thu, 21 Apr 2005 18:57:18 +0200] rev 15794
Adapted to new interface of instantiation and unification / matching functions.
berghofe [Thu, 21 Apr 2005 18:56:03 +0200] rev 15793
Made inst1_tac more robust against changes of variable indices.
nipkow [Thu, 21 Apr 2005 17:22:23 +0200] rev 15792
fix
nipkow [Thu, 21 Apr 2005 17:22:17 +0200] rev 15791
tuning locales
paulson [Thu, 21 Apr 2005 15:33:30 +0200] rev 15790
removed tracing info
paulson [Thu, 21 Apr 2005 15:05:24 +0200] rev 15789
added hearder lines and deleted some redundant material
paulson [Thu, 21 Apr 2005 13:15:25 +0200] rev 15788
adding the Proof General preview
paulson [Thu, 21 Apr 2005 10:05:06 +0200] rev 15787
improved SML/NJ compatibility, etc.
gagern [Wed, 20 Apr 2005 22:43:52 +0200] rev 15786
Added op in front of constructor for better parsing.
gagern [Wed, 20 Apr 2005 22:37:29 +0200] rev 15785
Fix automatic determination of poly version.
gagern [Wed, 20 Apr 2005 19:00:30 +0200] rev 15784
removed redundant readlink call
webertj [Wed, 20 Apr 2005 18:57:05 +0200] rev 15783
call to Array.modifyi replaced
quigley [Wed, 20 Apr 2005 18:01:50 +0200] rev 15782
Corrected the problem with the ATP directory.
nipkow [Wed, 20 Apr 2005 17:19:42 +0200] rev 15781
Used locale interpretations everywhere. -> lemma had new name
nipkow [Wed, 20 Apr 2005 17:19:18 +0200] rev 15780
Used locale interpretations everywhere.
quigley [Wed, 20 Apr 2005 16:03:17 +0200] rev 15779
Removed remaining references to Main.thy in reconstruction code.
gagern [Wed, 20 Apr 2005 14:18:33 +0200] rev 15778
Allow symlinks to shell scripts
kleing [Wed, 20 Apr 2005 00:45:54 +0200] rev 15777
added locale instantiation
webertj [Tue, 19 Apr 2005 18:46:04 +0200] rev 15776
refute extended
paulson [Tue, 19 Apr 2005 18:08:55 +0200] rev 15775
syntax fix
paulson [Tue, 19 Apr 2005 18:08:44 +0200] rev 15774
more tidying of libraries in Reconstruction
quigley [Tue, 19 Apr 2005 15:15:06 +0200] rev 15773
Completed integration of reconstruction code. Now finds and displays proofs when used with modified version
of Proof General. C.Q.
paulson [Tue, 19 Apr 2005 13:35:01 +0200] rev 15772
auto update
paulson [Tue, 19 Apr 2005 13:34:50 +0200] rev 15771
restored the target HOL-Complex-Import
paulson [Tue, 19 Apr 2005 11:40:23 +0200] rev 15770
fixed presentation
obua [Tue, 19 Apr 2005 10:59:31 +0200] rev 15769
Removed mult_commute axiom from comm_semiring axclass.
webertj [Tue, 19 Apr 2005 00:14:27 +0200] rev 15768
compilation error fixed
webertj [Mon, 18 Apr 2005 17:20:49 +0200] rev 15767
support for recursion over mutually recursive IDTs
ballarin [Mon, 18 Apr 2005 15:54:23 +0200] rev 15766
Cleaned up, now use interpretation.
ballarin [Mon, 18 Apr 2005 15:53:51 +0200] rev 15765
Cleaned up, now uses interpretation.
paulson [Mon, 18 Apr 2005 10:36:05 +0200] rev 15764
deleted obsolete code
ballarin [Mon, 18 Apr 2005 09:25:23 +0200] rev 15763
Interpretation supports statically scoped attributes; documentation.
wenzelm [Sun, 17 Apr 2005 19:40:43 +0200] rev 15762
updated;
wenzelm [Sun, 17 Apr 2005 19:40:34 +0200] rev 15761
added delete_safe, insert, remove, remove_multi;
tuned;
wenzelm [Sun, 17 Apr 2005 19:39:39 +0200] rev 15760
clarified insert/remove;
tuned canonical fold/fold_rev;
wenzelm [Sun, 17 Apr 2005 19:39:11 +0200] rev 15759
tuned;
wenzelm [Sun, 17 Apr 2005 19:38:53 +0200] rev 15758
binds/thms: do not store options, but delete from table;
tuned;
wenzelm [Sun, 17 Apr 2005 19:38:40 +0200] rev 15757
tuned comments;
wenzelm [Sun, 17 Apr 2005 19:38:30 +0200] rev 15756
removed;
wenzelm [Sat, 16 Apr 2005 18:58:55 +0200] rev 15755
expect translations functions to be stamped already;
added remove_const_gram;
wenzelm [Sat, 16 Apr 2005 18:58:30 +0200] rev 15754
added stamp_trfun, mk_trfun, eq_trfun;
wenzelm [Sat, 16 Apr 2005 18:58:18 +0200] rev 15753
tuned extend_prtabs;
added remove_prtabs;
wenzelm [Sat, 16 Apr 2005 18:58:09 +0200] rev 15752
added make_gram;
merge_gram: do not add chain productions to prods;
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;
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!);