| Tue, 12 Nov 2013 14:24:34 +0100 |
blanchet |
ported part of function package to new 'Ctr_Sugar' abstraction
|
file |
diff |
annotate
|
| Sun, 08 Sep 2013 22:32:47 +0200 |
Manuel Eberl |
generate elim rules for elimination of function equalities;
|
file |
diff |
annotate
|
| Wed, 31 Oct 2012 11:23:21 +0100 |
blanchet |
moved "SAT" before "FunDef" and moved back all SAT-related ML files to where they belong
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 22:55:41 +0200 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
| Mon, 23 Apr 2012 21:44:36 +0200 |
wenzelm |
more standard method setup;
|
file |
diff |
annotate
|
| Thu, 12 Apr 2012 18:39:19 +0200 |
wenzelm |
more standard method setup;
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 22:08:53 +0100 |
wenzelm |
declare command keywords via theory header, including strict checking outside Pure;
|
file |
diff |
annotate
|
| Sat, 18 Feb 2012 09:46:58 +0100 |
krauss |
added congruence rules for Option.{map|bind}
|
file |
diff |
annotate
|
| Sat, 23 Oct 2010 23:42:04 +0200 |
krauss |
integrated partial_function into HOL-Plain
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 10:48:37 +0200 |
haftmann |
dropped superfluous [code del]s
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 11:52:04 +0200 |
krauss |
default termination prover as plain tactic
|
file |
diff |
annotate
|
| Sat, 02 Jan 2010 23:18:58 +0100 |
krauss |
absorb structures Decompose and Descent into Termination, to simplify further restructuring
|
file |
diff |
annotate
|
| Fri, 06 Nov 2009 14:42:42 +0100 |
krauss |
renamed method induct_scheme to induction_schema
|
file |
diff |
annotate
|
| Fri, 30 Oct 2009 01:32:06 +0100 |
krauss |
absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
|
file |
diff |
annotate
|
| Fri, 23 Oct 2009 16:37:56 +0200 |
krauss |
renamed auto_term.ML -> relation.ML
|
file |
diff |
annotate
|