Help Index
A
B
C
D
E
F
G
H
I
J
K
L
M
N
O
P
Q
R
S
T
U
V
W
X
Y
Z
A
Abstract Machines
AMN
Operations
Substitutions
Analysed Form
Analyser
Animator
Annotations
Annotations
Positioning
Antecedents
ASCII
ASCII
ASSERTIONS Clause
AutoProver
B
B-Method
B-Platform
Memory
B-Theory Language
B-Toolkit
Installation
Library Requirements
Running
BToolProver
BToolkitd
Backtracking
BASE
Base Generators
basic io
Bit TYPE
Bool TYPE
BProcessInfo
BUnlock
C
Cartesian Product
Changing Directory
Close
Code Sharing
Command Bar
Command Buttons
Commit
CommitEdits
Concatenation
Generalised
Conjunction
Consequent
CONSTANTS
CONSTANTS Clause
CONSTRAINTS Clause
Constructs
Area
Colour-coding
Name length
CreateSLIB
D
DEFINITIONS Clause
Dependent Constructs
Design Overview
Development Environment
Disjunction
Disk Contents
Display Area
Documents
Document Mark Up
E
Editor
Enumerator
Environment
BKIT
PATH
XBMotif
Environments
Documents
Generators
Main
Provers
Translators
Equals
Equivalence
Expressions
Expression List
EXTENDS Clause
Syntax
Using
F
file dump
Find
Formula
Freeness
Functions
Functions
Application
Bijection
Partial
Total
G
Getting Started
GLOBAL
Goals
Current
Set
Guards
bident
Guards
binhyp
breade
bsearch
btest
H
Help
Hypertext
Hypotheses
Current set
Hypotheses
Viewing
I
Identifier
Upper Case
Variable
Variable List
IMPLEMENTATION
IMPLEMENTATION
Implication
IMPORTS Clause
Syntax
Using
Syntax
Using
Backwards
Forwards
Rewriting
Inference Rules
Backward
Forward
Ordering
Rewrite
Simple
Information Hiding
Information Panel
INITIALISATION Clause
Injection
Partial
Total
Installation
Errors
Generator
Motif
Non Motif
Motif
InterProver
Introduce
IntroduceSLIB
IntroduceSRC
IntroduceTLIB
INVARIANT
INVARIANT Clause
J
Joker
K
L
latex
Layered Approach
Lemma
Lemma creation
Lemma proof
Library Machines
Input Output Machines
Mathematical Concepts Machines
Library Machines
Multiple Objects Machines
Programming Concepts Machines
Type Machines
Licence File
Linker
Name Clashes
Lock
M
MACHINE
MACHINE
Mathematical Notation
MiniRemake
Mouse
N
Natural Numbers
Addition
Difference
Division
Inequality
Interval
Maximum
Minimum
Product
Remainder
Set of
Natural Numbers
Set of
Non zero
Negation
Not Equals
Not Set Inclusion
Not Set Member
Not Strict Set Inclusion
Newlines
Non Determinism
Normaliser
Number
O
ON Clause
Operations
Query
OPERATIONS Clause
Operator Binding
Operator Priorities
Options
Construct Display
Documents
Document Mark Up Language
Options
Editor
Interface
Programming Language
Remake
op name
Ordered Pair
Overview
P
Palettes
Pattern Match
Predicates
PRE Clause
Print
PROMOTES
PROMOTES Clause
Syntax
Using
Construction
Cycle
Proof
Guidelines
Levels
PROOFMETHOD File
ProofPrinter
Proof Obligation
File
Generator
PROPERTIES Clause
Q
Quantification
Existential
Lambda Abstraction
Unbounded Choice
Quantification
Universal
Quoted String
R
Reasoning Depth
REFINEMENT
REFINEMENT
Refinement
REFINES Clause
Relations
Anti Domain Restriction
Anti Range Restriction
Closure
Codomain
Composition
Domain
Domain Restriction
Identity
Image
Inverse
Iteration
Overriding
Product, Direct
Product, Parallel
Projection
Range Restriction
Relation
Remake
Remove
Rename
Rename ffnc obj
Rename file io
Rename fnc obj
Rename Narr
Rename Nfnc
Rename Nseq
Rename Nvar
Rename seq obj
Rename set
Rename set obj
Rename str obj
Rename token io
Rename Varr
Rename Vffnc
Rename Vfnc
Rename Vseq
Rename Vvar
Renaming
INCLUDES
Renaming Library Machines
Reset
ResetLevel
Reset Construct
Run
S
Save Development
Scalar TYPE
SEES Clause
Syntax
Using
Sequences
Append
Bijective
Concatenation
Empty
Enumeration
Finite
First Element
Frint
Injective
Last Element
Prepend
Projection
Reverse
Singleton
Size of
Tail
SETS
Sets
Cardinality
Comprehension
Difference
Empty
Enumeration
Inclusion
Intersection
Generalised
UGeneralised
Membership
Power
Product
Sets
Singleton
Subsets
Finite
Finite Non Empty
Non empty
Summation
Union
Generalised
UGeneralised
SETS Clause
Show
Show Unproved
Simple Rule
Specification Overview
Stateless Machine
Status
String TYPE
Structuring Developments
Substitutions
Application
Choice
Generalised
Guarded
Parameterised
Postconditioned
Preconditioned
Sequencing
Simple
Simultaneous
skip
Partial
Total
System Library
Files
.c
.g
.h
T
Tactic
Atomic
DED
Default
FEQL
Forward
GEN
HYP
Normal
Special
SUB
Tactic
User
Theory
Theory Name
Tool Bar
Top Bar
Translator
TypeChecker
Type determining predicate
Type File
U
Users Theory
FwdUsersTheory
in Animator
in InterProver
UsersTheory
Syntax
USES Clause
Using
USETAC Clause
Utilities
V
Variables
VARIABLES Clause
W
X
Y
Z
A full on-line help listing is available in the
Contents Page
©
B-Core (UK) Limited
, Last updated: 22 Feb 2002
© B-Core
(UK) Limited, Last updated: 22 Feb 2002
