| Fri, 18 Oct 2013 10:43:20 +0200 |
blanchet |
killed most "no_atp", to make Sledgehammer more complete
|
file |
diff |
annotate
|
| Tue, 27 Aug 2013 16:06:27 +0200 |
hoelzl |
renamed inner_dense_linorder to dense_linorder
|
file |
diff |
annotate
|
| Tue, 27 Aug 2013 14:37:56 +0200 |
hoelzl |
renamed typeclass dense_linorder to unbounded_dense_linorder
|
file |
diff |
annotate
|
| Thu, 25 Jul 2013 08:57:16 +0200 |
haftmann |
factored syntactic type classes for bot and top (by Alessandro Coglio)
|
file |
diff |
annotate
|
| Sat, 25 May 2013 15:37:53 +0200 |
wenzelm |
syntax translations always depend on context;
|
file |
diff |
annotate
|
| Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| Tue, 09 Apr 2013 15:29:25 +0200 |
wenzelm |
discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
|
file |
diff |
annotate
|
| Fri, 29 Mar 2013 22:13:02 +0100 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Tue, 26 Mar 2013 21:53:56 +0100 |
haftmann |
more uniform style for interpretation and sublocale declarations
|
file |
diff |
annotate
|
| Sat, 23 Mar 2013 17:11:06 +0100 |
haftmann |
locales for abstract orders
|
file |
diff |
annotate
|
| Wed, 20 Feb 2013 12:04:42 +0100 |
hoelzl |
split dense into inner_dense_order and no_top/no_bot
|
file |
diff |
annotate
|
| Sun, 24 Feb 2013 20:29:13 +0100 |
haftmann |
turned example into library for comparing growth of functions
|
file |
diff |
annotate
|
| Wed, 10 Oct 2012 12:52:24 +0200 |
haftmann |
more explicit code equations
|
file |
diff |
annotate
|
| Sat, 29 Sep 2012 18:23:46 +0200 |
wenzelm |
more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 22:55:41 +0200 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
| Thu, 12 Apr 2012 18:39:19 +0200 |
wenzelm |
more standard method setup;
|
file |
diff |
annotate
|
| Sat, 17 Mar 2012 09:51:18 +0100 |
wenzelm |
'definition' no longer exports the foundational "raw_def";
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 18:20:12 +0100 |
wenzelm |
outer syntax command definitions based on formal command_spec derived from theory header declarations;
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 22:08:53 +0100 |
wenzelm |
declare command keywords via theory header, including strict checking outside Pure;
|
file |
diff |
annotate
|
| Mon, 12 Mar 2012 21:41:11 +0100 |
noschinl |
tuned proofs
|
file |
diff |
annotate
|
| Mon, 12 Mar 2012 15:11:24 +0100 |
noschinl |
tuned simpset
|
file |
diff |
annotate
|
| Sun, 26 Feb 2012 20:10:14 +0100 |
haftmann |
tuned syntax declarations; tuned structure
|
file |
diff |
annotate
|
| Sun, 26 Feb 2012 15:28:48 +0100 |
haftmann |
marked candidates for rule declarations
|
file |
diff |
annotate
|
| Thu, 23 Feb 2012 20:33:35 +0100 |
haftmann |
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
|
file |
diff |
annotate
|
| Tue, 21 Feb 2012 08:15:42 +0100 |
haftmann |
reverting changesets from 5d33a3269029 on: change of order of declaration of classical rules makes serious problems
|
file |
diff |
annotate
|
| Sun, 19 Feb 2012 15:30:35 +0100 |
haftmann |
distributed lattice properties of predicates to places of instantiation
|
file |
diff |
annotate
|
| Mon, 19 Dec 2011 14:41:08 +0100 |
noschinl |
weaken preconditions on lemmas
|
file |
diff |
annotate
|
| Thu, 15 Dec 2011 16:10:44 +0100 |
noschinl |
add complementary lemmas for {min,max}_least
|
file |
diff |
annotate
|
| Mon, 24 Oct 2011 16:47:24 +0200 |
huffman |
instance bool :: linorder
|
file |
diff |
annotate
|
| Mon, 24 Oct 2011 12:26:05 +0200 |
bulwahn |
removing poor man's dictionary construction which were only for the ancient code generator with no support of type classes
|
file |
diff |
annotate
|
| Fri, 21 Oct 2011 11:17:14 +0200 |
bulwahn |
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
|
file |
diff |
annotate
|
| Thu, 20 Oct 2011 22:26:02 +0200 |
blanchet |
mark "xt..." rules as "no_atp", since they are easy consequences of other better named properties
|
file |
diff |
annotate
|
| Tue, 13 Sep 2011 17:07:33 -0700 |
huffman |
tuned proofs
|
file |
diff |
annotate
|
| Mon, 08 Aug 2011 17:23:15 +0200 |
wenzelm |
misc tuning -- eliminated old-fashioned rep_thm;
|
file |
diff |
annotate
|
| Wed, 03 Aug 2011 23:21:52 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Sat, 16 Jul 2011 22:04:02 +0200 |
haftmann |
consolidated bot and top classes, tuned notation
|
file |
diff |
annotate
|
| Wed, 13 Jul 2011 23:49:56 +0200 |
haftmann |
uniqueness lemmas for bot and top
|
file |
diff |
annotate
|
| Wed, 13 Jul 2011 19:43:12 +0200 |
haftmann |
moved lemmas bot_less and less_top to classes bot and top respectively
|
file |
diff |
annotate
|
| Wed, 13 Jul 2011 19:40:18 +0200 |
haftmann |
tightened specification of classes bot and top: uniqueness of top and bot elements
|
file |
diff |
annotate
|
| Wed, 29 Jun 2011 21:34:16 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 29 Jun 2011 20:39:41 +0200 |
wenzelm |
simplified/unified Simplifier.mk_solver;
|
file |
diff |
annotate
|
| Fri, 13 May 2011 23:58:40 +0200 |
wenzelm |
clarified map_simpset versus Simplifier.map_simpset_global;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 14:20:57 +0200 |
wenzelm |
discontinued special treatment of structure Mixfix;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 13:31:16 +0200 |
wenzelm |
explicit structure Syntax_Trans;
|
file |
diff |
annotate
|
| Wed, 08 Dec 2010 15:05:46 +0100 |
haftmann |
bot comes before top, inf before sup etc.
|
file |
diff |
annotate
|
| Wed, 08 Dec 2010 14:52:23 +0100 |
haftmann |
nice syntax for lattice INFI, SUPR;
|
file |
diff |
annotate
|
| Wed, 08 Dec 2010 13:34:50 +0100 |
haftmann |
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 10:56:46 +0200 |
haftmann |
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 20:51:17 +0200 |
haftmann |
formerly unnamed infix impliciation now named HOL.implies
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 18:36:22 +0200 |
wenzelm |
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
| Tue, 24 Aug 2010 14:41:37 +0200 |
hoelzl |
moved generic lemmas in Probability to HOL
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 14:21:57 +0200 |
blanchet |
"no_atp" fact that leads to unsound proofs in Sledgehammer
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 10:48:37 +0200 |
haftmann |
dropped superfluous [code del]s
|
file |
diff |
annotate
|
| Mon, 17 May 2010 23:54:15 +0200 |
wenzelm |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
|
file |
diff |
annotate
|
| Tue, 04 May 2010 08:55:43 +0200 |
haftmann |
locale predicates of classes carry a mandatory "class" prefix
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 12:58:52 +0100 |
blanchet |
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
|
file |
diff |
annotate
|
| Thu, 04 Mar 2010 18:42:39 +0100 |
hoelzl |
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
|
file |
diff |
annotate
|
| Thu, 25 Feb 2010 22:32:09 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Mon, 22 Feb 2010 15:53:18 +0100 |
haftmann |
distributed theory Algebras to theories Groups and Lattices
|
file |
diff |
annotate
|
| Thu, 11 Feb 2010 23:00:22 +0100 |
wenzelm |
modernized translations;
|
file |
diff |
annotate
|