| 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
|
| Tue, 08 Feb 2011 07:42:08 +0100 |
nipkow |
added termination lemmas
|
file |
diff |
annotate
|
| Wed, 08 Dec 2010 13:34:50 +0100 |
haftmann |
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
|
file |
diff |
annotate
|
| Thu, 18 Nov 2010 17:01:16 +0100 |
haftmann |
map_pair replaces prod_fun
|
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
|
| Mon, 12 Jul 2010 10:48:37 +0200 |
haftmann |
dropped superfluous [code del]s
|
file |
diff |
annotate
|
| Fri, 11 Jun 2010 17:14:02 +0200 |
haftmann |
declare lex_prod_def [code del]
|
file |
diff |
annotate
|
| Wed, 05 May 2010 00:59:59 +0200 |
krauss |
repaired comments where SOMEthing went utterly wrong (cf. 2b04504fcb69)
|
file |
diff |
annotate
|
| Tue, 04 May 2010 08:55:43 +0200 |
haftmann |
locale predicates of classes carry a mandatory "class" prefix
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 12:58:52 +0100 |
blanchet |
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
|
file |
diff |
annotate
|
| Thu, 11 Mar 2010 14:40:29 +0100 |
haftmann |
Big_Operators now in Main rather than Plain
|
file |
diff |
annotate
|
| Wed, 10 Mar 2010 16:53:27 +0100 |
haftmann |
split off theory Big_Operators from theory Finite_Set
|
file |
diff |
annotate
|
| Thu, 18 Feb 2010 14:21:44 -0800 |
huffman |
get rid of many duplicate simp rule warnings
|
file |
diff |
annotate
|
| Mon, 26 Oct 2009 23:27:16 +0100 |
krauss |
authentic constants; moved "acyclic" further down
|
file |
diff |
annotate
|
| Mon, 26 Oct 2009 23:26:57 +0100 |
krauss |
point-free characterization of well-foundedness
|
file |
diff |
annotate
|
| Mon, 26 Oct 2009 23:26:18 +0100 |
krauss |
replaced (outdated) comments by explicit statements
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 14:43:18 +0200 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 16:32:53 +0200 |
haftmann |
simplified proof
|
file |
diff |
annotate
|
| Mon, 31 Aug 2009 20:34:48 +0200 |
krauss |
moved lemma Wellfounded.in_inv_image to Relation.thy
|
file |
diff |
annotate
|
| Mon, 31 Aug 2009 20:34:44 +0200 |
krauss |
moved wfrec to Recdef.thy
|
file |
diff |
annotate
|
| Mon, 31 Aug 2009 20:32:00 +0200 |
krauss |
no consts_code for wfrec, as it violates the "code generation = equational reasoning" principle
|
file |
diff |
annotate
|
| Tue, 28 Jul 2009 13:37:08 +0200 |
haftmann |
explicit is better than implicit
|
file |
diff |
annotate
|
| Tue, 28 Jul 2009 08:48:56 +0200 |
krauss |
moved obsolete same_fst to Recdef.thy
|
file |
diff |
annotate
|
| Mon, 27 Jul 2009 21:47:41 +0200 |
krauss |
"more standard" argument order of relation composition (op O)
|
file |
diff |
annotate
|
| Sat, 25 Jul 2009 18:44:55 +0200 |
haftmann |
explicit is better than implicit
|
file |
diff |
annotate
|
| Tue, 23 Jun 2009 12:09:30 +0200 |
haftmann |
uniformly capitialized names for subdirectories
|
file |
diff |
annotate
|
| Sun, 26 Apr 2009 20:23:09 +0200 |
haftmann |
reverted slip in theory imports
|
file |
diff |
annotate
|
| Sun, 26 Apr 2009 08:34:53 +0200 |
haftmann |
adjusted to changes in power syntax
|
file |
diff |
annotate
|
| Wed, 11 Mar 2009 08:45:47 +0100 |
haftmann |
explicit code equations for some rarely used pred operations
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 23:40:23 +0100 |
haftmann |
changed import hierarchy
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 16:47:31 +0100 |
haftmann |
dropped ID
|
file |
diff |
annotate
|
| Tue, 16 Dec 2008 08:46:07 +0100 |
krauss |
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
|
file |
diff |
annotate
|
| Tue, 18 Nov 2008 21:17:14 +0100 |
krauss |
removed lemmas called lemma1 and lemma2
|
file |
diff |
annotate
|
| Wed, 12 Nov 2008 17:23:22 +0100 |
krauss |
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
|
file |
diff |
annotate
|
| Fri, 10 Oct 2008 06:45:53 +0200 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
| Tue, 07 Oct 2008 16:07:50 +0200 |
haftmann |
arbitrary is undefined
|
file |
diff |
annotate
|
| Wed, 17 Sep 2008 15:59:23 +0200 |
krauss |
wf_finite_psubset[simp], in_finite_psubset[simp]
|
file |
diff |
annotate
|
| Mon, 11 Aug 2008 14:49:53 +0200 |
haftmann |
moved class wellorder to theory Orderings
|
file |
diff |
annotate
|