Tue, 23 Jan 2007 20:29:03 +0100 krauss fixes smlnj-related problem, updated signature
Tue, 23 Jan 2007 15:54:22 +0100 dixon added a fold up and fold down as separate functions and fixed zipto to
Mon, 22 Jan 2007 19:00:29 +0100 nipkow simplified proofs
Mon, 22 Jan 2007 18:17:04 +0100 krauss Included ex/Fundefs.thy in HOL-ex session
Mon, 22 Jan 2007 17:29:43 +0100 krauss * Preliminary implementation of tail recursion
Mon, 22 Jan 2007 16:53:33 +0100 aspinall Add location_of_position. Needs work elsewhere.
Mon, 22 Jan 2007 16:52:26 +0100 aspinall Test askref
Mon, 22 Jan 2007 16:52:02 +0100 aspinall Expose currently open file
Mon, 22 Jan 2007 16:51:29 +0100 aspinall Sync location with pgip.rnc, fixing attribute names
Mon, 22 Jan 2007 15:37:08 +0100 aspinall Add askrefs, setrefs, error_with_pos
Mon, 22 Jan 2007 15:36:58 +0100 aspinall Comments
Mon, 22 Jan 2007 15:34:15 +0100 aspinall Comment
Mon, 22 Jan 2007 15:33:42 +0100 aspinall Add line_of, name_of destructors.
Mon, 22 Jan 2007 15:08:48 +0100 krauss Added lemma nat_size[simp]: "size (n::nat) = n"
Mon, 22 Jan 2007 00:40:29 +0100 wenzelm tuned;
Sun, 21 Jan 2007 19:09:38 +0100 wenzelm improved fact references: thmref;
Sun, 21 Jan 2007 19:09:37 +0100 wenzelm added atomic, print_int;
Sun, 21 Jan 2007 19:09:36 +0100 wenzelm tuned ML setup;
Sun, 21 Jan 2007 19:09:35 +0100 wenzelm * ML in Isar: improved error reporting;
Sun, 21 Jan 2007 17:13:30 +0100 wenzelm tuned;
Sun, 21 Jan 2007 16:46:40 +0100 wenzelm *** MESSAGE REFERS TO PREVIOUS VERSION ***
Sun, 21 Jan 2007 16:46:06 +0100 wenzelm *** MESSAGE REFERS TO PREVIOUS VERSION ***
Sun, 21 Jan 2007 16:43:47 +0100 wenzelm tuned comments
Sun, 21 Jan 2007 16:43:46 +0100 wenzelm simplified ML setup;
Sun, 21 Jan 2007 16:43:45 +0100 wenzelm use_text: added name argument;
Sun, 21 Jan 2007 16:43:44 +0100 wenzelm moved File.use to ML_Context.use;
Sun, 21 Jan 2007 16:43:42 +0100 wenzelm use_text: added name argument;
Sun, 21 Jan 2007 13:27:41 +0100 nipkow Added simproc list_neq (prompted by an application)
Sun, 21 Jan 2007 13:26:44 +0100 nipkow Added lists-as-multisets functions
Sat, 20 Jan 2007 14:27:46 +0100 wenzelm Simple and efficient binary numerals.
Sat, 20 Jan 2007 14:27:45 +0100 wenzelm added HOL/ex/Binary.thy;
Sat, 20 Jan 2007 14:09:27 +0100 wenzelm tuned ML setup;
Sat, 20 Jan 2007 14:09:23 +0100 wenzelm * ML within Isar: antiquotations;
Sat, 20 Jan 2007 14:09:22 +0100 wenzelm added @{theory};
Sat, 20 Jan 2007 14:09:21 +0100 wenzelm added the_context_finished;
Sat, 20 Jan 2007 14:09:20 +0100 wenzelm Toplevel.debug: coincide with Output.debugging;
Sat, 20 Jan 2007 14:09:19 +0100 wenzelm ML tactic: proper context for compile and runtime;
Sat, 20 Jan 2007 14:09:18 +0100 wenzelm tuned;
Sat, 20 Jan 2007 14:09:17 +0100 wenzelm added @{simpset};
Sat, 20 Jan 2007 14:09:16 +0100 wenzelm added is_finished_thy;
Sat, 20 Jan 2007 14:09:14 +0100 wenzelm Output.debug: non-strict;
Sat, 20 Jan 2007 14:09:12 +0100 wenzelm tuned ML setup;
Sat, 20 Jan 2007 14:09:11 +0100 wenzelm added @{clasimpset};
Sat, 20 Jan 2007 14:09:10 +0100 wenzelm added @{claset};
Fri, 19 Jan 2007 22:31:17 +0100 wenzelm tuned;
Fri, 19 Jan 2007 22:14:23 +0100 wenzelm tuned;
Fri, 19 Jan 2007 22:10:35 +0100 wenzelm renamed Isar/isar_output.ML to Thy/thy_output.ML;
Fri, 19 Jan 2007 22:08:32 +0100 wenzelm moved ML context stuff to from Context to ML_Context;
Fri, 19 Jan 2007 22:08:31 +0100 wenzelm results: proper context;
Fri, 19 Jan 2007 22:08:30 +0100 wenzelm tuned Scan.extend_lexicon;
Fri, 19 Jan 2007 22:08:29 +0100 wenzelm renamed IsarOutput to ThyOutput;
Fri, 19 Jan 2007 22:08:28 +0100 wenzelm moved parts to spec_parse.ML;
Fri, 19 Jan 2007 22:08:27 +0100 wenzelm removed obsolete Method;
Fri, 19 Jan 2007 22:08:26 +0100 wenzelm renamed IsarOutput to ThyOutput;
Fri, 19 Jan 2007 22:08:25 +0100 wenzelm added various ML setup functions (from sign.ML, pure_thy.ML);
Fri, 19 Jan 2007 22:08:24 +0100 wenzelm removed obsolete Attribute;
Fri, 19 Jan 2007 22:08:23 +0100 wenzelm tuned signature;
Fri, 19 Jan 2007 22:08:22 +0100 wenzelm renamed Isar/isar_output.ML to Thy/thy_output.ML;
Fri, 19 Jan 2007 22:08:21 +0100 wenzelm tuned signature of extend_lexicon;
Fri, 19 Jan 2007 22:08:20 +0100 wenzelm moved ML translation interfaces to isar_cmd.ML;
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip