| Mon, 28 Dec 2015 21:47:32 +0100 |
wenzelm |
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 22:58:50 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Sun, 12 Apr 2015 11:33:19 +0200 |
hoelzl |
move filters to their own theory
|
file |
diff |
annotate
|
| Fri, 07 Nov 2014 11:28:37 +0100 |
traytel |
more complete fp_sugars for sum and prod;
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Thu, 23 Oct 2014 19:40:39 +0200 |
haftmann |
further downshift of theory Parity in the hierarchy
|
file |
diff |
annotate
|
| Thu, 23 Oct 2014 14:04:05 +0200 |
haftmann |
downshift of theory Parity in the hierarchy
|
file |
diff |
annotate
|
| Tue, 07 Oct 2014 23:29:43 +0200 |
wenzelm |
more bibtex entries;
|
file |
diff |
annotate
|
| Thu, 18 Sep 2014 16:47:40 +0200 |
blanchet |
moved old 'size' generator together with 'old_datatype'
|
file |
diff |
annotate
|
| Thu, 18 Sep 2014 16:47:40 +0200 |
blanchet |
moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer)
|
file |
diff |
annotate
|
| Tue, 16 Sep 2014 19:23:37 +0200 |
blanchet |
tuned fact visibility
|
file |
diff |
annotate
|
| Tue, 16 Sep 2014 19:23:37 +0200 |
blanchet |
register 'prod' and 'sum' as datatypes, to allow N2M through them
|
file |
diff |
annotate
|
| Wed, 03 Sep 2014 00:06:26 +0200 |
blanchet |
tuned imports
|
file |
diff |
annotate
|
| Wed, 03 Sep 2014 00:06:24 +0200 |
blanchet |
use 'datatype_new' in 'Main'
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 16:34:40 +0200 |
blanchet |
renamed BNF theories
|
file |
diff |
annotate
|
| Thu, 28 Aug 2014 00:40:37 +0200 |
blanchet |
moved old 'smt' method out of 'Main'
|
file |
diff |
annotate
|
| Thu, 24 Jul 2014 11:54:15 +0200 |
wenzelm |
more robust notation BNF_Def.convol, which is private to main HOL, but may cause syntax ambiguities nonetheless (e.g. List.thy);
|
file |
diff |
annotate
|
| Wed, 11 Jun 2014 11:28:46 +0200 |
blanchet |
removed old SMT module from Sledgehammer
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 08:13:23 +0100 |
traytel |
simplified internal datatype construction
|
file |
diff |
annotate
|
| Tue, 11 Mar 2014 17:18:41 +0100 |
blanchet |
moved 'Quickcheck_Narrowing' further down the theory graph
|
file |
diff |
annotate
|
| Wed, 19 Feb 2014 10:30:21 +0100 |
traytel |
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
|
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
|
| Thu, 23 Jan 2014 19:02:22 +0100 |
blanchet |
hide 'csum' etc.
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 22:24:48 +0100 |
blanchet |
renamed 'regular' to 'regularCard' to avoid clashes (e.g. in Meson_Test)
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 21:45:08 +0100 |
blanchet |
hide BNF notation
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 19:05:25 +0100 |
blanchet |
removed dependency of BNF package on Nitpick
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 18:59:53 +0100 |
blanchet |
deactivate one more cardinal notation
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 18:24:56 +0100 |
blanchet |
moved hide_const from BNF to Main
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 18:24:56 +0100 |
blanchet |
tuned names
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 18:24:56 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|