2014-02-13 wenzelm 2014-02-13 reactivate some examples that still appear to work;
2014-02-13 wenzelm 2014-02-13 removed dead code;
2014-02-13 wenzelm 2014-02-13 explicit indication that redefining outer syntax commands is not supposed to happen -- NB: interactive mode requires global change of syntax;
2014-02-13 wenzelm 2014-02-13 do not redefine outer syntax commands;
2014-02-13 wenzelm 2014-02-13 tuned whitespace;
2014-02-13 wenzelm 2014-02-13 static repair of ML file -- untested (!) by default since 76965c356d2a;
2014-02-12 blanchet 2014-02-12 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')
2014-02-12 blanchet 2014-02-12 don't hide constant forever, since it may appear in some 'primcorec'-generated theorems
2014-02-12 blanchet 2014-02-12 tuning
2014-02-12 traytel 2014-02-12 HOL-IMP fastness
2014-02-12 wenzelm 2014-02-12 merged, resolving some conflicts;
2014-02-12 wenzelm 2014-02-12 eliminated hard tabs (assuming tab-width=2);
2014-02-12 wenzelm 2014-02-12 more platform notes;
2014-02-12 wenzelm 2014-02-12 tuned whitespace;
2014-02-12 wenzelm 2014-02-12 removed odd comments -- inferred types are shown by Prover IDE;
2014-02-12 wenzelm 2014-02-12 maintain blob edits within history, which is important for Snapshot.convert/revert;
2014-02-12 wenzelm 2014-02-12 more accurate eq_content;
2014-02-12 wenzelm 2014-02-12 clarified message_positions: cover alt_id as well; tuned;
2014-02-11 wenzelm 2014-02-11 maintain multiple command chunks and markup trees: for main chunk and loaded files; document view for all text areas, including auxiliary files;
2014-02-11 wenzelm 2014-02-11 common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content); more informative type Blob, to allow markup reports;
2014-02-11 wenzelm 2014-02-11 tuned signature;
2014-02-11 wenzelm 2014-02-11 report (but ignore) markup within auxiliary files;
2014-02-12 Andreas Lochbihler 2014-02-12 merged
2014-02-12 Andreas Lochbihler 2014-02-12 make integer_of_char and char_of_integer work with NBE and code_simp
2014-02-12 Andreas Lochbihler 2014-02-12 make lifting setup for String.literal local to prevent transfer from replacing STR ''...'' literals
2014-02-12 blanchet 2014-02-12 [mq]: news
2014-02-12 blanchet 2014-02-12 remove hidden fact about hidden constant from code generator setup
2014-02-12 blanchet 2014-02-12 for extraction -- use the exhaust rule that's registered with 'datatype_realizer.ML'
2014-02-12 blanchet 2014-02-12 compile
2014-02-12 blanchet 2014-02-12 updated certificates
2014-02-12 blanchet 2014-02-12 tuned message
2014-02-12 blanchet 2014-02-12 tabled, v.: postpone consideration of
2014-02-12 blanchet 2014-02-12 adapted to renaming of 'Projl' and 'Projr'
2014-02-12 blanchet 2014-02-12 adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems * * * more transition of 'xxx_rec' to 'rec_xxx' and same for case * * * compile * * * 'rename_tac's to avoid referring to generated names * * * more robust scripts with 'rename_tac' * * * 'where' -> 'of' * * * 'where' -> 'of' * * * renamed 'xxx_rec' to 'rec_xxx'
2014-02-12 blanchet 2014-02-12 adapted theories to 'xxx_case' to 'case_xxx' * * * 'char_case' -> 'case_char' and same for 'rec' * * * compile * * * renamed 'xxx_case' to 'case_xxx'
2014-02-12 blanchet 2014-02-12 renamed 'nat_{case,rec}' to '{case,rec}_nat'
2014-02-12 blanchet 2014-02-12 renamed '{prod,sum,bool,unit}_case' to 'case_...'
2014-02-12 blanchet 2014-02-12 adapted theories to '{case,rec}_{list,option}' names
2014-02-12 blanchet 2014-02-12 avoid old 'prod.simps' -- better be more specific
2014-02-12 blanchet 2014-02-12 repaired hard-coded constant names
2014-02-12 blanchet 2014-02-12 killed 'rep_compat' option
2014-02-12 blanchet 2014-02-12 made 'ctr_sugar' more friendly to the 'datatype_realizer' * * * reverted changes to 'datatype_realizer.ML'
2014-02-12 blanchet 2014-02-12 use names like 'rec_mytype' and 'case_mytype' in old datatype package as well, to avoid a mixture
2014-02-12 blanchet 2014-02-12 use right local theory -- shows up when 'no_discs_sels' is set
2014-02-12 blanchet 2014-02-12 compatibility names
2014-02-12 blanchet 2014-02-12 use new selector support to define 'the', 'hd', 'tl'
2014-02-12 blanchet 2014-02-12 transformed 'option' and 'list' into new-style datatypes (but register them as old-style as well) * * * compile * * * tuned imports to prevent merge issues in 'Main'
2014-02-12 blanchet 2014-02-12 avoid duplicate 'case' definitions by first looking up 'Ctr_Sugar'
2014-02-12 blanchet 2014-02-12 tuned code
2014-02-12 blanchet 2014-02-12 more 'ctr_sugar' modernization
2014-02-12 blanchet 2014-02-12 tuning
2014-02-12 blanchet 2014-02-12 ported predicate compiler to 'ctr_sugar' * * * ported predicate compiler to 'ctr_sugar', part 2
2014-02-12 blanchet 2014-02-12 updated docs
2014-02-12 blanchet 2014-02-12 generate 'fundec_cong' attribute for new-style (co)datatypes * * * compile
2014-02-12 blanchet 2014-02-12 got rid of dynamic scoping the easy way
2014-02-12 blanchet 2014-02-12 removed trivial 'rec' examples for nonrecursive types (I could also have added the 'old.' prefix in front of the constant names)
2014-02-12 blanchet 2014-02-12 more liberal merging of BNFs and constructor sugar * * * make sure that the cache doesn't produce 'DUP's
2014-02-12 blanchet 2014-02-12 se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors * * * cleaner simp/iff sets
2014-02-12 blanchet 2014-02-12 have the same no-update semantics for 'case' as for 'Ctr_Sugar' and BNF data (this might not be the final word on the matter, but using a consistent policy seems like a good idea)
2014-02-11 wenzelm 2014-02-11 Mac OS X Lion (macbroy6) is baseline for portable executables; fringe platforms are unsupported;