Thu, 13 Feb 2014 13:16:17 +0100 blanchet repaired logic for default provers -- ensures Z3 is kept if installed and configured as noncommercial
Thu, 13 Feb 2014 13:16:17 +0100 blanchet avoid changing the state's context -- this results in transfer problems later with SMT, and hence preplay tactic failures
Thu, 13 Feb 2014 13:16:16 +0100 blanchet removed hint that is seldom useful in practice
Thu, 13 Feb 2014 12:24:28 +0100 wenzelm reactivate some examples that still appear to work;
Thu, 13 Feb 2014 12:14:47 +0100 wenzelm removed dead code;
Thu, 13 Feb 2014 12:09:51 +0100 wenzelm explicit indication that redefining outer syntax commands is not supposed to happen -- NB: interactive mode requires global change of syntax;
Thu, 13 Feb 2014 11:54:14 +0100 wenzelm do not redefine outer syntax commands;
Thu, 13 Feb 2014 11:37:00 +0100 wenzelm tuned whitespace;
Thu, 13 Feb 2014 11:23:55 +0100 wenzelm static repair of ML file -- untested (!) by default since 76965c356d2a;
Wed, 12 Feb 2014 17:36:00 +0100 blanchet iteration n in the 'default' vs. 'update_new' vs. 'update' saga -- 'update' makes sense now that we honor the canonical order on 'merge' (as opposed to raising 'DUP')
Wed, 12 Feb 2014 17:35:59 +0100 blanchet don't hide constant forever, since it may appear in some 'primcorec'-generated theorems
Wed, 12 Feb 2014 17:35:59 +0100 blanchet tuning
Wed, 12 Feb 2014 16:35:58 +0100 traytel HOL-IMP fastness
Wed, 12 Feb 2014 14:32:45 +0100 wenzelm merged, resolving some conflicts;
Wed, 12 Feb 2014 13:56:43 +0100 wenzelm eliminated hard tabs (assuming tab-width=2);
Wed, 12 Feb 2014 13:53:11 +0100 wenzelm more platform notes;
Wed, 12 Feb 2014 13:33:05 +0100 wenzelm tuned whitespace;
Wed, 12 Feb 2014 13:31:18 +0100 wenzelm removed odd comments -- inferred types are shown by Prover IDE;
Wed, 12 Feb 2014 11:28:17 +0100 wenzelm maintain blob edits within history, which is important for Snapshot.convert/revert;
Wed, 12 Feb 2014 11:05:48 +0100 wenzelm more accurate eq_content;
Wed, 12 Feb 2014 10:50:49 +0100 wenzelm clarified message_positions: cover alt_id as well;
Tue, 11 Feb 2014 21:58:31 +0100 wenzelm maintain multiple command chunks and markup trees: for main chunk and loaded files;
Tue, 11 Feb 2014 17:44:29 +0100 wenzelm common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
Tue, 11 Feb 2014 15:55:05 +0100 wenzelm tuned signature;
Tue, 11 Feb 2014 15:05:13 +0100 wenzelm report (but ignore) markup within auxiliary files;
Wed, 12 Feb 2014 10:59:25 +0100 Andreas Lochbihler merged
Wed, 12 Feb 2014 09:06:04 +0100 Andreas Lochbihler make integer_of_char and char_of_integer work with NBE and code_simp
Wed, 12 Feb 2014 08:56:38 +0100 Andreas Lochbihler make lifting setup for String.literal local to prevent transfer from replacing STR ''...'' literals
Wed, 12 Feb 2014 10:20:31 +0100 blanchet [mq]: news
Wed, 12 Feb 2014 08:37:28 +0100 blanchet remove hidden fact about hidden constant from code generator setup
Wed, 12 Feb 2014 08:37:28 +0100 blanchet for extraction -- use the exhaust rule that's registered with 'datatype_realizer.ML'
Wed, 12 Feb 2014 08:37:28 +0100 blanchet compile
Wed, 12 Feb 2014 08:37:28 +0100 blanchet updated certificates
Wed, 12 Feb 2014 08:37:28 +0100 blanchet tuned message
Wed, 12 Feb 2014 08:37:28 +0100 blanchet tabled, v.: postpone consideration of
Wed, 12 Feb 2014 08:37:28 +0100 blanchet adapted to renaming of 'Projl' and 'Projr'
Wed, 12 Feb 2014 08:37:06 +0100 blanchet adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
Wed, 12 Feb 2014 08:35:57 +0100 blanchet adapted theories to 'xxx_case' to 'case_xxx'
Wed, 12 Feb 2014 08:35:57 +0100 blanchet renamed 'nat_{case,rec}' to '{case,rec}_nat'
Wed, 12 Feb 2014 08:35:57 +0100 blanchet renamed '{prod,sum,bool,unit}_case' to 'case_...'
Wed, 12 Feb 2014 08:35:56 +0100 blanchet adapted theories to '{case,rec}_{list,option}' names
Wed, 12 Feb 2014 08:35:56 +0100 blanchet avoid old 'prod.simps' -- better be more specific
Wed, 12 Feb 2014 08:35:56 +0100 blanchet repaired hard-coded constant names
Wed, 12 Feb 2014 08:35:56 +0100 blanchet killed 'rep_compat' option
Wed, 12 Feb 2014 08:35:56 +0100 blanchet made 'ctr_sugar' more friendly to the 'datatype_realizer'
Wed, 12 Feb 2014 08:35:56 +0100 blanchet use names like 'rec_mytype' and 'case_mytype' in old datatype package as well, to avoid a mixture
Wed, 12 Feb 2014 08:35:56 +0100 blanchet use right local theory -- shows up when 'no_discs_sels' is set
Wed, 12 Feb 2014 08:35:56 +0100 blanchet compatibility names
Wed, 12 Feb 2014 08:35:56 +0100 blanchet use new selector support to define 'the', 'hd', 'tl'
Wed, 12 Feb 2014 08:35:56 +0100 blanchet transformed 'option' and 'list' into new-style datatypes (but register them as old-style as well)
Wed, 12 Feb 2014 08:35:56 +0100 blanchet avoid duplicate 'case' definitions by first looking up 'Ctr_Sugar'
Wed, 12 Feb 2014 08:35:56 +0100 blanchet tuned code
Wed, 12 Feb 2014 08:35:56 +0100 blanchet more 'ctr_sugar' modernization
Wed, 12 Feb 2014 08:35:56 +0100 blanchet tuning
Wed, 12 Feb 2014 08:35:56 +0100 blanchet ported predicate compiler to 'ctr_sugar'
Wed, 12 Feb 2014 08:35:56 +0100 blanchet updated docs
Wed, 12 Feb 2014 08:35:56 +0100 blanchet generate 'fundec_cong' attribute for new-style (co)datatypes
Wed, 12 Feb 2014 08:35:56 +0100 blanchet got rid of dynamic scoping the easy way
Wed, 12 Feb 2014 08:35:56 +0100 blanchet removed trivial 'rec' examples for nonrecursive types (I could also have added the 'old.' prefix in front of the constant names)
Wed, 12 Feb 2014 08:35:56 +0100 blanchet more liberal merging of BNFs and constructor sugar
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip