<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
<!-- This is file org.lamport.tla.toobox.doc/html/model/tlc-options-page.html  -->


<html>
<head>
    <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
 <LINK href="../style.css" rel="stylesheet" type="text/css">

<title>TLC Options Page</title>
</head>
<!-- a comment here -->

<body>
<h1>TLC Options Page</h1>


<pre>
Contents
  <a href="#config">Configuration</a>
  <a href="#checking">Checking Mode</a>
  <a href="#featur