Mon, 05 Jul 2010 09:12:35 -0700 huffman section -> subsection
Sun, 04 Jul 2010 09:26:30 -0700 huffman generalize some lemmas about derivatives
Sun, 04 Jul 2010 09:25:17 -0700 huffman uniqueness of Frechet derivative
Tue, 06 Jul 2010 21:33:14 +0200 wenzelm implode pseudo utf8, i.e. decode byte-stuffed low ASCII characters;
Tue, 06 Jul 2010 10:02:24 +0200 wenzelm merged
Tue, 06 Jul 2010 09:27:49 +0200 haftmann even more fun with primrec
Tue, 06 Jul 2010 09:21:15 +0200 haftmann refactored reference operations
Tue, 06 Jul 2010 09:21:13 +0200 haftmann tuned
Tue, 06 Jul 2010 09:21:13 +0200 haftmann tuned empty heap
Mon, 05 Jul 2010 16:43:08 +0100 paulson merged
Mon, 05 Jul 2010 14:21:53 +0100 paulson merged
Mon, 05 Jul 2010 14:21:30 +0100 paulson Unification (flexflex) bug fix; making "auto" deterministic
Mon, 05 Jul 2010 16:46:23 +0200 haftmann moved "open" operations from Heap.thy to Array.thy and Ref.thy
Mon, 05 Jul 2010 15:36:37 +0200 haftmann only definite assignment
Mon, 05 Jul 2010 15:25:42 +0200 haftmann moved special operation array_ran here
Mon, 05 Jul 2010 15:25:42 +0200 haftmann remove primitive operation Heap.array in favour of Heap.array_of_list
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;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip