2008-04-02 haftmann 2008-04-02 moved some code lemmas for Numerals here
2008-04-02 chaieb 2008-04-02 No longer imports InfiniteSet, ATP_Linkup is sufficient.
2008-03-31 gagern 2008-03-31 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53 (forget_structure); doing some more advanced file name rewriting.
2008-03-31 wenzelm 2008-03-31 before close: Exn.capture/release;
2008-03-31 wenzelm 2008-03-31 discontinued unused hooks explode_platform_path_fn, platform_path_fn, shell_path_fn; norm_absolute: non-critical (not thread-safe!); added open_input, open_output, open_append combinators; tuned;
2008-03-31 wenzelm 2008-03-31 added add_substring; output: operate directly on stream; tuned;
2008-03-31 wenzelm 2008-03-31 discontinued File.explode_platform_path -- use plain Path.explode;
2008-03-30 nipkow 2008-03-30 *** empty log message ***
2008-03-29 wenzelm 2008-03-29 functional theory setup -- requires linear access;
2008-03-29 wenzelm 2008-03-29 simplified print_simpset;
2008-03-29 wenzelm 2008-03-29 purely functional setup of claset/simpset/clasimpset; tuned signature;
2008-03-29 wenzelm 2008-03-29 purely functional setup of claset/simpset/clasimpset;
2008-03-29 wenzelm 2008-03-29 fixed spelling;
2008-03-29 wenzelm 2008-03-29 added exec_file; tuned;
2008-03-29 wenzelm 2008-03-29 CRITICAL: further trace levels for 1000ms and 100ms;
2008-03-29 wenzelm 2008-03-29 removed obsolete store_thm(s), cf. functional versions in pure_thy.ML; tuned;
2008-03-29 wenzelm 2008-03-29 added generic_theory transaction;
2008-03-29 wenzelm 2008-03-29 commands 'use' and 'ML' now thy_decl; removed obsolete 'ML_setup' -- superceded by 'ML';
2008-03-29 wenzelm 2008-03-29 removed obsolete use_XXX; added ml_diag;
2008-03-29 wenzelm 2008-03-29 eliminated destructive/critical theorem database; simplified store_thm(s); removed obsolete smart_store_thm(s); tuned;
2008-03-29 wenzelm 2008-03-29 certify wrt. dynamic context; functional store_thm (wrt. thread data);
2008-03-29 wenzelm 2008-03-29 added map_theory_result, map_proof_result;
2008-03-29 wenzelm 2008-03-29 certify wrt. dynamic context;
2008-03-29 wenzelm 2008-03-29 eliminated non-linear access to thy1 and thy12c;
2008-03-29 wenzelm 2008-03-29 replaced 'ML' by diagnostic 'ML_command';
2008-03-29 wenzelm 2008-03-29 updated generated file;
2008-03-29 wenzelm 2008-03-29 simplified PureThy.store_thm;
2008-03-29 wenzelm 2008-03-29 replaced 'ML_setup' by 'ML';
2008-03-29 wenzelm 2008-03-29 * Eliminated destructive theorem database. * Commands 'use' and 'ML' are now purely functional; added diagnostic 'ML_val'.
2008-03-29 wenzelm 2008-03-29 eliminated quiete_mode ref (not really needed);
2008-03-29 wenzelm 2008-03-29 eliminated quiete_mode ref (turned into proper argument);
2008-03-29 wenzelm 2008-03-29 eliminated quiete_mode ref (unused);
2008-03-29 wenzelm 2008-03-29 eliminated quiet_mode ref of some packages (avoid CRITICAL setmp!);
2008-03-28 wenzelm 2008-03-28 added forget_structure;
2008-03-28 wenzelm 2008-03-28 eval_wrapper: non-critical version via unique Isabelle structure, proper forget_structure;
2008-03-28 wenzelm 2008-03-28 ml_tactic: non-critical version via proof data and thread data;
2008-03-28 wenzelm 2008-03-28 NAMED_CRITICAL;
2008-03-28 haftmann 2008-03-28 unfold_locales now part of default tactic
2008-03-28 haftmann 2008-03-28 import Main explicitly
2008-03-28 haftmann 2008-03-28 dropped now superfluous ad-hoc adaption
2008-03-28 haftmann 2008-03-28 not depends on Main any longer
2008-03-28 haftmann 2008-03-28 accomodated to sledgehammer theory dependency requirement
2008-03-28 haftmann 2008-03-28 only invoke interpret
2008-03-28 wenzelm 2008-03-28 updated generated file;
2008-03-28 wenzelm 2008-03-28 Context.>> : operate on Context.generic;
2008-03-28 wenzelm 2008-03-28 avoid rebinding of existing facts;
2008-03-28 haftmann 2008-03-28 some styling
2008-03-28 haftmann 2008-03-28 some styling
2008-03-28 haftmann 2008-03-28 some styling
2008-03-28 urbanc 2008-03-28 tuned proofs
2008-03-28 wenzelm 2008-03-28 tuned;
2008-03-28 wenzelm 2008-03-28 updated dependencies;
2008-03-28 wenzelm 2008-03-28 reorganized signature of ML_Context;
2008-03-27 huffman 2008-03-27 remove commented text
2008-03-27 wenzelm 2008-03-27 avoid ambiguity of State.state vs. JVMType.state;
2008-03-27 huffman 2008-03-27 declare cont_lemmas_ext as simp rules individually
2008-03-27 wenzelm 2008-03-27 avoid amiguity of Continuity.chain vs. Porder.chain;
2008-03-27 wenzelm 2008-03-27 avoid amiguity of State.state vs. JVMType.state;
2008-03-27 haftmann 2008-03-27 changed wrong assignement in signature sections
2008-03-27 haftmann 2008-03-27 clarified character serializations