| Wed, 17 Apr 2019 16:57:06 +0000 |
haftmann |
backed out experimental b67bab2b132c, which slipped in accidentally
|
file |
diff |
annotate
|
| Tue, 16 Apr 2019 19:50:30 +0000 |
haftmann |
hierarchically inclusive named theorem collections
|
file |
diff |
annotate
|
| Wed, 06 Dec 2017 20:43:09 +0100 |
wenzelm |
prefer control symbol antiquotations;
|
file |
diff |
annotate
|
| Mon, 27 Jul 2015 17:44:55 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 08 Apr 2015 19:39:08 +0200 |
wenzelm |
proper context for Object_Logic operations;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 22:05:01 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Sun, 09 Nov 2014 14:08:00 +0100 |
wenzelm |
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
|
file |
diff |
annotate
|
| Sat, 16 Aug 2014 13:54:19 +0200 |
wenzelm |
updated to named_theorems;
|
file |
diff |
annotate
|
| Sat, 16 Aug 2014 13:23:50 +0200 |
wenzelm |
modernized module name and setup;
|
file |
diff |
annotate
|
| Sat, 14 Dec 2013 17:28:05 +0100 |
wenzelm |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
|
file |
diff |
annotate
|
| Fri, 28 Oct 2011 23:41:16 +0200 |
wenzelm |
tuned Named_Thms: proper binding;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Thu, 24 Mar 2011 16:56:19 +0100 |
wenzelm |
added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 17:08:56 +0100 |
wenzelm |
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 12:19:47 +0100 |
wenzelm |
modernized structure Object_Logic;
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 10:15:31 +0200 |
haftmann |
removed old-style \ and \\ infixes
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 20:54:31 +0200 |
wenzelm |
uniform use of Integer.min/max;
|
file |
diff |
annotate
|
| Mon, 19 Oct 2009 21:54:57 +0200 |
wenzelm |
uniform use of Integer.add/mult/sum/prod;
|
file |
diff |
annotate
|
| Thu, 02 Jul 2009 17:34:14 +0200 |
wenzelm |
renamed NamedThmsFun to Named_Thms;
|
file |
diff |
annotate
|
| Fri, 13 Mar 2009 23:50:05 +0100 |
wenzelm |
simplified method setup;
|
file |
diff |
annotate
|
| Fri, 13 Mar 2009 19:58:26 +0100 |
wenzelm |
unified type Proof.method and pervasive METHOD combinators;
|
file |
diff |
annotate
|
| Sat, 28 Feb 2009 14:09:58 +0100 |
wenzelm |
removed Ids;
|
file |
diff |
annotate
|
| Mon, 14 Jul 2008 17:02:55 +0200 |
krauss |
renamed conversions to _conv, tuned
|
file |
diff |
annotate
|
| Tue, 08 Apr 2008 20:09:54 +0200 |
krauss |
added missing file
|
file |
diff |
annotate
|