--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/Mercurial/isabelle-style-1.3.1.diff Wed Apr 20 17:17:01 2011 +0200
@@ -0,0 +1,140 @@
+diff -Naur gitweb/changelogentry.tmpl isabelle/changelogentry.tmpl
+--- gitweb/changelogentry.tmpl 2011-04-20 12:13:37.000000000 +0200
++++ isabelle/changelogentry.tmpl 2011-04-20 12:13:37.000000000 +0200
+@@ -1,14 +1,12 @@
+ <div>
+-<a class="title" href="{url}rev/{node|short}{sessionvars%urlparameter}"><span class="age">{date|age} ago</span>{desc|strip|firstline|escape|nonempty}<span class="logtags"> {inbranch%inbranchtag}{branches%branchtag}{tags%tagtag}</span></a>
+-</div>
+-<div class="title_text">
+-<div class="log_link">
+-<a href="{url}rev/{node|short}{sessionvars%urlparameter}">changeset</a><br/>
+-</div>
+-<i>{author|obfuscate} [{date|rfc822date}] rev {rev}</i><br/>
++<a class="title" href="{url}rev/{node|short}{sessionvars%urlparameter}"><span class="age">{date|age}</span>
++{author|obfuscate} [{date|rfc822date}] rev {rev}<span class="logtags"> {inbranch%inbranchtag}{branches%branchtag}{tags%tagtag}</span></a>
+ </div>
+ <div class="log_body">
+ {desc|strip|escape|addbreaks|nonempty}
+ <br/>
++<div class="files">
++{files}
++</div>
+ <br/>
+ </div>
+diff -Naur gitweb/changeset.tmpl isabelle/changeset.tmpl
+--- gitweb/changeset.tmpl 2011-04-20 12:13:37.000000000 +0200
++++ isabelle/changeset.tmpl 2011-04-20 12:13:37.000000000 +0200
+@@ -29,7 +29,7 @@
+ <div class="title_text">
+ <table cellspacing="0">
+ <tr><td>author</td><td>{author|obfuscate}</td></tr>
+-<tr><td></td><td>{date|date} ({date|age} ago)</td></tr>
++<tr><td></td><td>{date|date} ({date|age})</td></tr>
+ {branch%changesetbranch}
+ <tr><td>changeset {rev}</td><td style="font-family:monospace">{node|short}</td></tr>
+ {parent%changesetparent}
+diff -Naur gitweb/fileannotate.tmpl isabelle/fileannotate.tmpl
+--- gitweb/fileannotate.tmpl 2011-04-20 12:13:37.000000000 +0200
++++ isabelle/fileannotate.tmpl 2011-04-20 12:13:37.000000000 +0200
+@@ -36,7 +36,7 @@
+ <td>{author|obfuscate}</td></tr>
+ <tr>
+ <td></td>
+- <td>{date|date} ({date|age} ago)</td></tr>
++ <td>{date|date} ({date|age})</td></tr>
+ {branch%filerevbranch}
+ <tr>
+ <td>changeset {rev}</td>
+diff -Naur gitweb/filerevision.tmpl isabelle/filerevision.tmpl
+--- gitweb/filerevision.tmpl 2011-04-20 12:13:37.000000000 +0200
++++ isabelle/filerevision.tmpl 2011-04-20 12:13:37.000000000 +0200
+@@ -36,7 +36,7 @@
+ <td>{author|obfuscate}</td></tr>
+ <tr>
+ <td></td>
+- <td>{date|date} ({date|age} ago)</td></tr>
++ <td>{date|date} ({date|age})</td></tr>
+ {branch%filerevbranch}
+ <tr>
+ <td>changeset {rev}</td>
+diff -Naur gitweb/graph.tmpl isabelle/graph.tmpl
+--- gitweb/graph.tmpl 2011-04-20 12:13:37.000000000 +0200
++++ isabelle/graph.tmpl 2011-04-20 12:13:37.000000000 +0200
+@@ -63,7 +63,7 @@
+ var revlink = '<li style="_STYLE"><span class="desc">';
+ revlink += '<a class="list" href="{url}rev/_NODEID{sessionvars%urlparameter}" title="_NODEID"><b>_DESC</b></a>';
+ revlink += '</span> _TAGS';
+-revlink += '<span class="info">_DATE ago, by _USER</span></li>';
++revlink += '<span class="info">_DATE, by _USER</span></li>';
+
+ graph.vertex = function(x, y, color, parity, cur) {
+
+diff -Naur gitweb/map isabelle/map
+--- gitweb/map 2011-04-20 12:13:37.000000000 +0200
++++ isabelle/map 2011-04-20 12:13:37.000000000 +0200
+@@ -78,7 +78,7 @@
+ <tr style="font-family:monospace" class="parity{parity}">
+ <td class="linenr" style="text-align: right;">
+ <a href="{url}annotate/{node|short}/{file|urlescape}{sessionvars%urlparameter}#l{targetline}"
+- title="{node|short}: {desc|escape|firstline}">{author|user}@{rev}</a>
++ title="{node|short}: {desc|escape}">{author|user}@{rev}</a>
+ </td>
+ <td><pre><a class="linenr" href="#{lineid}" id="{lineid}">{linenumber}</a></pre></td>
+ <td><pre>{line|escape}</pre></td>
+@@ -150,7 +150,7 @@
+ tags = tags.tmpl
+ tagentry = '
+ <tr class="parity{parity}">
+- <td class="age"><i>{date|age} ago</i></td>
++ <td class="age"><i>{date|age}</i></td>
+ <td><a class="list" href="{url}rev/{node|short}{sessionvars%urlparameter}"><b>{tag|escape}</b></a></td>
+ <td class="link">
+ <a href="{url}rev/{node|short}{sessionvars%urlparameter}">changeset</a> |
+@@ -161,7 +161,7 @@
+ branches = branches.tmpl
+ branchentry = '
+ <tr class="parity{parity}">
+- <td class="age"><i>{date|age} ago</i></td>
++ <td class="age"><i>{date|age}</i></td>
+ <td><a class="list" href="{url}shortlog/{node|short}{sessionvars%urlparameter}"><b>{node|short}</b></a></td>
+ <td class="{status}">{branch|escape}</td>
+ <td class="link">
+@@ -204,11 +204,12 @@
+ inbranchtag = '<span class="inbranchtag" title="{name}">{name}</span> '
+ shortlogentry = '
+ <tr class="parity{parity}">
+- <td class="age"><i>{date|age} ago</i></td>
++ <td class="age"><i>{date|age}</i></td>
+ <td><i>{author|person}</i></td>
++ <td><i>{date|shortdate}</i></td>
+ <td>
+ <a class="list" href="{url}rev/{node|short}{sessionvars%urlparameter}">
+- <b>{desc|strip|firstline|escape|nonempty}</b>
++ <b>{desc|strip|escape|nonempty}</b>
+ <span class="logtags">{inbranch%inbranchtag}{branches%branchtag}{tags%tagtag}</span>
+ </a>
+ </td>
+@@ -219,10 +220,12 @@
+ </tr>'
+ filelogentry = '
+ <tr class="parity{parity}">
+- <td class="age"><i>{date|age} ago</i></td>
++ <td class="age"><i>{date|age}</i></td>
++ <td><i>{author|person}</i></td>
++ <td><i>{date|shortdate}</i></td>
+ <td>
+ <a class="list" href="{url}rev/{node|short}{sessionvars%urlparameter}">
+- <b>{desc|strip|firstline|escape|nonempty}</b>
++ <b>{desc|strip|escape|nonempty}</b>
+ </a>
+ </td>
+ <td class="link">
+@@ -238,7 +241,7 @@
+ </td>
+ <td>{description}</td>
+ <td>{contact|obfuscate}</td>
+- <td class="age">{lastchange|age} ago</td>
++ <td class="age">{lastchange|age}</td>
+ <td class="indexlinks">{archives%indexarchiveentry}</td>
+ <td><div class="rss_logo"><a href="{url}rss-log">RSS</a> <a href="{url}atom-log">Atom</a></div></td>
+ </tr>\n'
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/Mercurial/isabelle-style-1.4.3--1.8.2.diff Wed Apr 20 17:17:01 2011 +0200
@@ -0,0 +1,60 @@
+diff -Naur gitweb/changelogentry.tmpl isabelle/changelogentry.tmpl
+--- gitweb/changelogentry.tmpl 2011-04-20 12:27:29.000000000 +0200
++++ isabelle/changelogentry.tmpl 2011-04-20 12:32:48.000000000 +0200
+@@ -1,14 +1,12 @@
+ <div>
+-<a class="title" href="{url}rev/{node|short}{sessionvars%urlparameter}"><span class="age">{date|age}</span>{desc|strip|firstline|escape|nonempty}<span class="logtags"> {inbranch%inbranchtag}{branches%branchtag}{tags%tagtag}</span></a>
+-</div>
+-<div class="title_text">
+-<div class="log_link">
+-<a href="{url}rev/{node|short}{sessionvars%urlparameter}">changeset</a><br/>
+-</div>
+-<i>{author|obfuscate} [{date|rfc822date}] rev {rev}</i><br/>
++<a class="title" href="{url}rev/{node|short}{sessionvars%urlparameter}"><span class="age">{date|age}</span>
++{author|obfuscate} [{date|rfc822date}] rev {rev}<span class="logtags"> {inbranch%inbranchtag}{branches%branchtag}{tags%tagtag}</span></a>
+ </div>
+ <div class="log_body">
+ {desc|strip|escape|addbreaks|nonempty}
+ <br/>
++<div class="files">
++{files}
++</div>
+ <br/>
+ </div>
+diff -Naur gitweb/map isabelle/map
+--- gitweb/map 2011-04-20 12:27:29.000000000 +0200
++++ isabelle/map 2011-04-20 12:32:48.000000000 +0200
+@@ -78,7 +78,7 @@
+ <tr style="font-family:monospace" class="parity{parity}">
+ <td class="linenr" style="text-align: right;">
+ <a href="{url}annotate/{node|short}/{file|urlescape}{sessionvars%urlparameter}#l{targetline}"
+- title="{node|short}: {desc|escape|firstline}">{author|user}@{rev}</a>
++ title="{node|short}: {desc|escape}">{author|user}@{rev}</a>
+ </td>
+ <td><pre><a class="linenr" href="#{lineid}" id="{lineid}">{linenumber}</a></pre></td>
+ <td><pre>{line|escape}</pre></td>
+@@ -206,9 +206,10 @@
+ <tr class="parity{parity}">
+ <td class="age"><i>{date|age}</i></td>
+ <td><i>{author|person}</i></td>
++ <td><i>{date|shortdate}</i></td>
+ <td>
+ <a class="list" href="{url}rev/{node|short}{sessionvars%urlparameter}">
+- <b>{desc|strip|firstline|escape|nonempty}</b>
++ <b>{desc|strip|escape|nonempty}</b>
+ <span class="logtags">{inbranch%inbranchtag}{branches%branchtag}{tags%tagtag}</span>
+ </a>
+ </td>
+@@ -220,9 +221,11 @@
+ filelogentry = '
+ <tr class="parity{parity}">
+ <td class="age"><i>{date|age}</i></td>
++ <td><i>{author|person}</i></td>
++ <td><i>{date|shortdate}</i></td>
+ <td>
+ <a class="list" href="{url}rev/{node|short}{sessionvars%urlparameter}">
+- <b>{desc|strip|firstline|escape|nonempty}</b>
++ <b>{desc|strip|escape|nonempty}</b>
+ </a>
+ </td>
+ <td class="link">
--- a/Admin/Mercurial/isabelle-style.diff Wed Apr 20 16:49:52 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,73 +0,0 @@
-diff -r gitweb/changelogentry.tmpl isabelle/changelogentry.tmpl
-2,8c2,3
-< <a class="title" href="{url}rev/{node|short}{sessionvars%urlparameter}"><span class="age">{date|age} ago</span>{desc|strip|firstline|escape|nonempty}<span class="logtags"> {inbranch%inbranchtag}{branches%branchtag}{tags%tagtag}</span></a>
-< </div>
-< <div class="title_text">
-< <div class="log_link">
-< <a href="{url}rev/{node|short}{sessionvars%urlparameter}">changeset</a><br/>
-< </div>
-< <i>{author|obfuscate} [{date|rfc822date}] rev {rev}</i><br/>
----
-> <a class="title" href="{url}rev/{node|short}{sessionvars%urlparameter}"><span class="age">{date|age}</span>
-> {author|obfuscate} [{date|rfc822date}] rev {rev}<span class="logtags"> {inbranch%inbranchtag}{branches%branchtag}{tags%tagtag}</span></a>
-12a8,10
-> <div class="files">
-> {files}
-> </div>
-diff -r gitweb/changeset.tmpl isabelle/changeset.tmpl
-32c32
-< <tr><td></td><td>{date|date} ({date|age} ago)</td></tr>
----
-> <tr><td></td><td>{date|date} ({date|age})</td></tr>
-diff -r gitweb/fileannotate.tmpl isabelle/fileannotate.tmpl
-39c39
-< <td>{date|date} ({date|age} ago)</td></tr>
----
-> <td>{date|date} ({date|age})</td></tr>
-diff -r gitweb/filerevision.tmpl isabelle/filerevision.tmpl
-39c39
-< <td>{date|date} ({date|age} ago)</td></tr>
----
-> <td>{date|date} ({date|age})</td></tr>
-diff -r gitweb/graph.tmpl isabelle/graph.tmpl
-66c66
-< revlink += '<span class="info">_DATE ago, by _USER</span></li>';
----
-> revlink += '<span class="info">_DATE, by _USER</span></li>';
-diff -r gitweb/map isabelle/map
-81c81
-< title="{node|short}: {desc|escape|firstline}">{author|user}@{rev}</a>
----
-> title="{node|short}: {desc|escape}">{author|user}@{rev}</a>
-153c153
-< <td class="age"><i>{date|age} ago</i></td>
----
-> <td class="age"><i>{date|age}</i></td>
-164c164
-< <td class="age"><i>{date|age} ago</i></td>
----
-> <td class="age"><i>{date|age}</i></td>
-207c207
-< <td class="age"><i>{date|age} ago</i></td>
----
-> <td class="age"><i>{date|age}</i></td>
-208a209
-> <td><i>{date|shortdate}</i></td>
-211c212
-< <b>{desc|strip|firstline|escape|nonempty}</b>
----
-> <b>{desc|strip|escape|nonempty}</b>
-222c223,225
-< <td class="age"><i>{date|age} ago</i></td>
----
-> <td class="age"><i>{date|age}</i></td>
-> <td><i>{author|person}</i></td>
-> <td><i>{date|shortdate}</i></td>
-225c228
-< <b>{desc|strip|firstline|escape|nonempty}</b>
----
-> <b>{desc|strip|escape|nonempty}</b>
-241c244
-< <td class="age">{lastchange|age} ago</td>
----
-> <td class="age">{lastchange|age}</td>
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Wed Apr 20 16:49:52 2011 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Wed Apr 20 17:17:01 2011 +0200
@@ -273,7 +273,9 @@
@{const_name "ord_fun_inst.less_fun"},
@{const_name Metis.fequal},
@{const_name Meson.skolem},
- @{const_name transfer_morphism}
+ @{const_name transfer_morphism},
+ @{const_name enum_prod_inst.enum_all_prod},
+ @{const_name enum_prod_inst.enum_ex_prod}
(*@{const_name "==>"}, @{const_name "=="}*)]
val forbidden_mutant_consts =
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Wed Apr 20 16:49:52 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Wed Apr 20 17:17:01 2011 +0200
@@ -116,7 +116,14 @@
KK.TupleIndex (length js,
fold (fn j => fn accum => accum * univ_card + j) js 0)
-val tuple_set_from_atom_schema = foldl1 KK.TupleProduct o map KK.TupleAtomSeq
+(* This code is not just a silly optimization: It works around a limitation in
+ Kodkodi, whereby {} (i.e., KK.TupleProduct) is always given the cardinality
+ of the bound in which it appears, resulting in Kodkod arity errors. *)
+fun tuple_product (ts as KK.TupleSet []) _ = ts
+ | tuple_product _ (ts as KK.TupleSet []) = ts
+ | tuple_product ts1 ts2 = KK.TupleProduct (ts1, ts2)
+
+val tuple_set_from_atom_schema = fold1 tuple_product o map KK.TupleAtomSeq
val upper_bound_for_rep = tuple_set_from_atom_schema o atom_schema_of_rep
val single_atom = KK.TupleSet o single o KK.Tuple o single
@@ -358,17 +365,17 @@
fun tuple_perhaps_needy_atom upper j =
single_atom j
|> not discr
- ? (fn ts => KK.TupleProduct (ts,
- case exact_bound_for_perhaps_needy_atom j of
- SOME ts => ts
- | NONE => if upper then upper_bound_for_rep R2
- else KK.TupleSet []))
+ ? (fn ts => tuple_product ts
+ (case exact_bound_for_perhaps_needy_atom j of
+ SOME ts => ts
+ | NONE => if upper then upper_bound_for_rep R2
+ else KK.TupleSet []))
fun bound_tuples upper =
if null T1_need_vals then
if upper then
KK.TupleAtomSeq (epsilon - delta, delta + j0)
|> not discr
- ? (fn ts => KK.TupleProduct (ts, upper_bound_for_rep R2))
+ ? (fn ts => tuple_product ts (upper_bound_for_rep R2))
else
KK.TupleSet []
else
@@ -393,9 +400,8 @@
if T1 = T2 andalso epsilon > delta andalso
is_datatype_acyclic dtype then
index_seq delta (epsilon - delta)
- |> map (fn j =>
- KK.TupleProduct (KK.TupleSet [KK.Tuple [j + j0]],
- KK.TupleAtomSeq (atom_seq_for_self_rec j)))
+ |> map (fn j => tuple_product (KK.TupleSet [KK.Tuple [j + j0]])
+ (KK.TupleAtomSeq (atom_seq_for_self_rec j)))
|> n_fold_tuple_union
else
bound_tuples true]
--- a/src/HOL/ex/Quickcheck_Examples.thy Wed Apr 20 16:49:52 2011 +0200
+++ b/src/HOL/ex/Quickcheck_Examples.thy Wed Apr 20 17:17:01 2011 +0200
@@ -294,4 +294,28 @@
quickcheck[random, size = 10]
oops
+subsection {* Examples with locales *}
+
+locale Truth
+
+context Truth
+begin
+
+lemma "False"
+quickcheck[expect = no_counterexample]
+oops
+
end
+
+interpretation Truth .
+
+context Truth
+begin
+
+lemma "False"
+quickcheck[expect = counterexample]
+oops
+
+end
+
+end
--- a/src/Tools/quickcheck.ML Wed Apr 20 16:49:52 2011 +0200
+++ b/src/Tools/quickcheck.ML Wed Apr 20 17:17:01 2011 +0200
@@ -507,10 +507,14 @@
maps (fn (label, time) =>
Pretty.str (label ^ ": " ^ string_of_int time ^ " ms") :: Pretty.brk 1 :: []) (rev timings))
-fun pretty_counterex_and_reports ctxt auto (result :: _) =
- Pretty.chunks (pretty_counterex ctxt auto (response_of result) ::
- (* map (pretty_reports ctxt) (reports_of result) :: *)
- (if Config.get ctxt timing then cons (pretty_timings (timings_of result)) else I) [])
+fun pretty_counterex_and_reports ctxt auto [] =
+ Pretty.chunks [Pretty.strs (tool_name auto ::
+ space_explode " " "is used in a locale where no interpretation is provided."),
+ Pretty.strs (space_explode " " "Please provide an executable interpretation for the locale.")]
+ | pretty_counterex_and_reports ctxt auto (result :: _) =
+ Pretty.chunks (pretty_counterex ctxt auto (response_of result) ::
+ (* map (pretty_reports ctxt) (reports_of result) :: *)
+ (if Config.get ctxt timing then cons (pretty_timings (timings_of result)) else I) [])
(* automatic testing *)
@@ -593,11 +597,11 @@
fun quickcheck_params_cmd args = Context.theory_map (fold parse_test_param args);
fun check_expectation state results =
- (if found_counterexample (hd results) andalso expect (Proof.context_of state) = No_Counterexample
+ (if exists found_counterexample results andalso expect (Proof.context_of state) = No_Counterexample
then
error ("quickcheck expected to find no counterexample but found one")
else
- (if not (found_counterexample (hd results)) andalso expect (Proof.context_of state) = Counterexample
+ (if not (exists found_counterexample results) andalso expect (Proof.context_of state) = Counterexample
then
error ("quickcheck expected to find a counterexample but did not find one")
else ()))