Mizar vs Isar キーワード対応表

Mizar	Isar
let	fix
assume	assume
set	let
set	def
consider ... such that	obtain ... where
take	(no equivalent)
per cases ...	proof ... qed
suppose	next assume
(no keyword)	have
thus	show
hence	then show
thesis	(?thesis)
proof ... end	proof ... qed
@proof ... end	sorry
now ... end	{ ... }
then	then
then ... by	with
by	from
by	using
;	.
;	..
;	by auto
from ... ;	by (rule ... )