| Sat, 17 Dec 2016 15:22:00 +0100 |
haftmann |
dropped comment after conversation with author: predicate compiler works independently from any code generator setup
|
file |
diff |
annotate
|
| Thu, 10 Mar 2016 12:33:04 +0100 |
haftmann |
clarified: constructors in the sense of the code generator are not invertible;
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 20:37:59 +0200 |
wenzelm |
moved remaining display.ML to more_thm.ML;
|
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
|
| Fri, 21 Mar 2014 10:45:03 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 13:33:05 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Mon, 10 Feb 2014 14:33:47 +0100 |
wenzelm |
comments;
|
file |
diff |
annotate
|
| Mon, 04 Nov 2013 17:25:36 +0100 |
blanchet |
careful with lists of different lengths
|
file |
diff |
annotate
|
| Thu, 31 Oct 2013 16:54:22 +0100 |
blanchet |
generate stable names for axioms
|
file |
diff |
annotate
|
| Fri, 24 May 2013 17:00:46 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 28 Feb 2013 18:35:31 +0100 |
wenzelm |
provide explicit dummy names (cf. dfe469293eb4);
|
file |
diff |
annotate
|
| Mon, 12 Nov 2012 23:24:40 +0100 |
haftmann |
dropped dead code
|
file |
diff |
annotate
|
| Wed, 12 Sep 2012 13:56:49 +0200 |
wenzelm |
standardized ML aliases;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2012 21:16:15 +0100 |
wenzelm |
discontinued old-style Term.list_abs in favour of plain Term.abs;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 17:51:49 +0200 |
wenzelm |
simplified Name.variant -- discontinued builtin fold_map;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 16:34:49 +0200 |
wenzelm |
discontinued Name.variant to emphasize that this is old-style / indirect;
|
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
|
| Wed, 01 Dec 2010 15:02:39 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 21 Oct 2010 19:13:10 +0200 |
bulwahn |
using a signature in core_data and moving some more functions to core_data
|
file |
diff |
annotate
|
| Thu, 30 Sep 2010 15:37:11 +0200 |
bulwahn |
applying case beta reduction to case term before matching in predicate compile function flattening; moving case beta reduction function to Predicate_Compile_Aux
|
file |
diff |
annotate
|
| Thu, 30 Sep 2010 10:48:09 +0200 |
bulwahn |
removing dead code
|
file |
diff |
annotate
|
| Wed, 29 Sep 2010 11:55:08 +0200 |
bulwahn |
removing obsolete distinction between prod_case and other case expressions after merging of split and prod_case (d3daea901123) in predicate compiler
|
file |
diff |
annotate
|
| Tue, 31 Aug 2010 10:51:03 +0200 |
bulwahn |
renaming
|
file |
diff |
annotate
|
| Tue, 31 Aug 2010 08:00:56 +0200 |
bulwahn |
changing order of premises generated when flattening functions in premises; adapting example for second attack for hotel key card system
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 16:56:45 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 19 Aug 2010 12:11:57 +0200 |
haftmann |
use HOLogic.boolT and @{typ bool} more pervasively
|
file |
diff |
annotate
|
| Mon, 28 Jun 2010 15:03:07 +0200 |
haftmann |
merged constants "split" and "prod_case"
|
file |
diff |
annotate
|
| Wed, 26 May 2010 16:05:25 +0200 |
haftmann |
normalized references to constant "split"
|
file |
diff |
annotate
|