Thu, 01 Feb 2007 20:59:50 +0100 wenzelm tuned;
Thu, 01 Feb 2007 20:40:34 +0100 wenzelm proper use of PureThy.has_name_hint instead of hard-wired string'';
Thu, 01 Feb 2007 20:40:17 +0100 wenzelm removed non-modular comment;
Thu, 01 Feb 2007 13:41:19 +0100 paulson new theorem int_infinite
Wed, 31 Jan 2007 20:07:40 +0100 aspinall Fix tell_thm_deps to match changse in PureThy.
Wed, 31 Jan 2007 20:06:24 +0100 aspinall Expose hard-wired string which was changed and broke Proof General.
Wed, 31 Jan 2007 16:05:17 +0100 haftmann clarified error message
Wed, 31 Jan 2007 16:05:16 +0100 haftmann clarified command annotation
Wed, 31 Jan 2007 16:05:14 +0100 haftmann changed cong alist - now using AList operations instead of overwrite_warn
Wed, 31 Jan 2007 16:05:13 +0100 haftmann dropped Output.update_warn
Wed, 31 Jan 2007 16:05:12 +0100 haftmann print translation for record types with empty-sorted type variables raise Match instead of producing an error
Wed, 31 Jan 2007 16:05:10 +0100 haftmann dropped lemma duplicates in HOL.thy
Wed, 31 Jan 2007 14:03:31 +0100 paulson Tidying; more debugging information. New reference unwanted_types.
Tue, 30 Jan 2007 13:17:02 +0100 aspinall Tweak preferences for PGIP interfaces. Make <askids> return theory successors instead of parents (ideally should be content elements).
Tue, 30 Jan 2007 13:16:58 +0100 aspinall Add get_succs
Tue, 30 Jan 2007 13:14:41 +0100 aspinall Add operations on preference tables (remove, set_default).
Tue, 30 Jan 2007 08:21:23 +0100 haftmann adjusted to new codegen_funcgr interface
Tue, 30 Jan 2007 08:21:22 +0100 haftmann added interface for plugging in preprocessors
Tue, 30 Jan 2007 08:21:19 +0100 haftmann additional auxiliary here
Tue, 30 Jan 2007 08:21:18 +0100 haftmann whitespace tuning
Tue, 30 Jan 2007 08:21:17 +0100 haftmann dropped dead code
Tue, 30 Jan 2007 08:21:16 +0100 haftmann shifted import order
Tue, 30 Jan 2007 08:21:15 +0100 haftmann dropped whitespace
Tue, 30 Jan 2007 08:21:13 +0100 haftmann changed name of interpretation linorder to order
Mon, 29 Jan 2007 19:58:14 +0100 wenzelm proper simproc_setup;
Mon, 29 Jan 2007 19:58:14 +0100 wenzelm added get_simproc, @{simproc};
Sun, 28 Jan 2007 23:29:17 +0100 wenzelm added interface for target_naming;
Sun, 28 Jan 2007 23:29:16 +0100 wenzelm added simproc_setup;
Sun, 28 Jan 2007 23:29:15 +0100 wenzelm added def_simproc(_i) -- define named simprocs;
Sun, 28 Jan 2007 23:29:14 +0100 wenzelm updated;
Sun, 28 Jan 2007 11:52:52 +0100 chaieb Now deals with simples cases where the input equations contain type variables
Fri, 26 Jan 2007 13:59:06 +0100 haftmann refined algorithm
Fri, 26 Jan 2007 13:59:04 +0100 haftmann clarified code
Fri, 26 Jan 2007 13:59:03 +0100 haftmann exported interface for explicit error messages
Fri, 26 Jan 2007 13:59:02 +0100 haftmann added NestedEnvironment
Fri, 26 Jan 2007 10:48:09 +0100 paulson Improved debugging
Fri, 26 Jan 2007 10:46:22 +0100 paulson Streamlined and improved debugging messages
Fri, 26 Jan 2007 10:46:15 +0100 nipkow more fixes of arithmetic for min/max.
Fri, 26 Jan 2007 10:24:33 +0100 paulson min/max lemmas (actually unused!)
Fri, 26 Jan 2007 10:24:12 +0100 paulson simplification of Suc/numeral combinations with min, max
Fri, 26 Jan 2007 10:22:42 +0100 paulson Fixed long-standing, MAJOR bug in "lt"
Fri, 26 Jan 2007 09:24:35 +0100 haftmann adjusted manual to improved treatment of overloaded constants
Thu, 25 Jan 2007 16:57:57 +0100 nipkow Allows evaluation of min/max o numerals.
Thu, 25 Jan 2007 09:32:56 +0100 haftmann fixed bug for OCaml bigints
Thu, 25 Jan 2007 09:32:51 +0100 haftmann tuned
Thu, 25 Jan 2007 09:32:50 +0100 haftmann added explicit maintainance of coregular code theorems for overloaded constants
Thu, 25 Jan 2007 09:32:49 +0100 haftmann dropped useless stuff
Thu, 25 Jan 2007 09:32:48 +0100 haftmann clarified code
Thu, 25 Jan 2007 09:32:46 +0100 haftmann added explicit query function for arities to subalgebra projection
Thu, 25 Jan 2007 09:32:45 +0100 haftmann not importing NestedEnvironment
Thu, 25 Jan 2007 09:32:42 +0100 haftmann adjusted to changes in class package
Thu, 25 Jan 2007 09:32:37 +0100 haftmann made executable
Thu, 25 Jan 2007 09:32:36 +0100 haftmann improved
Thu, 25 Jan 2007 09:32:35 +0100 haftmann fxied bug for OCaml bigints
Thu, 25 Jan 2007 09:32:34 +0100 haftmann adjusted names
Wed, 24 Jan 2007 20:54:21 +0100 wenzelm tuned eta_contract;
Wed, 24 Jan 2007 20:54:20 +0100 wenzelm updated timing;
Wed, 24 Jan 2007 17:10:50 +0100 paulson some new lemmas
Wed, 24 Jan 2007 13:15:16 +0100 aspinall Let <loadfile> execute even while a file is open interactively.
Tue, 23 Jan 2007 20:29:03 +0100 krauss fixes smlnj-related problem, updated signature
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip