| Sun, 15 Dec 2013 18:54:26 +0100 |
blanchet |
tuning
|
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
|
| Tue, 19 Nov 2013 18:11:52 +0100 |
blanchet |
simplified old code
|
file |
diff |
annotate
|
| Wed, 29 May 2013 18:55:37 +0200 |
wenzelm |
resolve_inc_tyvars: back to old behavior before 0fa3b456a267 where types of equal Vars are *not* unified -- recover last example in src/HOL/Metis_Examples/Clausification.thy;
|
file |
diff |
annotate
|
| Wed, 29 May 2013 18:25:11 +0200 |
wenzelm |
tuned signature -- more explicit flags for low-level Thm.bicompose;
|
file |
diff |
annotate
|
| Mon, 27 May 2013 15:57:38 +0200 |
wenzelm |
instantiate types as well (see also Thm.first_order_match);
|
file |
diff |
annotate
|
| Thu, 16 May 2013 13:34:13 +0200 |
blanchet |
tuning -- renamed '_from_' to '_of_' in Sledgehammer
|
file |
diff |
annotate
|
| Wed, 15 May 2013 17:43:42 +0200 |
blanchet |
renamed Sledgehammer functions with 'for' in their names to 'of'
|
file |
diff |
annotate
|
| Sun, 12 May 2013 20:46:17 +0200 |
wenzelm |
more standard Isabelle/ML operations -- avoid inaccurate Bool.fromString;
|
file |
diff |
annotate
|
| Sat, 11 May 2013 16:13:08 +0200 |
wenzelm |
avoid PolyML.makestring, even in dead code;
|
file |
diff |
annotate
|
| Fri, 12 Apr 2013 15:30:38 +0200 |
wenzelm |
tuned exceptions -- avoid composing error messages in low-level situations;
|
file |
diff |
annotate
|
| Mon, 14 Jan 2013 09:59:50 +0100 |
blanchet |
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
|
file |
diff |
annotate
|
| Tue, 26 Jun 2012 11:14:39 +0200 |
blanchet |
added type arguments to "ATerm" constructor -- but don't use them yet
|
file |
diff |
annotate
|
| Mon, 27 Feb 2012 15:48:02 +0100 |
wenzelm |
prefer cut_tac, where it is clear that the special variants cut_rules_tac or cut_facts_tac are not required;
|
file |
diff |
annotate
|
| Thu, 02 Feb 2012 01:20:28 +0100 |
blanchet |
implemented partial application aliases (for SPASS mainly)
|
file |
diff |
annotate
|
| Mon, 23 Jan 2012 17:40:32 +0100 |
blanchet |
renamed two files to make room for a new file
|
file |
diff |
annotate
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
wrap lambdas earlier, to get more control over beta/eta
|
file |
diff |
annotate
|
| Tue, 15 Nov 2011 22:13:39 +0100 |
blanchet |
continued implementation of lambda-lifting in Metis
|
file |
diff |
annotate
|
| Tue, 15 Nov 2011 22:13:39 +0100 |
blanchet |
started implementing lambda-lifting in Metis
|
file |
diff |
annotate
|
| Thu, 25 Aug 2011 14:25:07 +0200 |
blanchet |
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
|
file |
diff |
annotate
|
| Wed, 17 Aug 2011 18:05:31 +0200 |
wenzelm |
modernized signature of Term.absfree/absdummy;
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 20:53:43 +0200 |
wenzelm |
old term operations are legacy;
|
file |
diff |
annotate
|
| Fri, 10 Jun 2011 17:52:09 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 23:12:02 +0200 |
wenzelm |
renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 20:56:08 +0200 |
wenzelm |
clarified special incr_type_indexes;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 00:16:28 +0200 |
blanchet |
removed needless function that duplicated standard functionality, with a little unnecessary twist
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 00:16:28 +0200 |
blanchet |
removed more dead code
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 00:16:28 +0200 |
blanchet |
renamed "untyped_aconv" to distinguish it clearly from the standard "aconv_untyped"
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 22:13:49 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 16:20:18 +0200 |
blanchet |
restore comment about subtle issue
|
file |
diff |
annotate
|