isabelle: 9a4c049f8997 tip
afp: af801987e595 tip
Running Separation_Logic_Imperative_HOL ...
*** Undefined fact: "sum_list_update_nat" (line 598 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Separation_Logic_Imperative_HOL/Examples/Hash_Table.thy")
*** At command "from" (line 598 of
"/mnt/home/ha
This does it nicely (20s):
apply (simp add: T⇩c_def I⇩c_def)
apply clarify
apply (cases u; elim disjE; simp; blast)
Larry
> On 25 Jun 2015, at 14:52, Larry Paulson wrote:
>
> I took a look, and it all runs perfectly well, except here:
>
>show "xs ∈ T⇩c ∧ ys ∈ T⇩c ∧
>
Hi Larry,
thanks for finding out so quickly!
Florian
Am 25.06.2015 um 16:02 schrieb Larry Paulson:
> This does it nicely (20s):
>
>apply (simp add: T⇩c_def I⇩c_def)
>apply clarify
>apply (cases u; elim disjE; simp; blast)
>
>
> Larry
>
>> On 25 Jun 2015, at 14:5
Maybe this is hitting the concrete wall set by hardware constraints.
I am building on lxbroy10; relevant settings might include
> ISABELLE_BUILD_JAVA_OPTIONS=-Xmx4096m -Xss2m
> ISABELLE_PLATFORM32=x86-linux
> ISABELLE_JAVA_SYSTEM_OPTIONS=-server -Dfile.encoding=UTF-8
> -Disabelle.threads=0
> ISA
I took a look, and it all runs perfectly well, except here:
show "xs ∈ T⇩c ∧ ys ∈ T⇩c ∧
ipurge_tr_rev I⇩c id u xs = ipurge_tr_rev I⇩c id u ys ⟶
{x. u = x ∧ xs @ [x] ∈ T⇩c} = {x. u = x ∧ ys @ [x] ∈ T⇩c}"
(* The following proof step performs an exhaustive case distinction over
a
isabelle: 19c277ea65ae tip
afp: 16e7d42ef7f4 tip
Running Noninterference_Generic_Unwinding ...
*** Timeout
Noninterference_Generic_Unwinding FAILED
(see also
/mnt/home/haftmann/data/isabelle/master/heaps/polyml-5.5.2_x86-linux/log/Noninterference_Generic_Unwinding)
val it = (): unit
Loading theor
solved in afp id 03689082b646
Am Dienstag, den 05.11.2013, 19:09 +0100 schrieb Florian Haftmann:
> isabelle id 9d623cada37f
> afp id 68e8895167cc
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailma
isabelle id 9d623cada37f
afp id 68e8895167cc
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
___
isabelle-dev ma
