CODEWITHSUNDEEP
isabelle
Fadoua
Fadoua

Reputation: 171

ML-programming in Isabelle (beginner)

I am learning how to write ML code in Isabelle (just started).

I am following the explanation and the examples in "The Isabelle Cookbook" (2013) and using Isabelle2017.

The function term_of and prop_of cannot be used anymore? Examples on page 12 give rise to ML error:

ML error⌂:
Value or constructor (prop_of) has not been declared

What are the new functions?

Thank you.

Upvotes: 1

Views: 173

Answers (1)

larsrh
larsrh

Reputation: 2659

Both of these need to be namespaced now: Thm.prop_of and Thm.term_of.

Upvotes: 2

Related Questions