[isabelle] Exception in conv.ML



Hi all,

have the following weird behaviour. After having applied auto on my goal, I am left with 24 subgoals. Applying 24 copies of the following invokation of the blast method solves all 24 subgoals. However, if I try to collaspe all of them into a single invokation apply(blast 25 ...)+, I get the exception below.

What is going wrong here? And how can I fix it?

If need be, I can make my theories available, but I doubt that I can produce a minimal core example.

apply(blast 25 intro: rtranclp_trans rtranclp_tranclp_tranclp
                      treds1r_cons_treds1r List1Red2 treds1t_cons_treds1t
               dest: t)

*** exception THM 1 raised (line 212 of "conv.ML"):
*** gconv_rule
*** EX es'' xs''.
***    P,e # es,n,h' |- (es'', xs'') [<-->] (stk', loc', pc', xcp') &
***    (if tmoves2 (compP2 P) h stk (e # es) pc xcp
***     then h' = h &
***          (if xcp' = Any --> pc < pc' then treds1r else treds1t) P t h
***           (e' # es, xs) (es'', xs'')
***     else EX ta' es' xs'.
***             treds1r P t h (e' # es, xs) (es', xs') &
***             P,t |- <<es',(h, xs')>> [-ta'->] <<es'',(h', xs'')>> &
***             ta_bisim wbisim1 (extTA2J1 P ta') ta &
***             ¬ tmoves1 P h es' &
***             (calls1 (e' # es) = None &
***              no_calls2 (e # es) pc & es' = e' # es & xs' = xs))
*** At command "apply"

Best regards,
Andreas

--
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 023
76131 Karlsruhe

Telefon: +49 721 608-48352
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.