src/Pure/Isar/isar_thy.ML
2005-04-13 wenzelm 2005-04-13 *** empty log message ***
2005-04-11 ballarin 2005-04-11 First release of interpretation commands.
2005-03-24 ballarin 2005-03-24 Further work on interpretation commands. New command `interpret' for interpretation in proof contexts.
2005-03-10 ballarin 2005-03-10 Registrations of global locale interpretations: improved, better naming.
2005-03-09 ballarin 2005-03-09 First version of global registration command.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2005-01-24 berghofe 2005-01-24 Specific theorems in a named list of theorems can now be referred to via indices (type thmref).
2004-10-11 berghofe 2004-10-11 Some changes to allow skipping of proof scripts.
2004-09-27 ballarin 2004-09-27 Modified locales: improved implementation of "includes".
2004-08-12 ballarin 2004-08-12 Disallowed "includes" in locale declarations.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-05-29 wenzelm 2004-05-29 transform_error;
2004-05-21 wenzelm 2004-05-21 Sign.certify_tyname;
2004-04-22 wenzelm 2004-04-22 removed add_constdefs(_i), see constdefs.ML for improved version; advanced translation functions;
2004-04-16 berghofe 2004-04-16 Replaced quote by Library.quote, since quote now refers to Symbol.quote
2004-04-14 wenzelm 2004-04-14 renamed have_thms to note_thms;
2004-04-07 ballarin 2004-04-07 Locale instantiation: label parameter optional, new attribute paramter.
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;