Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
Tue, 07 Oct 2014 23:29:43 +0200 |
wenzelm |
more bibtex entries;
|
file |
diff |
annotate
|
Wed, 23 Apr 2014 10:23:27 +0200 |
blanchet |
move size hooks together, with new one preceding old one and sharing same theory data
|
file |
diff |
annotate
|
Thu, 03 Apr 2014 10:51:22 +0200 |
blanchet |
use same idiom as used for datatype 'size' function to name constants and theorems emerging from various type interpretations -- reduces the chances of name clashes on theory merges
|
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
|
Sun, 16 Mar 2014 18:09:04 +0100 |
haftmann |
normalising simp rules for compound operators
|
file |
diff |
annotate
|
Thu, 06 Mar 2014 13:36:48 +0100 |
blanchet |
renamed 'map_pair' to 'map_prod'
|
file |
diff |
annotate
|
Fri, 17 Jan 2014 10:02:50 +0100 |
blanchet |
folded 'Wellfounded_More_FP' into 'Wellfounded'
|
file |
diff |
annotate
|
Sun, 10 Nov 2013 15:05:06 +0100 |
haftmann |
qualifed popular user space names
|
file |
diff |
annotate
|
Sat, 20 Oct 2012 09:09:34 +0200 |
bulwahn |
adjusting proofs
|
file |
diff |
annotate
|
Wed, 22 Aug 2012 22:55:41 +0200 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
Tue, 03 Apr 2012 17:26:30 +0900 |
griff |
renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
|
file |
diff |
annotate
|
Mon, 12 Mar 2012 15:12:22 +0100 |
noschinl |
tuned pred_set_conv lemmas. Skipped lemmas changing the lemmas generated by inductive_set
|
file |
diff |
annotate
|
Mon, 12 Mar 2012 15:11:24 +0100 |
noschinl |
tuned simpset
|
file |
diff |
annotate
|
Fri, 24 Feb 2012 22:46:44 +0100 |
haftmann |
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
|
file |
diff |
annotate
|
Fri, 24 Feb 2012 09:40:02 +0100 |
haftmann |
given up disfruitful branch
|
file |
diff |
annotate
|
Thu, 23 Feb 2012 21:25:59 +0100 |
haftmann |
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
|
file |
diff |
annotate
|
Mon, 30 Jan 2012 13:55:19 +0100 |
bulwahn |
adding code_unfold to make measure executable
|
file |
diff |
annotate
|
Sat, 28 Jan 2012 06:13:03 +0100 |
bulwahn |
reverting 46c2c96f5d92 as it only provides mostly non-terminating executions for generated code
|
file |
diff |
annotate
|
Wed, 25 Jan 2012 16:07:48 +0100 |
bulwahn |
adding very basic code generation to Wellfounded theory
|
file |
diff |
annotate
|
Tue, 10 Jan 2012 18:12:55 +0100 |
berghofe |
pred_subset_eq and SUP_UN_eq2 are now standard pred_set_conv rules
|
file |
diff |
annotate
|
Sat, 24 Dec 2011 15:53:10 +0100 |
haftmann |
adjusted to set/pred distinction by means of type constructor `set`
|
file |
diff |
annotate
|
Thu, 13 Oct 2011 23:02:59 +0200 |
haftmann |
moved acyclic predicate up in hierarchy
|
file |
diff |
annotate
|
Thu, 13 Oct 2011 22:56:19 +0200 |
haftmann |
modernized definitions
|
file |
diff |
annotate
|
Tue, 20 Sep 2011 21:47:52 +0200 |
haftmann |
tuned specification and lemma distribution among theories; tuned proofs
|
file |
diff |
annotate
|
Thu, 15 Sep 2011 12:40:08 -0400 |
hoelzl |
removed further legacy rules from Complete_Lattices
|
file |
diff |
annotate
|
Tue, 13 Sep 2011 17:07:33 -0700 |
huffman |
tuned proofs
|
file |
diff |
annotate
|
Thu, 11 Aug 2011 09:15:45 +0200 |
krauss |
removed unused material, which does not really belong here
|
file |
diff |
annotate
|
Wed, 01 Jun 2011 15:53:47 +0200 |
nipkow |
tuned lemmas
|
file |
diff |
annotate
|
Wed, 01 Jun 2011 11:51:25 +0200 |
nipkow |
new lemmas
|
file |
diff |
annotate
|