| Tue, 31 Dec 2013 14:29:16 +0100 |
wenzelm |
proper context for norm_hhf and derived operations;
|
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
|
| Thu, 05 Dec 2013 09:20:32 +0100 |
Andreas Lochbihler |
restrict admissibility to non-empty chains to allow more syntax-directed proof rules
|
file |
diff |
annotate
|
| Tue, 12 Nov 2013 13:47:24 +0100 |
blanchet |
ported 'partial_function' to 'Ctr_Sugar' abstraction
|
file |
diff |
annotate
|
| Wed, 24 Jul 2013 17:15:59 +0200 |
krauss |
derive specialized version of full fixpoint induction (with admissibility)
|
file |
diff |
annotate
|
| Wed, 24 Jul 2013 15:29:23 +0200 |
krauss |
export mono_thm
|
file |
diff |
annotate
|
| Wed, 03 Jul 2013 00:08:29 +0200 |
krauss |
more robust instantiation: extract vars from conclusion instead of relying on fixed overall ordering
|
file |
diff |
annotate
|
| Mon, 20 May 2013 17:14:39 +0200 |
wenzelm |
more precise treatment of theory vs. Proof.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
|
| Fri, 22 Mar 2013 00:39:14 +0100 |
krauss |
allow induction predicates with arbitrary arity (not just binary)
|
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 20:07:00 +0100 |
wenzelm |
prefer formally checked @{keyword} parser;
|
file |
diff |
annotate
|
| Tue, 08 Nov 2011 11:44:37 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 28 Oct 2011 23:41:16 +0200 |
wenzelm |
tuned Named_Thms: proper binding;
|
file |
diff |
annotate
|
| Tue, 20 Sep 2011 01:32:04 +0200 |
krauss |
match types when applying mono_thm -- previous export generalizes type variables;
|
file |
diff |
annotate
|