Mon, 10 Nov 2014 21:49:48 +0100 |
wenzelm |
proper context for assume_tac (atac remains as fall-back without context);
|
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
|
Wed, 09 Apr 2014 12:22:57 +0200 |
wenzelm |
proper context for print_tac;
|
file |
diff |
annotate
|
Wed, 09 Apr 2014 11:32:41 +0200 |
wenzelm |
more conventional tactic programming;
|
file |
diff |
annotate
|
Fri, 21 Feb 2014 00:09:56 +0100 |
blanchet |
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
|
file |
diff |
annotate
|
Wed, 12 Feb 2014 14:32:45 +0100 |
wenzelm |
merged, resolving some conflicts;
|
file |
diff |
annotate
|
Wed, 12 Feb 2014 13:33:05 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
Wed, 12 Feb 2014 08:37:28 +0100 |
blanchet |
tuned message
|
file |
diff |
annotate
|
Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
ported predicate compiler to 'ctr_sugar'
|
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
|
Sat, 27 Jul 2013 16:35:51 +0200 |
wenzelm |
standardized aliases;
|
file |
diff |
annotate
|
Thu, 30 May 2013 12:35:40 +0200 |
wenzelm |
standardized aliases;
|
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
|
Wed, 27 Mar 2013 14:50:30 +0100 |
wenzelm |
clarified Skip_Proof.cheat_tac: more standard tactic;
|
file |
diff |
annotate
|
Mon, 12 Nov 2012 23:24:40 +0100 |
haftmann |
dropped dead code
|
file |
diff |
annotate
|
Tue, 14 Feb 2012 17:26:35 +0100 |
wenzelm |
eliminated obsolete aliases;
|
file |
diff |
annotate
|
Wed, 30 Nov 2011 23:30:08 +0100 |
wenzelm |
discontinued obsolete datatype "alt_names";
|
file |
diff |
annotate
|
Sun, 27 Nov 2011 23:10:19 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
Fri, 11 Nov 2011 08:32:45 +0100 |
bulwahn |
adding CPS compilation to predicate compiler;
|
file |
diff |
annotate
|
Sun, 15 May 2011 18:59:27 +0200 |
wenzelm |
eliminated obsolete "assert" function, including divergent (unused!?) clone in Predicate_Compile_Proof;
|
file |
diff |
annotate
|
Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
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
|
Fri, 17 Dec 2010 13:45:43 +0100 |
wenzelm |
refer to regular structure Simplifier;
|
file |
diff |
annotate
|
Thu, 21 Oct 2010 19:13:09 +0200 |
bulwahn |
splitting large core file into core_data, mode_inference and predicate_compile_proof
|
file |
diff |
annotate
|