| Thu, 22 Dec 2016 08:43:30 +0100 |
haftmann |
proper logical constants
|
file |
diff |
annotate
|
| Fri, 29 Jul 2016 09:49:23 +0200 |
Andreas Lochbihler |
add lemmas contributed by Peter Gammie
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 16:25:08 +0100 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
| Sun, 13 Dec 2015 21:56:15 +0100 |
wenzelm |
more general types Proof.method / context_tactic;
|
file |
diff |
annotate
|
| Mon, 09 Nov 2015 15:48:17 +0100 |
wenzelm |
qualifier is mandatory by default;
|
file |
diff |
annotate
|
| Wed, 04 Nov 2015 08:13:52 +0100 |
ballarin |
Keyword 'rewrites' identifies rewrite morphisms.
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 22:58:50 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Tue, 14 Apr 2015 13:57:25 +0200 |
Andreas Lochbihler |
move lemma from AFP/Coinductive
|
file |
diff |
annotate
|
| Sat, 07 Mar 2015 21:32:31 +0100 |
wenzelm |
clarified Drule.gen_all: observe context more carefully;
|
file |
diff |
annotate
|
| Wed, 11 Feb 2015 14:03:05 +0100 |
Andreas Lochbihler |
add lemmas about flat_ord
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Sat, 16 Aug 2014 19:20:11 +0200 |
wenzelm |
updated to named_theorems;
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 21:32:41 +0100 |
blanchet |
moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
|
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
|
| Fri, 27 Sep 2013 12:26:23 +0200 |
Andreas Lochbihler |
generalise lemma
|
file |
diff |
annotate
|
| Mon, 02 Sep 2013 16:28:11 +0200 |
Andreas Lochbihler |
move admissible out of class ccpo to avoid unnecessary class predicate in foundational theorems
|
file |
diff |
annotate
|
| Wed, 24 Jul 2013 17:15:59 +0200 |
krauss |
derive specialized version of full fixpoint induction (with admissibility)
|
file |
diff |
annotate
|
| Fri, 22 Mar 2013 00:39:16 +0100 |
krauss |
added rudimentary induction rule for partial_function (heap)
|
file |
diff |
annotate
|
| Tue, 19 Mar 2013 13:19:21 +0100 |
Andreas Lochbihler |
add induction rule for partial_function (tailrec)
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 22:55:41 +0200 |
wenzelm |
prefer ML_file over old uses;
|
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
|
| Thu, 29 Dec 2011 18:54:07 +0100 |
huffman |
remove constant 'ccpo.lub', re-use constant 'Sup' instead
|
file |
diff |
annotate
|
| Sat, 29 Oct 2011 12:55:34 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 31 May 2011 11:16:34 +0200 |
krauss |
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
|
file |
diff |
annotate
|
| Tue, 31 May 2011 11:11:17 +0200 |
krauss |
admissibility on option type
|
file |
diff |
annotate
|
| Mon, 23 May 2011 21:34:37 +0200 |
krauss |
also manage induction rule;
|
file |
diff |
annotate
|
| Mon, 23 May 2011 10:58:21 +0200 |
krauss |
separate initializations for different modes of partial_function -- generation of induction rules will be non-uniform
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 21:41:14 +0200 |
krauss |
added rule let_mono
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 11:04:41 +0200 |
krauss |
hide_const various constants, in particular to avoid ugly qualifiers in HOLCF
|
file |
diff |
annotate
|
| Sat, 23 Oct 2010 23:41:19 +0200 |
krauss |
first version of partial_function package
|
file |
diff |
annotate
|