Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] make_string ; PolyML structure

view this post on Zulip Email Gateway (Aug 22 2022 at 17:38):

From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
And maybe related to the question below, what has happened to the PolyML
structure? In an Isabelle session it seems to be reduced to a single
item, structure IntInf

(I would normally expect that PolyML.makestring would solve the problem
I describe below)

Jeremy

view this post on Zulip Email Gateway (Aug 22 2022 at 17:39):

From: Makarius <makarius@sketis.net>
Contemporary Isabelle has a managed ML environment called "Isabelle/ML".
Applications no longer have access to the raw Poly/ML bootstrap
environment (what was also called "the ML level" some decades ago).

Makarius

Last updated: Apr 19 2024 at 16:20 UTC