revert to plain for now mkdir

one unified Word theory

more speaking names

more speaking names

moved specific operations here

more speaking theory names

more speaking theory names

use existing bit type from theory Bit

split off Cardinality from Numeral_Type

added literal and typerep instances

mkdir_leaf -- avoiding surprises with typos in user-given paths

generalize some lemmas about derivatives

add lemma at_within_interior

generalize more euclidean_space lemmas

minimize dependencies on Numeral_Type

change type of 'dimension' to 'a itself => nat

generalize some euclidean_space lemmas

merged

rewrote the TPTP problem generation code more or less from scratch; there is now an explicit AST data structure which will make it easy to support alternative formats (e.g., DFG, sorted TPTP, sorted DFG); also, if "full_types" is enabled, "hAPP" is then tagged properly

rename functions

merged

unfold_fun_n

pervasive tuning of code

explicit printing function for applify

fail with low-level exception, not user error;

eliminated some unused bindings;

recovered some indentation from the depths of time;

cleaned by using descending instead of lifting

merged

move function