2008-04-03 berghofe 2008-04-03 - use SkipProof.prove_global instead of Goal.prove_global - added skip_mono flag to inductive definition package
2008-04-03 berghofe 2008-04-03 Added prove_global.
2008-04-03 krauss 2008-04-03 Function package no longer overwrites theorems. Some tuning.
2008-04-03 wenzelm 2008-04-03 Why XML notation?
2008-04-03 wenzelm 2008-04-03 Symbol.STX, Symbol.DEL;
2008-04-03 wenzelm 2008-04-03 Symbol.SOH;
2008-04-03 wenzelm 2008-04-03 added detect; removed auxiliary buffer_of_tree; tuned;
2008-04-03 wenzelm 2008-04-03 added some ASCII control symbols;
2008-04-03 wenzelm 2008-04-03 added Pure/General/yxml.ML;
2008-04-03 urbanc 2008-04-03 added generalised definitions for freshness of sets of atoms and lists of atoms
2008-04-02 haftmann 2008-04-02 tuned imports
2008-04-02 haftmann 2008-04-02 tuned
2008-04-02 haftmann 2008-04-02 subst_alias
2008-04-02 haftmann 2008-04-02 improved improvements for instantiaton
2008-04-02 haftmann 2008-04-02 canonical meet_sort operation
2008-04-02 haftmann 2008-04-02 removed obscure "attach" feature
2008-04-02 haftmann 2008-04-02 extended
2008-04-02 haftmann 2008-04-02 tuned towards code generation
2008-04-02 haftmann 2008-04-02 explicit class "eq" for operational equality
2008-04-02 haftmann 2008-04-02 proofs adjusted to new situation in Int.thy/Presburger.thy
2008-04-02 haftmann 2008-04-02 explicit instantiation
2008-04-02 haftmann 2008-04-02 tuned proof
2008-04-02 haftmann 2008-04-02 dropped wrong code lemma
2008-04-02 haftmann 2008-04-02 moved some code lemmas for Numerals to other theories
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;