| Tue, 06 Oct 2015 15:14:28 +0200 |
wenzelm |
fewer aliases for toplevel theorem statements;
|
file |
diff |
annotate
|
| Tue, 01 Sep 2015 22:32:58 +0200 |
wenzelm |
eliminated \<Colon>;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 22:58:50 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Fri, 03 Jul 2015 08:26:34 +0200 |
hoelzl |
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
|
file |
diff |
annotate
|
| Mon, 04 May 2015 18:49:51 +0200 |
hoelzl |
strengthened lfp_ordinal_induct; added dual gfp variant
|
file |
diff |
annotate
|
| Mon, 04 May 2015 18:04:01 +0200 |
hoelzl |
add rules for least/greatest fixed point calculus
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Wed, 29 Oct 2014 11:41:54 +0100 |
wenzelm |
modernized setup;
|
file |
diff |
annotate
|
| Thu, 11 Sep 2014 18:54:36 +0200 |
blanchet |
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
|
file |
diff |
annotate
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
fixed infinite loops in 'register' functions + more uniform API
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 16:17:46 +0200 |
blanchet |
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
|
file |
diff |
annotate
|
| Fri, 14 Mar 2014 15:41:29 +0100 |
wenzelm |
discontinued somewhat pointless "thy_script" keyword kind;
|
file |
diff |
annotate
|
| Thu, 20 Feb 2014 15:14:37 +0100 |
noschinl |
less flex-flex pairs
|
file |
diff |
annotate
|
| Wed, 19 Feb 2014 08:34:33 +0100 |
blanchet |
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
|
file |
diff |
annotate
|
| Mon, 17 Feb 2014 13:31:42 +0100 |
blanchet |
renamed old 'primrec' to 'old_primrec' (until the new 'primrec' can be moved above 'Nat' in the theory dependencies)
|
file |
diff |
annotate
|