| Fri, 27 Nov 2009 16:26:23 +0100 |
Removed eq_to_mono2, added not_mono.
|
file | diff | annotate |
| Mon, 09 Nov 2009 15:50:15 +0000 |
New theory Probability/Borel.thy, and some associated lemmas
|
file | diff | annotate |
| Wed, 21 Oct 2009 11:19:11 +0100 |
merged
|
file | diff | annotate |
| Tue, 20 Oct 2009 16:32:51 +0100 |
Some new lemmas concerning sets
|
file | diff | annotate |
| Wed, 21 Oct 2009 08:16:25 +0200 |
merged
|
file | diff | annotate |
| Wed, 21 Oct 2009 08:14:38 +0200 |
dropped redundant gen_ prefix
|
file | diff | annotate |
| Tue, 20 Oct 2009 16:13:01 +0200 |
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
|
file | diff | annotate |
| Tue, 20 Oct 2009 15:02:48 +0100 |
Removal of the unused atpset concept, the atp attribute and some related code.
|
file | diff | annotate |
| Wed, 07 Oct 2009 14:01:26 +0200 |
tuned proofs
|
file | diff | annotate |
| Sat, 19 Sep 2009 07:38:03 +0200 |
inter and union are mere abbreviations for inf and sup
|
file | diff | annotate |
| Mon, 31 Aug 2009 14:09:42 +0200 |
tuned the simp rules for Int involving insert and intervals.
|
file | diff | annotate |
| Tue, 28 Jul 2009 13:37:09 +0200 |
Set.UNIV and Set.empty are mere abbreviations for top and bot
|
file | diff | annotate |
| Wed, 22 Jul 2009 18:02:10 +0200 |
moved complete_lattice &c. into separate theory
|
file | diff | annotate |
| Wed, 22 Jul 2009 14:20:32 +0200 |
set intersection and union now named inter and union; closer connection between set and lattice operations; factored out complete lattice
|
file | diff | annotate |
| Tue, 21 Jul 2009 14:38:07 +0200 |
attempt for more concise setup of non-etacontracting binders
|
file | diff | annotate |
| Tue, 21 Jul 2009 11:09:50 +0200 |
Set.thy: prefer = over == where possible; tuned ML setup; dropped (moved) ML legacy
|
file | diff | annotate |
| Tue, 21 Jul 2009 07:54:44 +0200 |
swapped bootstrap order of UNION/Union and INTER/Inter in theory Set
|
file | diff | annotate |
| Mon, 20 Jul 2009 15:24:15 +0200 |
less digestible
|
file | diff | annotate |
| Mon, 20 Jul 2009 11:47:17 +0200 |
refined outline structure
|
file | diff | annotate |
| Mon, 20 Jul 2009 09:52:09 +0200 |
merged
|
file | diff | annotate |
| Mon, 20 Jul 2009 08:31:12 +0200 |
closer relation of sets and complete lattices; corresponding consts, defs and syntax at similar places in theory text
|
file | diff | annotate |
| Mon, 20 Jul 2009 08:32:07 +0200 |
merged
|
file | diff | annotate |
| Tue, 14 Jul 2009 15:54:19 +0200 |
refinement of lattice classes
|
file | diff | annotate |
| Wed, 15 Jul 2009 23:48:21 +0200 |
more antiquotations;
|
file | diff | annotate |
| Sat, 11 Jul 2009 21:33:01 +0200 |
added boolean_algebra type class; tuned lattice duals
|
file | diff | annotate |
| Mon, 06 Jul 2009 21:24:30 +0200 |
structure Thm: less pervasive names;
|
file | diff | annotate |
| Mon, 15 Jun 2009 16:13:19 +0200 |
authentic syntax for Pow and image
|
file | diff | annotate |
| Fri, 05 Jun 2009 08:06:03 +0200 |
merged
|
file | diff | annotate |
| Thu, 04 Jun 2009 15:28:59 +0200 |
insert now qualified and with authentic syntax
|
file | diff | annotate |
| Thu, 04 Jun 2009 19:44:06 +0200 |
finite lemmas
|
file | diff | annotate |
| Mon, 18 May 2009 23:15:38 +0200 |
fine-tuned elimination of comprehensions involving x=t.
|
file | diff | annotate |
| Sat, 16 May 2009 11:28:02 +0200 |
"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
|
file | diff | annotate |
| Tue, 31 Mar 2009 13:23:39 +0200 |
tuned;
|
file | diff | annotate |
| Thu, 19 Mar 2009 14:08:41 +0100 |
tuned some theorem and attribute bindings
|
file | diff | annotate |
| Sat, 14 Mar 2009 12:50:29 +0100 |
reverted to old version of Set.thy -- strange effects have to be traced first
|
file | diff | annotate |
| Sat, 07 Mar 2009 15:20:32 +0100 |
restructured theory Set.thy
|
file | diff | annotate |
| Thu, 05 Mar 2009 08:23:11 +0100 |
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
|
file | diff | annotate |
| Fri, 13 Feb 2009 23:55:04 +0100 |
finiteness lemmas
|
file | diff | annotate |
| Thu, 29 Jan 2009 22:28:03 +0100 |
Added strong congruence rule for UN.
|
file | diff | annotate |
| Fri, 10 Oct 2008 06:45:53 +0200 |
`code func` now just `code`
|
file | diff | annotate |
| Mon, 11 Aug 2008 14:50:00 +0200 |
rudimentary code setup for set operations
|
file | diff | annotate |
| Tue, 01 Jul 2008 06:51:59 +0200 |
remove simp attribute from range_composition
|
file | diff | annotate |
| Tue, 10 Jun 2008 15:30:56 +0200 |
removed some dubious code lemmas
|
file | diff | annotate |
| Wed, 07 May 2008 10:56:43 +0200 |
- Now uses Orderings as parent theory
|
file | diff | annotate |
| Tue, 22 Apr 2008 08:33:16 +0200 |
constant HOL.eq now qualified
|
file | diff | annotate |
| Wed, 02 Apr 2008 15:58:32 +0200 |
explicit class "eq" for operational equality
|
file | diff | annotate |
| Sat, 29 Mar 2008 19:14:00 +0100 |
replaced 'ML_setup' by 'ML';
|
file | diff | annotate |
| Wed, 19 Mar 2008 22:47:35 +0100 |
eliminated change_claset/simpset;
|
file | diff | annotate |
| Tue, 26 Feb 2008 20:38:15 +0100 |
moved some set lemmas from Set.thy here
|
file | diff | annotate |
| Fri, 25 Jan 2008 14:54:41 +0100 |
improved code theorem setup
|
file | diff | annotate |
| Wed, 02 Jan 2008 15:14:02 +0100 |
splitted class uminus from class minus
|
file | diff | annotate |
| Fri, 30 Nov 2007 20:13:03 +0100 |
adjustions to due to instance target
|
file | diff | annotate |
| Thu, 29 Nov 2007 17:08:26 +0100 |
instance command as rudimentary class target
|
file | diff | annotate |
| Fri, 23 Nov 2007 21:09:33 +0100 |
interpretation of typedecls: instantiation to class type
|
file | diff | annotate |
| Fri, 09 Nov 2007 13:41:27 +0100 |
avoid name clashes when generating code for union, inter
|
file | diff | annotate |
| Mon, 05 Nov 2007 18:18:39 +0100 |
added lemmas
|
file | diff | annotate |
| Wed, 26 Sep 2007 20:27:58 +0200 |
convenient obtain rule for sets
|
file | diff | annotate |
| Thu, 20 Sep 2007 16:37:30 +0200 |
clarified code lemmas
|
file | diff | annotate |
| Fri, 24 Aug 2007 14:14:16 +0200 |
made sets executable
|
file | diff | annotate |
| Sun, 19 Aug 2007 21:21:37 +0200 |
Made UN_Un simp
|
file | diff | annotate |