isabelle: Changelog

more opportunistic string_of_clause, to make double-sure its Syntax.string_of_term uncheck phase does not crash, and thus bomb ambiguous input via failed composition of warning (e.g. HOL/Imperative_HOL/ex/Linked_List.thy: lemma merge_simps);

Wed, 17 Jul 2013 21:04:38 +0200 tuned spelling;

changeset

wenzelm [Wed, 17 Jul 2013 21:04:38 +0200] rev 52689

tuned spelling;

Wed, 17 Jul 2013 12:41:59 +0900 show variants in error messages; more precise error messages (give witnesses for multiple instances)

changeset

Christian Sternagel [Wed, 17 Jul 2013 12:41:59 +0900] rev 52688

show variants in error messages; more precise error messages (give witnesses for multiple instances)

Wed, 17 Jul 2013 12:19:14 +0900 refactoring

changeset

Christian Sternagel [Wed, 17 Jul 2013 12:19:14 +0900] rev 52687

refactoring

Wed, 17 Jul 2013 17:16:51 +0200 more robust exn_messages_ids;

changeset

wenzelm [Wed, 17 Jul 2013 17:16:51 +0200] rev 52686

more robust exn_messages_ids; more robust failure of exn_messages_ids;

Wed, 17 Jul 2013 14:33:33 +0200 non-strict "Quiet" mode, to avoid odd crash of code_pred/after_qed due to ill-typed use of string_of_clause (e.g. in JinjaThreads/Common/Decl.thy of AFP/d1bb08f92ce5);

changeset

wenzelm [Wed, 17 Jul 2013 14:33:33 +0200] rev 52685

non-strict "Quiet" mode, to avoid odd crash of code_pred/after_qed due to ill-typed use of string_of_clause (e.g. in JinjaThreads/Common/Decl.thy of AFP/d1bb08f92ce5);

Wed, 17 Jul 2013 13:45:55 +0200 take context from static theory, not dynamic theory certificate;

changeset

wenzelm [Wed, 17 Jul 2013 13:45:55 +0200] rev 52684

take context from static theory, not dynamic theory certificate;

Wed, 17 Jul 2013 11:38:57 +0200 more official Thm.eq_thm_strict, without demanding ML equality type;

changeset

wenzelm [Wed, 17 Jul 2013 11:38:57 +0200] rev 52683

more official Thm.eq_thm_strict, without demanding ML equality type;

Wed, 17 Jul 2013 09:32:08 +0200 tuned;

changeset

wenzelm [Wed, 17 Jul 2013 09:32:08 +0200] rev 52682

tuned;