Sun, 10 Jul 2011 14:02:27 +0200 bulwahn improved NEWS
Sat, 09 Jul 2011 21:18:20 +0200 bulwahn NEWS
Sat, 09 Jul 2011 21:09:09 +0200 bulwahn standardized String.concat towards implode (cf. c37a1f29bbc0)
Sat, 09 Jul 2011 19:29:25 +0200 bulwahn adding quickcheck examples for evaluating floor and ceiling functions
Sat, 09 Jul 2011 19:28:33 +0200 bulwahn adding code equations to execute floor and ceiling on rational and real numbers
Sat, 09 Jul 2011 13:41:58 +0200 bulwahn adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
Sun, 10 Jul 2011 20:59:04 +0200 wenzelm inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
Sun, 10 Jul 2011 17:58:11 +0200 wenzelm lambda terms with XML data representation in Scala;
Sun, 10 Jul 2011 16:34:17 +0200 wenzelm XML data representation of lambda terms;
Sun, 10 Jul 2011 16:31:04 +0200 wenzelm YXML.string_of_body convenience;
Sun, 10 Jul 2011 16:13:37 +0200 wenzelm made SML/NJ happy;
Sun, 10 Jul 2011 16:09:08 +0200 wenzelm tuned signature;
Sun, 10 Jul 2011 15:48:15 +0200 wenzelm more abstract signature;
Sun, 10 Jul 2011 13:51:21 +0200 wenzelm simplified XML_Data;
Sun, 10 Jul 2011 13:00:22 +0200 wenzelm less currying in Scala;
Sun, 10 Jul 2011 00:21:19 +0200 wenzelm propagate header changes to prover process;
Sat, 09 Jul 2011 21:53:27 +0200 wenzelm echo prover input via raw_messages, for improved protocol tracing;
Sat, 09 Jul 2011 18:54:50 +0200 wenzelm tuned;
Sat, 09 Jul 2011 18:35:00 +0200 wenzelm tuned signature;
Sat, 09 Jul 2011 18:15:23 +0200 wenzelm clarified propagation of node name and header;
Sat, 09 Jul 2011 17:14:08 +0200 wenzelm more precise treatment of prover definedness;
Sat, 09 Jul 2011 16:53:19 +0200 wenzelm tuned source structure;
Sat, 09 Jul 2011 13:29:33 +0200 wenzelm some support for blobs (arbitrary text files) within document nodes;
Sat, 09 Jul 2011 12:56:51 +0200 wenzelm tuned signature;
Fri, 08 Jul 2011 22:00:53 +0200 wenzelm moved global state to structure Document (again);
Fri, 08 Jul 2011 21:44:47 +0200 wenzelm moved Outer_Syntax.load_thy to Thy_Load.load_thy;
Fri, 08 Jul 2011 20:27:09 +0200 wenzelm less stateful outer_syntax;
Fri, 08 Jul 2011 17:04:38 +0200 wenzelm discontinued odd Position.column -- left-over from attempts at PGIP implementation;
Fri, 08 Jul 2011 16:13:34 +0200 wenzelm discontinued special treatment of hard tabulators;
Fri, 08 Jul 2011 16:01:14 +0200 wenzelm eliminated hard tabs;
Fri, 08 Jul 2011 15:18:28 +0200 wenzelm merged
Fri, 08 Jul 2011 12:18:46 +0200 nipkow merged
Thu, 07 Jul 2011 21:53:53 +0200 nipkow added translation to fix critical pair between abbreviations for surj and ~=
Thu, 07 Jul 2011 23:33:14 +0200 bulwahn floor and ceiling definitions are not code equations -- this enables trivial evaluation of floor and ceiling
Fri, 08 Jul 2011 15:17:40 +0200 wenzelm standardized String.concat towards implode;
Fri, 08 Jul 2011 14:37:19 +0200 wenzelm more abstract Thy_Load.load_file/use_file for external theory resources;
Fri, 08 Jul 2011 13:59:54 +0200 wenzelm comment;
Fri, 08 Jul 2011 11:50:58 +0200 wenzelm clarified Thy_Load.digest_file -- read ML files only once;
Fri, 08 Jul 2011 11:13:21 +0200 wenzelm tuned signature;
Thu, 07 Jul 2011 23:55:15 +0200 wenzelm simplified make_option/dest_option;
Thu, 07 Jul 2011 22:04:30 +0200 wenzelm explicit Document.Node.Header, with master_dir and thy_name;
Thu, 07 Jul 2011 14:10:50 +0200 wenzelm explicit indication of type Symbol.Symbol;
Thu, 07 Jul 2011 13:48:30 +0200 wenzelm simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
Wed, 06 Jul 2011 23:11:59 +0200 wenzelm merged
Wed, 06 Jul 2011 17:19:34 +0100 blanchet make SML/NJ happier
Wed, 06 Jul 2011 17:19:34 +0100 blanchet make SML/NJ happy + tuning
Wed, 06 Jul 2011 17:19:34 +0100 blanchet moved ATP dependencies to HOL-Plain, where they belong
Wed, 06 Jul 2011 17:19:34 +0100 blanchet better setup for experimental "z3_atp"
Wed, 06 Jul 2011 17:58:03 +0200 krauss 64bit versions of some mira configurations
Wed, 06 Jul 2011 17:56:58 +0200 krauss removed unused mira configuration
Wed, 06 Jul 2011 13:57:52 +0200 bulwahn merged
Wed, 06 Jul 2011 13:52:42 +0200 bulwahn tuning options to avoid spurious isabelle test failures
Wed, 06 Jul 2011 22:02:52 +0200 wenzelm clarified record syntax: fieldext excludes the "more" pseudo-field (unlike 2f885b7e5ba7), so that errors like (| x = a, more = b |) are reported less confusingly;
Wed, 06 Jul 2011 20:46:06 +0200 wenzelm prefer Synchronized.var;
Wed, 06 Jul 2011 20:14:13 +0200 wenzelm tuned errors;
Wed, 06 Jul 2011 13:31:12 +0200 wenzelm record package: proper configuration options;
Wed, 06 Jul 2011 11:37:29 +0200 wenzelm just one copy of split_args;
Wed, 06 Jul 2011 09:54:40 +0200 wenzelm merged
Tue, 05 Jul 2011 19:11:29 +0200 hoelzl rename lemma Infinite_Product_Measure.sigma_sets_subseteq, it hides Sigma_Algebra.sigma_sets_subseteq
Tue, 05 Jul 2011 17:09:59 +0100 nik improved translation of lambdas in THF
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip