infoview is a unique feature

Stream: new members

[Huỳnh Trần Khanh]

is infoview a unique feature of lean? does this feature exist in other theorem proving languages?

[Huỳnh Trần Khanh]

i'm browsing an isabelle/hol proof right now and there is no infoview :cry:

[Patrick Massot]

Of course it exists everywhere. Otherwise the software isn't called an interactive theorem prover.

[Jason Rute]

But, some theorem provers, like HOL Light for one example, do the interactive part very differently. I guess the question is what is it about the info view that you are asking about?

[Huỳnh Trần Khanh]

so... I know this is somewhat off topic but where is the infoview in Isabelle/HOL :joy: