src/Pure/Isar/isar_thy.ML
2004-04-02 ballarin 2004-04-02 Experimental command for instantiation of locales in proof contexts: instantiate <label>: <loc>
2004-03-31 skalberg 2004-03-31 Added check that Theory.ML does not occur in the files section of the theory Theory.
2002-10-30 nipkow 2002-10-30 modified msg
2002-08-27 wenzelm 2002-08-27 check_goal: produce error instead of warning;
2002-07-18 wenzelm 2002-07-18 adapted add_locale;
2002-07-16 wenzelm 2002-07-16 add_locale: adapted args;
2002-07-02 wenzelm 2002-07-02 ProofContext.pretty_fact;
2002-02-27 wenzelm 2002-02-27 tuned local goal forms;
2002-02-26 wenzelm 2002-02-26 clarified multi statements;
2002-02-25 wenzelm 2002-02-25 markup commands moved to isar_cmd.ML;
2002-02-24 wenzelm 2002-02-24 added using_facts;
2002-02-12 wenzelm 2002-02-12 got rid of explicit marginal comments (now stripped earlier from input);
2002-01-24 wenzelm 2002-01-24 cond_print_result_rule: priority (again) instead of slightly ill-behaved tracing output;
2002-01-15 wenzelm 2002-01-15 tuned;
2002-01-11 wenzelm 2002-01-11 clarified/added theorems(_i) vs. locale_theorems(_i); clarified IsarThy.apply_theorems_i; localized smart_theorems, declare_theorems; removed declare_theorems_i;
2002-01-10 wenzelm 2002-01-10 tuned;
2002-01-10 wenzelm 2002-01-10 export multi_theorem(_i), locale_multi_theorem(_i);
2002-01-10 wenzelm 2002-01-10 simplified theorem(_i); smart_multi_theorem;
2001-12-27 wenzelm 2001-12-27 solve rule: tracing instead of priority;
2001-12-21 wenzelm 2001-12-21 Theory.hide_space_i true;
2001-11-28 wenzelm 2001-11-28 skip_proof: do not require quick_and_dirty in interactive mode;
2001-11-22 wenzelm 2001-11-22 locale expression import;
2001-11-19 wenzelm 2001-11-19 improved treatment of common result name;
2001-11-19 wenzelm 2001-11-19 multi_theorem: common statement header (covers *all* results);
2001-11-11 wenzelm 2001-11-11 theorem, have, show etc: multiple statements;
2001-11-06 wenzelm 2001-11-06 theorem(_i): locale atts; added add_locale;
2001-11-05 wenzelm 2001-11-05 pretty/print functions with context;
2001-11-04 wenzelm 2001-11-04 theorem(_i): locale elements;
2001-10-31 wenzelm 2001-10-31 global statements: locale argument;
2001-10-25 wenzelm 2001-10-25 check_goal: setmp proofs 0;
2001-10-22 wenzelm 2001-10-22 improved source arrangement of obtain;
2001-10-16 wenzelm 2001-10-16 support impromptu terminology of cases parameters;
2001-10-14 wenzelm 2001-10-14 use ObjectLogic;
2001-10-13 wenzelm 2001-10-13 generic theorem kinds;
2001-10-10 berghofe 2001-10-10 Fixed erroneous type constraint in token_translation function.
2001-02-03 wenzelm 2001-02-03 tuned msg;
2001-01-18 wenzelm 2001-01-18 show/thus: check_goal;
2000-11-13 wenzelm 2000-11-13 tuned statement args;
2000-11-10 wenzelm 2000-11-10 hide_space(_i): use Sign.certify_tycon, Sign.certify_tyabbr, Sign.certify_const;
2000-09-07 wenzelm 2000-09-07 print rule: priority;
2000-09-02 wenzelm 2000-09-02 method_setup: thms closure;
2000-08-14 wenzelm 2000-08-14 added declare_theorems(_i); adapted Context.use_let;
2000-07-30 wenzelm 2000-07-30 local_def(_i): no constraint on var;
2000-07-13 wenzelm 2000-07-13 add_defs(_i): overloaded option;
2000-07-06 wenzelm 2000-07-06 allow comment in more commands;
2000-06-29 wenzelm 2000-06-29 have_theorems etc.: handle multiple lists of arguments; added method_setup;
2000-06-03 wenzelm 2000-06-03 block commands: marginal comment;
2000-05-24 wenzelm 2000-05-24 added "done" proof;
2000-05-21 wenzelm 2000-05-21 adapted to inner syntax of sorts;
2000-05-18 wenzelm 2000-05-18 hide: check declared;
2000-05-18 wenzelm 2000-05-18 'apply' consumes facts;
2000-05-05 wenzelm 2000-05-05 GPLed; improved begin_theory ('files' may change theory);
2000-04-17 wenzelm 2000-04-17 made SML/NJ happy;
2000-04-17 wenzelm 2000-04-17 global/local_path: comment; added name space hide;
2000-04-07 wenzelm 2000-04-07 apply etc.: comments;
2000-03-30 wenzelm 2000-03-30 let_bind(_i): polymorphic version;
2000-03-26 wenzelm 2000-03-26 added 'ultimately';
2000-03-23 wenzelm 2000-03-23 added 'moreover' command;
2000-03-15 wenzelm 2000-03-15 removed export_chain;
2000-03-14 wenzelm 2000-03-14 invoke_case: include attributes;