| Tue, 09 Jun 2015 22:48:11 +0100 |
paulson |
more tidying up of proofs
|
changeset |
files
|
| Mon, 08 Jun 2015 23:52:21 +0100 |
paulson |
tidying messy proofs
|
changeset |
files
|
| Mon, 08 Jun 2015 23:51:08 +0100 |
paulson |
tidying messy proofs
|
changeset |
files
|
| Mon, 08 Jun 2015 22:04:19 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 08 Jun 2015 22:04:15 +0200 |
wenzelm |
clarified context;
|
changeset |
files
|
| Mon, 08 Jun 2015 21:39:16 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 08 Jun 2015 21:23:28 +0200 |
wenzelm |
clarified abstracted term bindings;
|
changeset |
files
|
| Mon, 08 Jun 2015 20:58:43 +0200 |
wenzelm |
avoid duplicate warning due to Variable.warn_extra_tfrees;
|
changeset |
files
|
| Mon, 08 Jun 2015 20:53:42 +0200 |
wenzelm |
clarified Proof_Context.cert_propp/read_propp;
|
changeset |
files
|
| Mon, 08 Jun 2015 19:38:08 +0200 |
wenzelm |
more careful treatment of term bindings in 'obtain' proof body;
|
changeset |
files
|
| Mon, 08 Jun 2015 14:45:31 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Mon, 08 Jun 2015 18:56:04 +0100 |
paulson |
Merge
|
changeset |
files
|
| Mon, 08 Jun 2015 00:25:10 +0100 |
paulson |
Tidied lots of messy proofs
|
changeset |
files
|
| Sun, 07 Jun 2015 23:37:32 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sun, 07 Jun 2015 22:04:50 +0200 |
wenzelm |
tuned (see also 66e6c539a36d);
|
changeset |
files
|
| Sun, 07 Jun 2015 21:58:18 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sun, 07 Jun 2015 21:30:53 +0200 |
wenzelm |
clarified: declare props once and for all;
|
changeset |
files
|
| Sun, 07 Jun 2015 20:03:40 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sun, 07 Jun 2015 15:35:49 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sun, 07 Jun 2015 15:01:07 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sun, 07 Jun 2015 14:36:36 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 07 Jun 2015 12:55:42 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 07 Jun 2015 12:55:28 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 07 Jun 2015 12:43:06 +0200 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Sat, 06 Jun 2015 13:38:24 +0200 |
wenzelm |
more tight treatment of subgoals: main goal may refer to extra variables;
|
changeset |
files
|
| Fri, 05 Jun 2015 13:41:06 +0200 |
wenzelm |
added Isar command 'supply';
|
changeset |
files
|
| Fri, 05 Jun 2015 13:26:12 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 05 Jun 2015 11:11:26 +0200 |
wenzelm |
clarified signature -- better support for Isar commands outside of Pure;
|
changeset |
files
|
| Wed, 03 Jun 2015 21:48:40 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 03 Jun 2015 19:25:05 +0200 |
wenzelm |
clarified context;
|
changeset |
files
|
| Tue, 02 Jun 2015 23:00:50 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 02 Jun 2015 19:56:29 +0200 |
wenzelm |
clarified context;
|
changeset |
files
|
| Tue, 02 Jun 2015 17:27:01 +0200 |
wenzelm |
cleaified context;
|
changeset |
files
|
| Tue, 02 Jun 2015 13:55:43 +0200 |
wenzelm |
clarified context;
|
changeset |
files
|
| Tue, 02 Jun 2015 11:03:02 +0200 |
wenzelm |
clarified context;
|
changeset |
files
|
| Tue, 02 Jun 2015 10:12:46 +0200 |
wenzelm |
clarified context;
|
changeset |
files
|
| Tue, 02 Jun 2015 10:12:29 +0200 |
wenzelm |
clarified context;
|
changeset |
files
|
| Tue, 02 Jun 2015 09:40:04 +0200 |
wenzelm |
clarified context;
|
changeset |
files
|
| Tue, 02 Jun 2015 09:16:19 +0200 |
wenzelm |
clarified context;
|
changeset |
files
|
| Tue, 02 Jun 2015 09:10:05 +0200 |
wenzelm |
tuned proof;
|
changeset |
files
|
| Wed, 03 Jun 2015 09:32:49 +0200 |
noschinl |
merged
|
changeset |
files
|
| Tue, 02 Jun 2015 13:14:36 +0200 |
noschinl |
simps_of_case: Better error if split rule is not an equality
|
changeset |
files
|
| Tue, 02 Jun 2015 13:14:11 +0200 |
noschinl |
simps_of_case: allow Drule.dummy_thm as ignored split rule
|
changeset |
files
|
| Mon, 01 Jun 2015 18:59:22 +0200 |
haftmann |
implicit partial divison operation in integral domains
|
changeset |
files
|
| Mon, 01 Jun 2015 18:59:21 +0200 |
haftmann |
separate class for division operator, with particular syntax added in more specific classes
|
changeset |
files
|
| Mon, 01 Jun 2015 18:59:21 +0200 |
haftmann |
explicit check for field sort, to anticipate situation where syntactic checking alone will not be sufficient any longer
|
changeset |
files
|
| Mon, 01 Jun 2015 18:59:21 +0200 |
haftmann |
dropped dead config option
|
changeset |
files
|
| Mon, 01 Jun 2015 18:59:20 +0200 |
haftmann |
tuned, including proper signature for functor argument
|
changeset |
files
|
| Mon, 01 Jun 2015 18:59:20 +0200 |
haftmann |
dropped dead code
|
changeset |
files
|
| Mon, 01 Jun 2015 18:59:20 +0200 |
haftmann |
explicit argument expansion of uncheck rules;
|
changeset |
files
|
| Mon, 01 Jun 2015 18:59:20 +0200 |
haftmann |
explicit input marker for operations
|
changeset |
files
|
| Mon, 01 Jun 2015 18:59:20 +0200 |
haftmann |
completely separated canonical class abbreviations from abbreviations stemming from non-canonical morphisms -- these have no shared concept
|
changeset |
files
|
| Mon, 01 Jun 2015 18:59:20 +0200 |
haftmann |
self-contained formulation of abbrev for named targets
|
changeset |
files
|
| Mon, 01 Jun 2015 18:59:20 +0200 |
haftmann |
correct sort constraints for abbreviations in type classes
|
changeset |
files
|
| Mon, 01 Jun 2015 18:59:20 +0200 |
haftmann |
separate function to compute exported abbreviation
|
changeset |
files
|
| Mon, 01 Jun 2015 18:59:20 +0200 |
haftmann |
clearly separated target primitives (target_foo) from self-contained target operations (foo)
|
changeset |
files
|
| Mon, 01 Jun 2015 18:59:20 +0200 |
haftmann |
tuned order
|
changeset |
files
|
| Mon, 01 Jun 2015 18:59:20 +0200 |
haftmann |
dedicated config options to deactivate uncheck phase for improvable syntax
|
changeset |
files
|
| Mon, 01 Jun 2015 18:59:19 +0200 |
haftmann |
clarified interfaces for improvable syntax
|
changeset |
files
|
| Mon, 01 Jun 2015 18:59:19 +0200 |
haftmann |
tuned
|
changeset |
files
|