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