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
|
Sun, 27 Dec 2015 22:07:17 +0100 |
wenzelm |
discontinued ASCII replacement syntax <*>;
|
file |
diff |
annotate
|
Mon, 07 Dec 2015 10:38:04 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
Wed, 11 Nov 2015 09:48:24 +0100 |
Andreas Lochbihler |
add various lemmas
|
file |
diff |
annotate
|
Tue, 13 Oct 2015 09:21:21 +0200 |
haftmann |
restored print translation from a1141fb798ff, to prevent a printing misfit observable using "thm divmod_nat_if" in theory "Divides", with a meagure indication in the comment
|
file |
diff |
annotate
|
Tue, 13 Oct 2015 09:21:15 +0200 |
haftmann |
prod_case as canonical name for product type eliminator
|
file |
diff |
annotate
|
Tue, 13 Oct 2015 09:21:14 +0200 |
haftmann |
moved lemmas
|
file |
diff |
annotate
|
Fri, 09 Oct 2015 20:26:03 +0200 |
wenzelm |
discontinued specific HTML syntax;
|
file |
diff |
annotate
|
Tue, 22 Sep 2015 11:48:22 +0200 |
haftmann |
effective revert of e6b1236f9b3d: spontaneous eta-contraction happens on the print translation level and can only be suppressed on the print translation level
|
file |
diff |
annotate
|
Wed, 09 Sep 2015 20:57:21 +0200 |
wenzelm |
simplified simproc programming interfaces;
|
file |
diff |
annotate
|
Sun, 06 Sep 2015 22:14:51 +0200 |
haftmann |
tuned notation, proofs, namespace
|
file |
diff |
annotate
|
Sun, 06 Sep 2015 22:14:51 +0200 |
haftmann |
obsolete: if case_prod is fully applied, it is printed as proper case expression;
|
file |
diff |
annotate
|
Sun, 06 Sep 2015 22:14:51 +0200 |
haftmann |
prefer "uncurry" as canonical name for case distinction on products in combinatorial view
|
file |
diff |
annotate
|
Sun, 06 Sep 2015 22:14:51 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
Sun, 06 Sep 2015 22:14:39 +0200 |
haftmann |
obsolete: all (formally unchecked) examples given in the comments work out of the box as advertised
|
file |
diff |
annotate
|
Sun, 06 Sep 2015 22:14:37 +0200 |
haftmann |
dropped whitespace leftover from b57df8eecad6
|
file |
diff |
annotate
|
Tue, 01 Sep 2015 22:32:58 +0200 |
wenzelm |
eliminated \<Colon>;
|
file |
diff |
annotate
|
Thu, 27 Aug 2015 21:19:48 +0200 |
haftmann |
standardized some occurences of ancient "split" alias
|
file |
diff |
annotate
|
Sat, 18 Jul 2015 22:58:50 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
Tue, 14 Apr 2015 11:32:01 +0200 |
Andreas Lochbihler |
add lemmas
|
file |
diff |
annotate
|
Tue, 31 Mar 2015 17:34:52 +0200 |
wenzelm |
clarified role of naming for background theory: transform_binding (e.g. for "concealed" flag) uses naming of hypothetical context;
|
file |
diff |
annotate
|
Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
Tue, 10 Feb 2015 14:48:26 +0100 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
file |
diff |
annotate
|
Thu, 13 Nov 2014 17:19:52 +0100 |
hoelzl |
import general theorems from AFP/Markov_Models
|
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, 30 Oct 2014 22:45:19 +0100 |
wenzelm |
eliminated aliases;
|
file |
diff |
annotate
|
Wed, 29 Oct 2014 19:01:49 +0100 |
wenzelm |
modernized setup;
|
file |
diff |
annotate
|
Wed, 29 Oct 2014 14:40:14 +0100 |
wenzelm |
modernized setup;
|
file |
diff |
annotate
|
Mon, 29 Sep 2014 08:13:23 +0200 |
haftmann |
corrected white-space accident
|
file |
diff |
annotate
|
Sun, 28 Sep 2014 20:27:47 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
Fri, 19 Sep 2014 13:27:04 +0200 |
blanchet |
made new 'primrec' bootstrapping-capable
|
file |
diff |
annotate
|
Thu, 11 Sep 2014 18:54:36 +0200 |
blanchet |
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
|
file |
diff |
annotate
|
Wed, 10 Sep 2014 14:57:03 +0200 |
haftmann |
dropped ineffective print_translation which has never been adjusted to check/uncheck-style case patterns
|
file |
diff |
annotate
|
Sat, 06 Sep 2014 20:12:32 +0200 |
haftmann |
added various facts
|
file |
diff |
annotate
|
Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
added 'plugins' option to control which hooks are enabled
|
file |
diff |
annotate
|
Mon, 18 Aug 2014 17:19:58 +0200 |
blanchet |
reordered some (co)datatype property names for more consistency
|
file |
diff |
annotate
|
Thu, 12 Jun 2014 08:48:59 +0200 |
haftmann |
uniform treatment of trivial unit instances: simplify by default, unfold in code preprocessor
|
file |
diff |
annotate
|
Tue, 10 Jun 2014 18:24:53 +0200 |
Andreas Lochbihler |
add type class instances for unit
|
file |
diff |
annotate
|
Mon, 26 May 2014 16:32:55 +0200 |
blanchet |
got rid of '=:' squiggly
|
file |
diff |
annotate
|
Tue, 20 May 2014 16:00:00 +0200 |
nipkow |
added unit :: linorder
|
file |
diff |
annotate
|
Mon, 21 Apr 2014 21:16:05 +0200 |
haftmann |
swap with qualifier;
|
file |
diff |
annotate
|
Sat, 12 Apr 2014 11:27:36 +0200 |
haftmann |
more operations and lemmas
|
file |
diff |
annotate
|
Thu, 10 Apr 2014 12:48:01 +0200 |
wenzelm |
modernized simproc_setup;
|
file |
diff |
annotate
|
Fri, 21 Mar 2014 20:33:56 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
Wed, 19 Mar 2014 18:47:22 +0100 |
haftmann |
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
|
file |
diff |
annotate
|
Thu, 13 Mar 2014 08:56:08 +0100 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
Thu, 06 Mar 2014 13:36:48 +0100 |
blanchet |
renamed 'map_pair' to 'map_prod'
|
file |
diff |
annotate
|
Fri, 21 Feb 2014 00:09:56 +0100 |
blanchet |
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
|
file |
diff |
annotate
|
Fri, 14 Feb 2014 07:53:46 +0100 |
blanchet |
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
|
file |
diff |
annotate
|
Fri, 14 Feb 2014 07:53:46 +0100 |
blanchet |
renamed 'wrap_free_constructors' to 'free_constructors' (cf. 'functor', 'bnf', etc.)
|
file |
diff |
annotate
|
Fri, 14 Feb 2014 07:53:46 +0100 |
blanchet |
renamed 'enriched_type' to more informative 'functor' (following the renaming of enriched type constructors to bounded natural functors)
|
file |
diff |
annotate
|
Wed, 12 Feb 2014 17:35:59 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
Wed, 12 Feb 2014 08:37:06 +0100 |
blanchet |
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
|
file |
diff |
annotate
|
Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
renamed '{prod,sum,bool,unit}_case' to 'case_...'
|
file |
diff |
annotate
|
Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
avoid duplicate 'case' definitions by first looking up 'Ctr_Sugar'
|
file |
diff |
annotate
|
Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
|
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, 18 Oct 2013 10:43:20 +0200 |
blanchet |
killed most "no_atp", to make Sledgehammer more complete
|
file |
diff |
annotate
|
Sun, 23 Jun 2013 21:16:07 +0200 |
haftmann |
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
|
file |
diff |
annotate
|