[isabelle] Isabelle + Polyml 4.20 + IntelMac + CVS Snapshot



Hello,

i think i have got polyml running on my IntelMac now.
So i can now continue getting Isabelle running.


Trying to compile the pure logics i get the some errors (attached at the end).

There seem to be some problems with the CPure Theory. As i can see in the changelog file, there have been some changes in the CPure Theory.

Any ideas how to solve the problem?


Thanks

	Martin



---------
Errormessage i got by compiling the Pure Logics:

Started at Do Jun 29 17:50:50 CEST 2006 (polyml-4.2.0_unknown- platform on martin-klebermas-computer.local)
Building Pure ...
Pure FAILED
(see also /usr/local/Isabelle_29-Jun-2006/heaps/polyml-4.2.0_unknown- platform/log/Pure)

lemma conjunction_imp:
(PROP ?A && PROP ?B ==> PROP ?C) == ([| PROP ?A; PROP ?B |] ==> PROP ?C)
val it = () : unit
structure Pure : sig val thy : Theory.theory end
val it = () : unit
Loading theory "CPure"
*** Bind
*** Theory data method Pure/simpset.extend failed
*** At command "theory" (line 7 of "/usr/local/Isabelle_29-Jun-2006/ src/Pure/CPure.thy").
Exception- TOPLEVEL_ERROR raised

make[1]: *** [/usr/local/Isabelle_29-Jun-2006/heaps/ polyml-4.2.0_unknown-platform/Pure] Error 3
make: *** [Pure] Error 2
Finished at Do Jun 29 17:56:06 CEST 2006
0:05:16 elapsed time, 0:05:14 cpu time






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