Sun, 22 Mar 2009 21:48:14 +0100 wenzelm merged
Sun, 22 Mar 2009 19:43:21 +0100 nipkow merged
Sun, 22 Mar 2009 19:36:04 +0100 nipkow 1. New cancellation simprocs for common factors in inequations
Sun, 22 Mar 2009 11:56:32 +0100 haftmann clarified relationship of modules Code_Name and Code_Printer
Sun, 22 Mar 2009 11:56:22 +0100 haftmann added Symreltab (binary relations of symbols) instance of TableFun
Sun, 22 Mar 2009 21:30:21 +0100 wenzelm proper signature;
Sun, 22 Mar 2009 20:50:02 +0100 wenzelm added read_antiq, with improved error reporting;
Sun, 22 Mar 2009 20:49:48 +0100 wenzelm ML_Lex.read_antiq;
Sun, 22 Mar 2009 20:49:48 +0100 wenzelm ML_Lex.read_antiq;
Sun, 22 Mar 2009 20:49:47 +0100 wenzelm simplified Antiquote.read (again);
Sun, 22 Mar 2009 20:49:47 +0100 wenzelm export report -- version that actually covers all cases;
Sun, 22 Mar 2009 19:12:36 +0100 wenzelm Test of advanced ML compiler invocation in Poly/ML 5.3.
Sun, 22 Mar 2009 19:11:00 +0100 wenzelm ML/ml_test.ML: test of advanced ML compiler invocation in Poly/ML 5.3;
Sun, 22 Mar 2009 19:10:59 +0100 wenzelm added pretty_ml;
Sun, 22 Mar 2009 19:10:59 +0100 wenzelm export eval_antiquotes: refined version that operates on ML tokens;
Sun, 22 Mar 2009 19:10:59 +0100 wenzelm ML_Lex.pos_of: regular position;
Sun, 22 Mar 2009 19:10:58 +0100 wenzelm replaced Antiquote.is_antiq by Antiquote.is_text;
Sat, 21 Mar 2009 20:39:38 +0100 wenzelm merged
Sat, 21 Mar 2009 20:38:49 +0100 wenzelm extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
Sat, 21 Mar 2009 20:22:13 +0100 wenzelm merged
Sat, 21 Mar 2009 09:42:55 -0700 huffman merged
Sat, 21 Mar 2009 03:24:35 -0700 huffman move field lemmas into class locale context
Sat, 21 Mar 2009 03:23:17 -0700 huffman move diff_eq_0_iff_eq into class locale context
Sat, 21 Mar 2009 20:00:23 +0100 wenzelm removed obsolete pprint operations;
Sat, 21 Mar 2009 20:00:23 +0100 wenzelm added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
Sat, 21 Mar 2009 19:58:45 +0100 wenzelm adapted toplevel_pp to ML_Pretty.pretty;
Sat, 21 Mar 2009 19:58:45 +0100 wenzelm replaced install_pp/make_pp by more general toplevel_pp based on use_text;
Sat, 21 Mar 2009 19:58:45 +0100 wenzelm simplified datatype ML_Pretty.pretty: model Isabelle not Poly/ML;
Sat, 21 Mar 2009 19:58:44 +0100 wenzelm simplified datatype ML_Pretty.pretty: model Isabelle not Poly/ML;
Sat, 21 Mar 2009 15:09:44 +0100 wenzelm Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
Sat, 21 Mar 2009 15:08:00 +0100 wenzelm Pretty.position;
Sat, 21 Mar 2009 15:08:00 +0100 wenzelm added position;
Sat, 21 Mar 2009 15:08:00 +0100 wenzelm added generic ML_Pretty interface;
Sat, 21 Mar 2009 13:11:12 +0100 wenzelm restricted interrupts for tasks running as future worker thread -- attempt to prevent interrupt race conditions;
Sat, 21 Mar 2009 12:37:13 +0100 wenzelm more ambitious ML_OPTIONS;
Sat, 21 Mar 2009 12:35:34 +0100 wenzelm more stats;
Fri, 20 Mar 2009 21:32:12 +0100 wenzelm added ML syntax markup;
Fri, 20 Mar 2009 20:22:13 +0100 wenzelm report markup for ML tokens;
Fri, 20 Mar 2009 20:21:38 +0100 wenzelm Antiquote.read: argument for reporting text;
Fri, 20 Mar 2009 20:20:09 +0100 wenzelm future_job: do not inherit attributes, but enforce restricted interrupts -- attempt to prevent interrupt race conditions;
Fri, 20 Mar 2009 20:05:51 +0100 wenzelm uniform ml_prompts for RAW and Pure;
Fri, 20 Mar 2009 18:46:50 +0100 wenzelm eliminated old Addsimps;
Fri, 20 Mar 2009 17:12:37 +0100 wenzelm Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
Fri, 20 Mar 2009 17:04:44 +0100 wenzelm fixed possibility_tac;
Fri, 20 Mar 2009 15:24:18 +0100 wenzelm eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
Fri, 20 Mar 2009 11:26:59 +0100 wenzelm merged
Fri, 20 Mar 2009 10:44:25 +0100 berghofe merged
Fri, 20 Mar 2009 10:43:53 +0100 berghofe split_codegen now eta-expands terms on-the-fly.
Fri, 20 Mar 2009 11:26:25 +0100 wenzelm proper context for prove_cont/adm_tac;
Fri, 20 Mar 2009 11:08:59 +0100 wenzelm with_attributes: canonical capture/release scheme (potentially iron out race condition);
Fri, 20 Mar 2009 09:52:32 +0100 wenzelm considerable speedup of benchmarks by using minimal simpset;
Fri, 20 Mar 2009 09:51:41 +0100 wenzelm allow non-printable symbols within string tokens;
Thu, 19 Mar 2009 22:05:37 +0100 wenzelm merged
Thu, 19 Mar 2009 08:13:10 -0700 huffman add lemma det_diagonal; remove wellorder requirement on several lemmas
Thu, 19 Mar 2009 14:08:55 +0100 haftmann merged
Thu, 19 Mar 2009 14:08:41 +0100 haftmann tuned some theorem and attribute bindings
Thu, 19 Mar 2009 22:05:00 +0100 wenzelm proper spacing before ML antiquotations -- note that @ may be part of symbolic ML identifiers;
Thu, 19 Mar 2009 21:05:40 +0100 wenzelm eval_antiquotes: joint scanning of ML tokens and antiquotations;
Thu, 19 Mar 2009 21:04:53 +0100 wenzelm added scan_antiq;
Thu, 19 Mar 2009 19:49:09 +0100 wenzelm RAW: provide dummy Isar.main to make tty work gracefully (with ML toplevel);
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip