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
Tue, 05 Jul 2011 17:09:59 +0100 nik added generation of lambdas in THF
Tue, 05 Jul 2011 17:09:59 +0100 nik add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes first-order)
Tue, 05 Jul 2011 23:18:14 +0200 wenzelm simplified Symbol.iterator: produce strings, which are mostly preallocated;
Tue, 05 Jul 2011 22:43:18 +0200 wenzelm tuned comment (cf. e9f26e66692d);
Tue, 05 Jul 2011 22:39:15 +0200 wenzelm Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
Tue, 05 Jul 2011 22:38:44 +0200 wenzelm theory name needs to conform to Path syntax;
Tue, 05 Jul 2011 21:53:59 +0200 wenzelm hard-wired print mode "xsymbols" increases chance that "iff" in HOL will print symbolic arrow;
Tue, 05 Jul 2011 21:32:48 +0200 wenzelm prefer space_explode/split_lines as in Isabelle/ML;
Tue, 05 Jul 2011 21:20:24 +0200 wenzelm Path.split convenience;
Tue, 05 Jul 2011 20:36:49 +0200 wenzelm get theory from last executation state;
Tue, 05 Jul 2011 19:45:59 +0200 wenzelm explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOL-SPARK for example);
Tue, 05 Jul 2011 11:45:48 +0200 wenzelm clarified cancel_execution/await_cancellation;
Tue, 05 Jul 2011 11:16:37 +0200 wenzelm tuned signature;
Tue, 05 Jul 2011 10:54:05 +0200 wenzelm tuned;
Tue, 05 Jul 2011 09:54:39 +0200 krauss re-check to explicitly propagate a given type constraint to lhs -- necessary to trigger type improvement in an instantiation target
Mon, 04 Jul 2011 22:25:33 +0200 wenzelm Document.no_id/new_id as in ML (new_id *could* be session-specific but it isn't right now);
Mon, 04 Jul 2011 22:11:32 +0200 wenzelm quasi-static Isabelle_System -- reduced tendency towards "functorial style";
Mon, 04 Jul 2011 20:18:19 +0200 wenzelm explicit class Counter;
Mon, 04 Jul 2011 16:54:58 +0200 wenzelm merged
Mon, 04 Jul 2011 10:23:46 +0200 hoelzl the borel probability measure is easier to handle with {0 ..< 1} (coverable by disjoint intervals {_ ..< _})
Mon, 04 Jul 2011 10:15:49 +0200 hoelzl equalities of subsets of atLeastLessThan
Sun, 03 Jul 2011 09:59:25 +0200 bulwahn adding documentation of the value antiquotation to the code generation manual
Sun, 03 Jul 2011 08:15:14 +0200 blanchet make SML/NJ happy
Sat, 02 Jul 2011 22:55:58 +0200 haftmann install case certificate for If after code_datatype declaration for bool
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip