| Sun, 21 Aug 2011 22:13:04 +0200 |
krauss |
removed session HOL/Subst -- now subsumed my more modern HOL/ex/Unification.thy
|
changeset |
files
|
| Sun, 21 Aug 2011 22:13:04 +0200 |
krauss |
removed technical or trivial unused facts
|
changeset |
files
|
| Sun, 21 Aug 2011 22:13:04 +0200 |
krauss |
more precise authors and comments;
|
changeset |
files
|
| Sun, 21 Aug 2011 22:13:04 +0200 |
krauss |
added proof of idempotence, roughly after HOL/Subst/Unify.thy
|
changeset |
files
|
| Sun, 21 Aug 2011 22:13:04 +0200 |
krauss |
tuned proofs, sledgehammering overly verbose parts
|
changeset |
files
|
| Sun, 21 Aug 2011 22:13:04 +0200 |
krauss |
tuned notation
|
changeset |
files
|
| Sun, 21 Aug 2011 22:13:04 +0200 |
krauss |
ported some lemmas from HOL/Subst/*;
|
changeset |
files
|
| Sun, 21 Aug 2011 22:13:04 +0200 |
krauss |
changed constant names and notation to match HOL/Subst/*.thy, from which this theory is a clone.
|
changeset |
files
|
| Sun, 21 Aug 2011 21:18:59 -0700 |
huffman |
merged
|
changeset |
files
|
| Sun, 21 Aug 2011 12:22:31 -0700 |
huffman |
add lemmas interior_Times and closure_Times
|
changeset |
files
|
| Sun, 21 Aug 2011 22:56:55 +0200 |
haftmann |
avoid pred/set mixture
|
changeset |
files
|
| Sun, 21 Aug 2011 19:47:52 +0200 |
haftmann |
avoid pred/set mixture
|
changeset |
files
|
| Sun, 21 Aug 2011 22:04:01 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sun, 21 Aug 2011 11:03:15 -0700 |
huffman |
remove unnecessary euclidean_space class constraints
|
changeset |
files
|
| Sun, 21 Aug 2011 09:46:20 -0700 |
huffman |
section -> subsection
|
changeset |
files
|