| 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
|
| Sat, 25 May 2013 15:37:53 +0200 |
wenzelm |
syntax translations always depend on context;
|
file |
diff |
annotate
|
| Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| Fri, 12 Apr 2013 17:21:51 +0200 |
wenzelm |
modifiers for classical wrappers operate on Proof.context instead of claset;
|
file |
diff |
annotate
|
| Tue, 12 Mar 2013 07:51:10 +0100 |
nipkow |
extended set comprehension notation with {pttrn : A . P}
|
file |
diff |
annotate
|
| Sun, 17 Feb 2013 21:29:30 +0100 |
haftmann |
Sieve of Eratosthenes
|
file |
diff |
annotate
|
| Sat, 17 Nov 2012 17:55:52 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 16 Nov 2012 18:45:57 +0100 |
hoelzl |
move theorems to be more generally useable
|
file |
diff |
annotate
|
| Wed, 17 Oct 2012 14:13:57 +0200 |
bulwahn |
moving Pair_inject from legacy and duplicate section to general section, as Pair_inject was considered a duplicate in e8400e31528a by mistake (cf. communication on dev mailing list)
|
file |
diff |
annotate
|
| Fri, 12 Oct 2012 18:58:20 +0200 |
wenzelm |
discontinued obsolete typedef (open) syntax;
|
file |
diff |
annotate
|
| Wed, 10 Oct 2012 10:47:43 +0200 |
bulwahn |
moving simproc from Finite_Set to more appropriate Product_Type theory
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 22:55:41 +0200 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
| Thu, 24 May 2012 17:25:53 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Wed, 25 Apr 2012 00:57:41 +0200 |
blanchet |
added "no_atp"s for extremely prolific, useless facts for ATPs
|
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, 23 Feb 2012 20:15:59 +0100 |
haftmann |
tuned whitespace
|
file |
diff |
annotate
|
| Tue, 21 Feb 2012 08:15:42 +0100 |
haftmann |
reverting changesets from 5d33a3269029 on: change of order of declaration of classical rules makes serious problems
|
file |
diff |
annotate
|
| Mon, 20 Feb 2012 21:04:00 +0100 |
haftmann |
tuned whitespace
|
file |
diff |
annotate
|
| Sun, 01 Jan 2012 15:44:15 +0100 |
haftmann |
interaction of set operations for execution and membership predicate
|
file |
diff |
annotate
|
| Thu, 29 Dec 2011 10:47:55 +0100 |
haftmann |
attribute code_abbrev superseedes code_unfold_post
|
file |
diff |
annotate
|