| 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
|
| Mon, 26 Dec 2011 18:32:43 +0100 |
haftmann |
moved various set operations to theory Set (resp. Product_Type)
|
file |
diff |
annotate
|
| Wed, 30 Nov 2011 18:07:14 +0100 |
wenzelm |
prefer typedef without alternative name;
|
file |
diff |
annotate
|
| Wed, 30 Nov 2011 16:27:10 +0100 |
wenzelm |
prefer typedef without extra definition and alternative name;
|
file |
diff |
annotate
|
| Mon, 28 Nov 2011 11:22:36 +0100 |
nipkow |
Hide Product_Type.Times - too precious an identifier
|
file |
diff |
annotate
|
| Sun, 20 Nov 2011 21:07:10 +0100 |
wenzelm |
eliminated obsolete "standard";
|
file |
diff |
annotate
|
| Wed, 19 Oct 2011 17:45:25 +0200 |
huffman |
merged
|
file |
diff |
annotate
|
| Tue, 18 Oct 2011 15:19:06 +0200 |
huffman |
hide typedef-generated constants Product_Type.prod and Sum_Type.sum
|
file |
diff |
annotate
|
| Wed, 19 Oct 2011 08:37:22 +0200 |
bulwahn |
removing old code generator setup of inductive predicates
|
file |
diff |
annotate
|
| Wed, 19 Oct 2011 08:37:21 +0200 |
bulwahn |
removing old code generator setup for product types
|
file |
diff |
annotate
|
| Tue, 13 Sep 2011 17:07:33 -0700 |
huffman |
tuned proofs
|
file |
diff |
annotate
|
| Mon, 08 Aug 2011 10:32:55 -0700 |
huffman |
rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
|
file |
diff |
annotate
|
| Sun, 17 Jul 2011 19:48:02 +0200 |
haftmann |
moving UNIV = ... equations to their proper theories
|
file |
diff |
annotate
|
| Sat, 02 Jul 2011 22:55:58 +0200 |
haftmann |
install case certificate for If after code_datatype declaration for bool
|
file |
diff |
annotate
|
| Wed, 29 Jun 2011 18:12:34 +0200 |
wenzelm |
modernized some simproc setup;
|
file |
diff |
annotate
|
| Wed, 29 Jun 2011 17:35:46 +0200 |
wenzelm |
modernized some simproc setup;
|
file |
diff |
annotate
|
| Tue, 19 Apr 2011 23:57:28 +0200 |
wenzelm |
eliminated Codegen.mode in favour of explicit argument;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 13:31:16 +0200 |
wenzelm |
explicit structure Syntax_Trans;
|
file |
diff |
annotate
|
| Wed, 06 Apr 2011 13:33:46 +0200 |
wenzelm |
typed_print_translation: discontinued show_sorts argument;
|
file |
diff |
annotate
|
| Thu, 24 Mar 2011 16:56:19 +0100 |
wenzelm |
added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
|
file |
diff |
annotate
|
| Tue, 22 Mar 2011 12:49:07 +0100 |
nipkow |
fixed a printing problem for bounded quantifiers and bounded set operators in the case of tuples
|
file |
diff |
annotate
|
| Mon, 21 Feb 2011 10:44:19 +0100 |
blanchet |
renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
|
file |
diff |
annotate
|
| Tue, 11 Jan 2011 14:12:37 +0100 |
haftmann |
"enriched_type" replaces less specific "type_lifting"
|
file |
diff |
annotate
|
| Tue, 21 Dec 2010 17:52:23 +0100 |
haftmann |
tuned type_lifting declarations
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 17:43:54 +0100 |
wenzelm |
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 09:19:10 +0100 |
haftmann |
replace `type_mapper` by the more adequate `type_lifting`
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 10:03:13 +0100 |
huffman |
theorem names generated by the (rep_)datatype command now have mandatory qualifiers
|
file |
diff |
annotate
|
| Mon, 22 Nov 2010 10:34:33 +0100 |
hoelzl |
Replace surj by abbreviation; remove surj_on.
|
file |
diff |
annotate
|
| Thu, 18 Nov 2010 17:01:16 +0100 |
haftmann |
map_pair replaces prod_fun
|
file |
diff |
annotate
|
| Tue, 16 Nov 2010 16:36:57 -0800 |
huffman |
typedef (open) unit
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 11:13:15 +0200 |
nipkow |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file |
diff |
annotate
|
| Fri, 10 Sep 2010 10:21:25 +0200 |
haftmann |
Haskell == is infix, not infixl
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 10:05:19 +0200 |
nipkow |
expand_fun_eq -> ext_iff
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 19:34:23 +0200 |
haftmann |
renamed class/constant eq to equal; tuned some instantiations
|
file |
diff |
annotate
|