FAQ  Admin  GUI  Term  Objects  FormalContent  ExpressionTree  Refiner  Tactics  Nuprl2015  System  Fragments  Web 

FAQ:
  
faq flags
  using the faq
  special FAQs
  data structure documentation conventions

Admin:
  
vncviewer
  emacs
  nuprl accounts
  Connecting to nuprl servers.
  patching a VM
  SSH basics
  ssh
  TODO
  user identity
  UUID

GUI:
  
ML Scanner not character
  twm
  manipulating structured lists
  GUI overview
  GUI Buttons
  Term Text
  enter in text does not break line.
  nuprl process emacs toploop.
  Interactive TopLoop
  instantiating terms
  The Navigator
  proof editor concepts
  dialog_view_hook
  Starting an Editor
  Proof Search Tool

Term:
  
TermSig
  Term
  Definition
  Substition
  ascii term syntax
  Terms as Data Structures

Objects:
  
object versions overview
  version history merge
  what does activating an object do
  Saving and compiling ML code.
  Using LibSearch to find arbitrary objects.
  How to recover object deleted (RmLink) from directory.
  obid graph
  object tables
  Objects and Object Ids
  Object Menu
  How proofs are stored in the libary.
  Proof CLI
  Object properties

FormalContent:
  
Exporting theories to the Web
  Reference Environment
  MkTHY*
  Add new theory to user theory group
  Theories
  Theory Group
  Proofs as Data
  Tactic Expressions
  Separate Refinement
  Goals and Sequents
  INF objects

ExpressionTree:
  
Expression Trees
  Searching Directory Tree

Refiner:
  
interrupting a refiner
  Refiner process.
  Rule interpreter args
  Command Line Proof manipulation
  Rebuild subtree reordering.
  Kreitzing and dekreitzing

Tactics:
  
ML
  Basic tactics
  How to write your own tactics
  Rewriting with order relations.
  RelRST (using reflexive, symmetric, transitive relations)
  override default typing lemma
  functionality and rewriting

Nuprl2015:
  
MkTHY button missing from /theories/user

System:
  
transaction
  Killing rebuild and refine tools
  Sequentializing Concurrent Transactions
  Transaction read clash
  System Architecture
  System Overview
  notifiable_process
  print output
  queries
  Bots
  Events

Fragments:
  
dbbot
  dbbot dialog hooks
  tnf bot
  Tactic Data
  Tactical Normal Form
  dekreitz fragments
  Clean up bad replay
  Redo hpf
  Fix HIE/Hrank
  fragment table maintainence recipes
  fragment table maintenance functions
  Alpha normalized fragments
  Story
  fragment policies
  Using Fragments to suggest proof completions.
  Fragment equality and matching functions
  Interactive Fragment Pipeline
  Replay from fragments.
  Fragments Overview
  Fragment
  Interactive Fragment recipes
  Thin Fragments
  Alpha generalized fragments
  Fragment record structure
  Fragment tactic structures

Web:
  
Fragment Dashboard

Top