Mon, 05 Jul 2010 15:12:20 +0200 haftmann tuned proof
Mon, 05 Jul 2010 15:12:20 +0200 haftmann tuned
Mon, 05 Jul 2010 23:07:36 +0200 wenzelm Outer_Syntax.prepare_command: disallow control commands here, and consequently in Isar documents;
Mon, 05 Jul 2010 22:26:20 +0200 wenzelm specific ML_val vs. ML_command;
Mon, 05 Jul 2010 20:36:39 +0200 wenzelm async_state: report within proper transaction context;
Mon, 05 Jul 2010 14:35:00 +0200 haftmann merged
Mon, 05 Jul 2010 14:34:28 +0200 haftmann simplified representation of monad type
Mon, 05 Jul 2010 11:25:06 +0200 wenzelm attempt to reconstruct missing HOL/Codegenerator_Test/ROOT.ML;
Mon, 05 Jul 2010 10:47:39 +0200 wenzelm merged
Mon, 05 Jul 2010 10:42:27 +0200 haftmann updated document
Mon, 05 Jul 2010 10:39:49 +0200 haftmann dropped passed irregular names
Sat, 03 Jul 2010 00:50:35 +0200 blanchet adapt Nitpick to "prod_case" and "*" -> "sum" renaming;
Sat, 03 Jul 2010 00:49:12 +0200 blanchet remove needless signature entry
Fri, 02 Jul 2010 17:27:44 +0200 haftmann references to ghc and ocaml
Fri, 02 Jul 2010 17:27:44 +0200 haftmann explicit code_datatype declaration prevents multiple instantiations later on
Fri, 02 Jul 2010 16:50:53 +0200 haftmann refrain from using datatype declaration -- opens chance for quickcheck later on
Fri, 02 Jul 2010 16:50:52 +0200 haftmann tuned proof
Fri, 02 Jul 2010 16:20:56 +0200 haftmann reverted to verion from fc27be4c6b1c
Fri, 02 Jul 2010 16:15:49 +0200 haftmann traceback for error messages
Fri, 02 Jul 2010 16:10:59 +0200 haftmann accomodate for different behvaiour of nitpick (c.f. also 180e80b4eac1)
Fri, 02 Jul 2010 14:23:18 +0200 haftmann introduced distinct session HOL-Codegenerator_Test
Fri, 02 Jul 2010 14:23:17 +0200 haftmann tuned bootstrap files
Fri, 02 Jul 2010 14:23:17 +0200 haftmann remove codegeneration-related theories from big library theory
Fri, 02 Jul 2010 14:23:17 +0200 haftmann drop unconvenient code declarations
Fri, 02 Jul 2010 14:23:16 +0200 haftmann build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
Sun, 04 Jul 2010 21:01:22 +0200 wenzelm general Future.report -- also for Toplevel.async_state;
Sun, 04 Jul 2010 00:05:32 +0200 wenzelm simplified Isabelle_Process.Result: use markup directly;
Sat, 03 Jul 2010 23:24:36 +0200 wenzelm run_command: actually observe "print" flag;
Sat, 03 Jul 2010 22:33:10 +0200 wenzelm Toplevel.run_command: asynchronous state output, as an attempt to address potentially slow pretty printing (e.g. in HOL/Bali);
Sat, 03 Jul 2010 20:36:30 +0200 wenzelm more precise timing;
Sat, 03 Jul 2010 20:20:13 +0200 wenzelm more efficient document model/view -- avoid repeated iteration over commands from start, prefer bulk operations;
Fri, 02 Jul 2010 21:48:54 +0200 wenzelm standard argument order;
Fri, 02 Jul 2010 21:41:06 +0200 wenzelm do not open auxiliary ML structures;
Fri, 02 Jul 2010 20:44:17 +0200 wenzelm tuned white space;
Fri, 02 Jul 2010 10:47:50 +0200 haftmann fixed spelling
Fri, 02 Jul 2010 10:45:25 +0200 haftmann merged
Thu, 01 Jul 2010 16:55:05 +0200 haftmann "prod" and "sum" replace "*" and "+" respectively; qualified constants Set.member and Set.Collect
Thu, 01 Jul 2010 16:54:44 +0200 haftmann "prod" and "sum" replace "*" and "+" respectively
Thu, 01 Jul 2010 16:54:42 +0200 haftmann qualified constants Set.member and Set.Collect
Thu, 01 Jul 2010 16:54:42 +0200 haftmann "prod" and "sum" replace "*" and "+" respectively; qualified constants Set.member and Set.Collect
Thu, 01 Jul 2010 15:40:58 -0700 huffman merged
Thu, 01 Jul 2010 15:40:38 -0700 huffman convert theorem path_connected_sphere to euclidean_space class
Thu, 01 Jul 2010 09:24:04 -0700 huffman generalize more lemmas from ordered_euclidean_space to euclidean_space
Thu, 01 Jul 2010 19:14:54 +0200 wenzelm avoid Old_Number_Theory;
Thu, 01 Jul 2010 18:31:46 +0200 wenzelm misc tuning and modernization;
Thu, 01 Jul 2010 14:32:57 +0200 haftmann merged
Thu, 01 Jul 2010 13:47:27 +0200 haftmann once more a try with mkdir_leaf
Thu, 01 Jul 2010 13:38:17 +0200 haftmann refined semantics of mkdir_leaf: do not fail if directory already exists
Thu, 01 Jul 2010 13:32:14 +0200 haftmann avoid bitstrings in generated code
Thu, 01 Jul 2010 10:57:19 +0200 hoelzl Updated NEWS
Thu, 01 Jul 2010 11:48:42 +0200 hoelzl Add theory for indicator function.
Thu, 01 Jul 2010 09:01:09 +0200 hoelzl Instantiate product type as euclidean space.
Thu, 01 Jul 2010 08:13:20 +0200 haftmann merged
Thu, 01 Jul 2010 08:12:55 +0200 haftmann repaired line ending
Thu, 01 Jul 2010 08:12:40 +0200 haftmann revert to plain for now mkdir
Wed, 30 Jun 2010 17:12:38 +0200 haftmann one unified Word theory
Wed, 30 Jun 2010 16:46:44 +0200 haftmann more speaking names
Wed, 30 Jun 2010 16:45:47 +0200 haftmann more speaking names
Wed, 30 Jun 2010 16:41:03 +0200 haftmann moved specific operations here
Wed, 30 Jun 2010 16:28:29 +0200 haftmann more speaking theory names
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip