2000-05-30 berghofe 2000-05-30 the is now defined using primrec, avoiding explicit use of arbitrary.
2000-05-30 wenzelm 2000-05-30 cleaned up;
2000-05-30 wenzelm 2000-05-30 global timing flag;
2000-05-30 wenzelm 2000-05-30 fixed comment;
2000-05-30 wenzelm 2000-05-30 renamed trace/stat_norm_ast to trace/stat_ast;
2000-05-30 wenzelm 2000-05-30 renamed Syntax.trace_norm_ast to Syntax.trace_ast; removed Syntax.stat_norm_ast;
2000-05-30 wenzelm 2000-05-30 proof_timing replaced by global timing;
2000-05-30 wenzelm 2000-05-30 * ML: renamed flags Syntax.trace_norm_ast to Syntax.trace_ast; global timing flag supersedes proof_timing and Toplevel.trace;
2000-05-28 wenzelm 2000-05-28 Collect_neg_eq;
2000-05-28 wenzelm 2000-05-28 \newcommand{\indexisarcase};
2000-05-28 wenzelm 2000-05-28 case 'antecedent';
2000-05-26 wenzelm 2000-05-26 write major keywords;
2000-05-26 paulson 2000-05-26 sublist and some lemmas about it
2000-05-26 paulson 2000-05-26 a more robust proof
2000-05-26 paulson 2000-05-26 fixed the dependences
2000-05-26 paulson 2000-05-26 tidied
2000-05-26 paulson 2000-05-26 restored some of the lessThans
2000-05-26 paulson 2000-05-26 addss -> force_tac
2000-05-26 paulson 2000-05-26 named the primrec clauses of upt
2000-05-26 paulson 2000-05-26 renamed upt_Suc, since that name is needed for its primrec rule
2000-05-26 paulson 2000-05-26 new setsum results
2000-05-26 wenzelm 2000-05-26 tuned case_tac;
2000-05-26 paulson 2000-05-26 updated acknowledgements
2000-05-26 paulson 2000-05-26 fixed the documentation of goalw_cterm and prove_goalw_cterm
2000-05-25 paulson 2000-05-25 res_inst_tac, etc., no longer print the "dest_state" message when the selected subgoal does not exist
2000-05-25 paulson 2000-05-25 setsum replaces sum_below
2000-05-25 paulson 2000-05-25 moved mostly to HOL/SetInterval.ML and UNITY/UNITY.ML
2000-05-25 paulson 2000-05-25 sum_below moved here from Arith
2000-05-25 paulson 2000-05-25 improved error msgs, listing variable names
2000-05-25 paulson 2000-05-25 better indentation; declared function "null"
2000-05-25 paulson 2000-05-25 new default rules
2000-05-25 paulson 2000-05-25 deleted sum_below: no need for it with setsum and lessThan
2000-05-25 paulson 2000-05-25 documented permute_prems
2000-05-25 paulson 2000-05-25 better indentation
2000-05-25 paulson 2000-05-25 overloading of 0
2000-05-24 wenzelm 2000-05-24 added "done" proof;
2000-05-24 wenzelm 2000-05-24 proper token_translation for latex mode;
2000-05-24 paulson 2000-05-24 some lemmas about plus_ac0
2000-05-24 paulson 2000-05-24 setsum is now overloaded on plus_ac0; lemmas about lessThan, etc.
2000-05-24 paulson 2000-05-24 setsum is now overloaded on plus_ac0
2000-05-24 paulson 2000-05-24 installing plus_ac0 for nat
2000-05-24 paulson 2000-05-24 we must not require SetInterval this early
2000-05-24 paulson 2000-05-24 installing the plus_ac0 axclass
2000-05-24 paulson 2000-05-24 Adding SetInterval, deleting UNITY/LessThan
2000-05-24 paulson 2000-05-24 added parent
2000-05-24 paulson 2000-05-24 facts about lessThan, etc., mostly from UNITY/LessThan
2000-05-24 paulson 2000-05-24 installing the plus_ac0 simprules
2000-05-24 paulson 2000-05-24 rewrote a very long proof (Key_analz_image_Key) because it had stopped working
2000-05-24 paulson 2000-05-24 overloaded 0
2000-05-24 paulson 2000-05-24 tidying for overloaded 0, setsum, etc.
2000-05-24 paulson 2000-05-24 installing plus_ac0 for multisets
2000-05-24 paulson 2000-05-24 replacing "below" by "lessThan"
2000-05-24 paulson 2000-05-24 installing plus_ac0 for int
2000-05-24 paulson 2000-05-24 restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
2000-05-24 wenzelm 2000-05-24 tuned;
2000-05-24 wenzelm 2000-05-24 "done" command;
2000-05-24 wenzelm 2000-05-24 fixed index;
2000-05-24 paulson 2000-05-24 restored NatSum.thy
2000-05-23 paulson 2000-05-23 now 0 is overloaded
2000-05-23 paulson 2000-05-23 added type constraint ::nat because 0 is now overloaded