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;
Fri, 19 Jan 2007 22:08:19 +0100 wenzelm moved thm/thms to ml_context.ML;
(0) -10000 -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 +30000 tip