Store (nholz)

Store Module

Namespace: HOL
Assembly: nholz.dll

This module implements databases for storing theorems and lemmas under a name index. Like axioms, stored theorems are restricted to having no free variables or assumptions, whereas stored lemmas are theorems that have no such restrictions.

Functions and values

Function or value	Description
`get_all_lemmas ()` Full Usage: `get_all_lemmas ()` Parameters: () : `unit` Returns: `(string * thm) list`	() : `unit` Returns: `(string * thm) list`
`get_all_thms ()` Full Usage: `get_all_thms ()` Parameters: () : `unit` Returns: `(string * thm) list`	() : `unit` Returns: `(string * thm) list`
`get_lemma x` Full Usage: `get_lemma x` Parameters: x : `string` Returns: `thm`	x : `string` Returns: `thm`
`get_thm x` Full Usage: `get_thm x` Parameters: x : `string` Returns: `thm`	x : `string` Returns: `thm`
`save_lemma (x, th)` Full Usage: `save_lemma (x, th)` Parameters: x : `string` th : `thm` Returns: `thm`	x : `string` th : `thm` Returns: `thm`
`save_thm (x, th)` Full Usage: `save_thm (x, th)` Parameters: x : `string` th : `thm` Returns: `thm`	This is the theorem storage command. It takes a string and a theorem argument. The theorem gets stored in the database under the string index. The string must not be used for the name of an existing theorem (unless in benign redefinition), and the theorem must not contain free variables or or assumptions. x : `string` th : `thm` Returns: `thm`
`the_lemmas` Full Usage: `the_lemmas` Returns: `dltree<string, thm> ref`	Returns: `dltree<string, thm> ref`
`the_theorems` Full Usage: `the_theorems` Returns: `dltree<string, thm> ref`	Returns: `dltree<string, thm> ref`