2008-07-15 haftmann 2008-07-15 tuned code theorem bookkeeping
2008-07-15 wenzelm 2008-07-15 tuned changelogentry;
2008-07-15 wenzelm 2008-07-15 refined Output.status_fn: priority (only visible for non-empty output, e.g. via test_markup print mode);
2008-07-15 wenzelm 2008-07-15 support for command status;
2008-07-15 wenzelm 2008-07-15 added status channel; writeln_default: suppress empty messages;
2008-07-15 wenzelm 2008-07-15 added status channel;
2008-07-15 wenzelm 2008-07-15 tuned;
2008-07-15 wenzelm 2008-07-15 simplified commit_exit;
2008-07-15 wenzelm 2008-07-15 simplified commit_exit: operate on previous node of final state, include warning here; misc tuning;
2008-07-15 wenzelm 2008-07-15 removed obsolete commit_exit;
2008-07-15 wenzelm 2008-07-15 added command 'linear_undo'; tuned;
2008-07-15 wenzelm 2008-07-15 removed command 'redo'; added command 'linear_undo';
2008-07-15 wenzelm 2008-07-15 adapted ThyInfo.end_theory;
2008-07-15 haftmann 2008-07-15 dropped map; fixed swap
2008-07-15 haftmann 2008-07-15 curried gcd
2008-07-14 wenzelm 2008-07-14 cover macbroy as well; tuned;
2008-07-14 wenzelm 2008-07-14 tuned filelogentry;
2008-07-14 wenzelm 2008-07-14 print_mode "test_markup": do not change prompt, otherwise Proof General will not work;
2008-07-14 wenzelm 2008-07-14 tuned message;
2008-07-14 wenzelm 2008-07-14 updated generated file;
2008-07-14 wenzelm 2008-07-14 inform_file_processed: Isar.init_point last!
2008-07-14 wenzelm 2008-07-14 removed HOL-Complex, which has been discontinued after Isabelle2008;
2008-07-14 wenzelm 2008-07-14 added HOL-Nominal image;
2008-07-14 wenzelm 2008-07-14 removed obsolete Pure/General/history.ML;
2008-07-14 wenzelm 2008-07-14 inform_file_processed: try harder not to fail, ensure
2008-07-14 wenzelm 2008-07-14 commit_exit: proper error;
2008-07-14 wenzelm 2008-07-14 export EXCURSION_FAIL;
2008-07-14 haftmann 2008-07-14 dropped junk
2008-07-14 haftmann 2008-07-14 moved bootstrap of simplifier
2008-07-14 haftmann 2008-07-14 tuned
2008-07-14 wenzelm 2008-07-14 end_theory: no result;
2008-07-14 wenzelm 2008-07-14 removed obsolete Toplevel.RESTART;
2008-07-14 wenzelm 2008-07-14 proper_inform_file_processed: new implementation based on global Isar state (cf. isar.ML); removed obsolete Toplevel.RESTART;
2008-07-14 wenzelm 2008-07-14 eliminated internal command history -- superceeded by global Isar state (cf. isar.ML); added commit_exit; removed obsolete exception RESTART; init_theory: removed obsolete kill argument; removed obsolete undo_limit, undo_exit, kill, history; misc tuning;
2008-07-14 wenzelm 2008-07-14 adapted IsarCmd.init_theory;
2008-07-14 wenzelm 2008-07-14 renamed theory to init_theory, removed obsolete kill argument; removed unused init_toplevel, begin_theory, end_theory; print_theorems: Toplevel.previous_node_of;
2008-07-14 wenzelm 2008-07-14 added commit_exit;
2008-07-14 krauss 2008-07-14 single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
2008-07-14 krauss 2008-07-14 renamed conversions to _conv, tuned
2008-07-14 chaieb 2008-07-14 Simplified proofs
2008-07-14 chaieb 2008-07-14 Simple theorems about zgcd moved to GCD.thy
2008-07-14 chaieb 2008-07-14 Theorem names as in IntPrimes.thy, also several theorems moved from there
2008-07-14 chaieb 2008-07-14 Fixed proofs.
2008-07-14 wenzelm 2008-07-14 ProofNode.current
2008-07-14 wenzelm 2008-07-14 command 'redo' no longer available;
2008-07-14 wenzelm 2008-07-14 replaced obsolete ProofHistory by ProofNode (backtracking only);
2008-07-14 wenzelm 2008-07-14 removed obsolete 'redo' command; cannot_undo: global history; tuned;
2008-07-14 wenzelm 2008-07-14 removed obsolete history commands; moved back, cannot_undo to isar_syn.ML;
2008-07-14 wenzelm 2008-07-14 Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
2008-07-14 wenzelm 2008-07-14 obsolete (cf. proof_node.ML);
2008-07-14 wenzelm 2008-07-14 removed Isar/proof_history.ML; added Isar/proof_node.ML
2008-07-14 haftmann 2008-07-14 added further simple interfaces
2008-07-14 haftmann 2008-07-14 simpsets as pre/postprocessors; generic preprocessor now named function transformators
2008-07-14 haftmann 2008-07-14 unified curried gcd, lcm, zgcd, zlcm
2008-07-11 wenzelm 2008-07-11 Sorts.weaken: abstract argument; tuned;
2008-07-11 wenzelm 2008-07-11 Sorts.weaken: abstract argument;
2008-07-11 huffman 2008-07-11 instance real_field < field_char_0; instance star :: (field_char_0) field_char_0
2008-07-11 haftmann 2008-07-11 re-removed subclass relation real_field < field_char_0: coregularity violation in NSA/HyperDef
2008-07-11 haftmann 2008-07-11 Fract now total; improved code generator setup
2008-07-11 haftmann 2008-07-11 simple inheritance concept