2000-03-08 wenzelm 2000-03-08 invoke_case: name assumption;
2000-03-08 wenzelm 2000-03-08 fixed section syntax;
2000-03-08 wenzelm 2000-03-08 sect: exlude ":" from parser;
2000-03-08 wenzelm 2000-03-08 removed tune_names;
2000-03-08 wenzelm 2000-03-08 tuned ML types; improved translation functions; 'case' command; 'oops' command; "Emulating tactic scripts";
2000-03-08 wenzelm 2000-03-08 tuned;
2000-03-08 wenzelm 2000-03-08 added \CASE, \OBTAIN, \SORRY, \OOPS; removed \SUFF;
2000-03-08 wenzelm 2000-03-08 added dest_global/local_rules; cases/induct: tuned rule selection, always admit insts; accomodate rule case names;
2000-03-08 wenzelm 2000-03-08 mk_elims, add_cases_induct: name rule cases;
2000-03-08 wenzelm 2000-03-08 generalized FINDGOAL, HEADGOAL; handling of local contexts: method_cases, invoke_case;
2000-03-08 wenzelm 2000-03-08 handling of local contexts: print_cases, get_case, add_cases;
2000-03-08 wenzelm 2000-03-08 added METHOD_CASES, resolveq_cases_tac; removed multi_resolveq; improved 'tactic' method: bind thm(s) function;
2000-03-08 wenzelm 2000-03-08 added invoke_case;
2000-03-08 wenzelm 2000-03-08 added 'case' command; added 'print_cases' command;
2000-03-08 wenzelm 2000-03-08 added print_cases;
2000-03-08 wenzelm 2000-03-08 added 'case_names' and 'params';
2000-03-08 wenzelm 2000-03-08 added rule_cases.ML;
2000-03-08 wenzelm 2000-03-08 export ALLGOALS_RANGE;
2000-03-08 wenzelm 2000-03-08 added (un)tag_rule;
2000-03-08 wenzelm 2000-03-08 added Isar/rule_cases.ML;
2000-03-08 wenzelm 2000-03-08 added isatool mkdir; isatool document -c; isatool usedir -D -c;
2000-03-08 wenzelm 2000-03-08 isabelle -c: tell ML system to compress output image;
2000-03-08 wenzelm 2000-03-08 pass -c option;
2000-03-08 wenzelm 2000-03-08 observe COMPRESS option;
2000-03-08 wenzelm 2000-03-08 option -c: tell ML system to compress output image;
2000-03-08 wenzelm 2000-03-08 * isatool mkdir provides easy setup of Isabelle session directories, including proper documents; * generated LaTeX sources are now deleted after successful run (isatool document -c); may retain a copy somewhere else via -D option of isatool usedir; * old-style theories now produce (crude) LaTeX sources as well; * compression of ML heaps images may now be controlled via -c option of isabelle and isatool usedir;
2000-03-08 wenzelm 2000-03-08 tuned error msg: rows counted from 1;
2000-03-08 paulson 2000-03-08 tidied
2000-03-08 paulson 2000-03-08 tidied
2000-03-08 paulson 2000-03-08 function "remove" and new lemmas for Factorization
2000-03-08 paulson 2000-03-08 new theory ex/Factorization
2000-03-08 paulson 2000-03-08 new lemmas
2000-03-06 wenzelm 2000-03-06 added simple_args; added 'tactic' method;
2000-03-06 wenzelm 2000-03-06 argument: include verbatim;
2000-03-06 wenzelm 2000-03-06 moved use_mltext, use_mltext_theory, use_let, use_setup to context.ML;
2000-03-06 wenzelm 2000-03-06 added use_mltext, use_mltext_theory, use_let, use_setup (from isar_thy.ML);
2000-03-06 wenzelm 2000-03-06 rsyncd setup; --delete mode (beware!);
2000-03-06 kleing 2000-03-06 switched to mirroring with rsync server
2000-03-06 wenzelm 2000-03-06 new Poly/ML setup made default;
2000-03-04 wenzelm 2000-03-04 induct: "stripped" option;
2000-03-04 wenzelm 2000-03-04 require NatDef;
2000-03-04 wenzelm 2000-03-04 REPEAT_ALL_NEW;
2000-03-04 wenzelm 2000-03-04 added REPEAT_ALL_NEW;
2000-03-04 paulson 2000-03-04 tidied
2000-03-04 paulson 2000-03-04 tidied
2000-03-04 paulson 2000-03-04 new theories UNITY/Detects, UNITY/Reachability
2000-03-03 wenzelm 2000-03-03 added con_elim_s(olved_)tac; added 'simplified' flag;
2000-03-03 wenzelm 2000-03-03 mk_cases / inductive_cases: use InductMethod.con_elim_(solved_)tac;
2000-03-03 wenzelm 2000-03-03 added multi_resolveq, resolveq_tac;
2000-03-03 paulson 2000-03-03 Added Tanja's Detects and Reachability theories. Also changed object-quantifiers to meta-quantifiers in ball_constrains_UN/INT...
2000-03-03 paulson 2000-03-03 improved reasoning about {} and UNIV
2000-03-03 wenzelm 2000-03-03 join_rules: compatibility check;
2000-03-03 wenzelm 2000-03-03 token_trans: symbol length;
2000-03-02 wenzelm 2000-03-02 join induct rules;
2000-03-02 wenzelm 2000-03-02 added 'prolog' method;
2000-03-02 wenzelm 2000-03-02 added freeze_all; tuned spacing;
2000-03-02 paulson 2000-03-02 polished version of the Allocator using Rename
2000-03-02 paulson 2000-03-02 tidied the proofs of singleton_insert_inj_eq, singleton_insert_inj_eq' and installed them by AddIffs, since they are an important special case of equalityE.
2000-03-01 wenzelm 2000-03-01 project induct rule;
2000-03-01 wenzelm 2000-03-01 tuned;