Name Last modified Size Description![[PARENTDIR]](/icons/back.gif){kind=icon}
Parent Directory -
![[ ]](/icons/unknown.gif){kind=icon}
define_type.doc 2015-11-01 21:21 6.0K
REWR_CONV.doc 2015-11-01 21:21 5.6K
new_inductive_definition.doc 2015-11-01 21:21 4.9K
TARGET_REWRITE_TAC.doc 2015-11-01 21:21 4.7K
IMP_REWRITE_TAC.doc 2015-11-01 21:21 4.7K
lift_function.doc 2015-11-01 21:21 4.4K
SEMIRING_NORMALIZERS_CONV.doc 2015-11-01 21:21 4.1K
RING.doc 2015-11-01 21:21 4.0K
prove_recursive_functions_exist.doc 2015-11-01 21:21 3.8K
IMP_RES_THEN.doc 2015-11-01 21:21 3.8K
SUBGOAL_THEN.doc 2015-11-01 21:21 3.7K
REWRITE_TAC.doc 2015-11-01 21:21 3.6K
lift_theorem.doc 2015-11-01 21:21 3.4K
new_inductive_set.doc 2015-11-01 21:21 3.4K
define.doc 2015-11-01 21:21 3.2K
REAL_RING.doc 2015-11-01 21:21 3.1K
new_recursive_definition.doc 2015-11-01 21:21 3.1K
prove_general_recursive_function_exists.doc 2015-11-01 21:21 3.1K
GEN_REWRITE_TAC.doc 2015-11-01 21:21 3.1K
LABEL_TAC.doc 2015-11-01 21:21 3.0K
LIST_INDUCT_TAC.doc 2015-11-01 21:21 3.0K
INT_RING.doc 2015-11-01 21:21 2.8K
GEN_REWRITE_RULE.doc 2015-11-01 21:21 2.8K
MESON_TAC.doc 2015-11-01 21:21 2.7K
define_quotient_type.doc 2015-11-01 21:21 2.7K
GEN_REWRITE_CONV.doc 2015-11-01 21:21 2.7K
lookup.doc 2015-11-01 21:21 2.6K
derive_strong_induction.doc 2015-11-01 21:21 2.5K
search.doc 2015-11-01 21:21 2.5K
MATCH_CONV.doc 2015-11-01 21:21 2.4K
DEPTH_CONV.doc 2015-11-01 21:21 2.4K
pure_prove_recursive_function_exists.doc 2015-11-01 21:21 2.4K
derive_nonschematic_inductive_relations.doc 2015-11-01 21:21 2.4K
POP_ASSUM.doc 2015-11-01 21:21 2.4K
REAL_POLY_CONV.doc 2015-11-01 21:21 2.4K
prove_inductive_relations_exist.doc 2015-11-01 21:21 2.3K
ONCE_DEPTH_CONV.doc 2015-11-01 21:21 2.3K
self_destruct.doc 2015-11-01 21:21 2.3K
STRIP_ASSUME_TAC.doc 2015-11-01 21:21 2.3K
STRIP_THM_THEN.doc 2015-11-01 21:21 2.3K
MAP_FIRST.doc 2015-11-01 21:21 2.3K
REAL_LINEAR_PROVER.doc 2015-11-01 21:21 2.2K
CONV_TAC.doc 2015-11-01 21:21 2.2K
enter.doc 2015-11-01 21:21 2.2K
GEN_REAL_ARITH.doc 2015-11-01 21:21 2.2K
SIMP_CONV.doc 2015-11-01 21:21 2.2K
SEQ_IMP_REWRITE_TAC.doc 2015-11-01 21:21 2.2K
INTRO_TAC.doc 2015-11-01 21:21 2.1K
DISJ_CASES_THEN2.doc 2015-11-01 21:21 2.1K
HIGHER_REWRITE_CONV.doc 2015-11-01 21:21 2.1K
PART_MATCH.doc 2015-11-01 21:21 2.1K
X_CHOOSE_THEN.doc 2015-11-01 21:21 2.1K
overload_interface.doc 2015-11-01 21:21 2.1K
COND_CASES_TAC.doc 2015-11-01 21:21 2.1K
SUBST_ALL_TAC.doc 2015-11-01 21:21 2.0K
new_basic_type_definition.doc 2015-11-01 21:21 2.0K
STRIP_TAC.doc 2015-11-01 21:21 2.0K
UNIFY_ACCEPT_TAC.doc 2015-11-01 21:21 2.0K
REAL_ARITH.doc 2015-11-01 21:21 2.0K
SUBST1_TAC.doc 2015-11-01 21:21 2.0K
install_user_printer.doc 2015-11-01 21:21 2.0K
override_interface.doc 2015-11-01 21:21 2.0K
new_type_definition.doc 2015-11-01 21:21 2.0K
STRIP_GOAL_THEN.doc 2015-11-01 21:21 2.0K
THENL.doc 2015-11-01 21:21 2.0K
SUBS.doc 2015-11-01 21:21 2.0K
INTEGER_RULE.doc 2015-11-01 21:21 2.0K
let_CONV.doc 2015-11-01 21:21 1.9K
set_goal.doc 2015-11-01 21:21 1.9K
AC.doc 2015-11-01 21:21 1.9K
TOP_DEPTH_CONV.doc 2015-11-01 21:21 1.9K
DESTRUCT_TAC.doc 2015-11-01 21:21 1.9K
INT_POLY_CONV.doc 2015-11-01 21:21 1.9K
NUM_RING.doc 2015-11-01 21:21 1.9K
prove_constructors_injective.doc 2015-11-01 21:21 1.9K
int_ideal_cofactors.doc 2015-11-01 21:21 1.9K
STRUCT_CASES_TAC.doc 2015-11-01 21:21 1.9K
the_definitions.doc 2015-11-01 21:21 1.9K
real_ideal_cofactors.doc 2015-11-01 21:21 1.9K
sort.doc 2015-11-01 21:21 1.9K
DISJ_CASES_THEN.doc 2015-11-01 21:21 1.9K
MATCH_MP.doc 2015-11-01 21:21 1.8K
NUM_RED_CONV.doc 2015-11-01 21:21 1.8K
INDUCT_TAC.doc 2015-11-01 21:21 1.8K
HINT_EXISTS_TAC.doc 2015-11-01 21:21 1.8K
monotonicity_theorems.doc 2015-11-01 21:21 1.8K
WF_INDUCT_TAC.doc 2015-11-01 21:21 1.8K
REAL_RAT_RED_CONV.doc 2015-11-01 21:21 1.8K
combine.doc 2015-11-01 21:21 1.8K
ONCE_REWRITE_TAC.doc 2015-11-01 21:21 1.8K
basic_rewrites.doc 2015-11-01 21:21 1.8K
prove_constructors_distinct.doc 2015-11-01 21:21 1.8K
HYP_TAC.doc 2015-11-01 21:21 1.8K
REWRITE_RULE.doc 2015-11-01 21:21 1.8K
ORDERED_REWR_CONV.doc 2015-11-01 21:21 1.8K
MESON.doc 2015-11-01 21:21 1.8K
ASM_REAL_ARITH_TAC.doc 2015-11-01 21:21 1.8K
ONCE_ASM_REWRITE_TAC.doc 2015-11-01 21:21 1.8K
THEN.doc 2015-11-01 21:21 1.8K
prioritize_num.doc 2015-11-01 21:21 1.8K
PURE_REWRITE_TAC.doc 2015-11-01 21:21 1.8K
REDEPTH_CONV.doc 2015-11-01 21:21 1.8K
mk_prover.doc 2015-11-01 21:21 1.8K
GEN_NNF_CONV.doc 2015-11-01 21:21 1.7K
the_implicit_types.doc 2015-11-01 21:21 1.7K
prioritize_overload.doc 2015-11-01 21:21 1.7K
FIX_TAC.doc 2015-11-01 21:21 1.7K
instantiate_casewise_recursion.doc 2015-11-01 21:21 1.7K
type_invention_warning.doc 2015-11-01 21:21 1.7K
FIND_ASSUM.doc 2015-11-01 21:21 1.7K
help.doc 2015-11-01 21:21 1.7K
COND_ELIM_CONV.doc 2015-11-01 21:21 1.7K
CONDS_ELIM_CONV.doc 2015-11-01 21:21 1.7K
ASM_REWRITE_TAC.doc 2015-11-01 21:21 1.7K
new_basic_definition.doc 2015-11-01 21:21 1.7K
STRUCT_CASES_THEN.doc 2015-11-01 21:21 1.6K
ITAUT_TAC.doc 2015-11-01 21:21 1.6K
new_specification.doc 2015-11-01 21:21 1.6K
new_definition.doc 2015-11-01 21:21 1.6K
ANTE_RES_THEN.doc 2015-11-01 21:21 1.6K
DISJ_CASES.doc 2015-11-01 21:21 1.6K
e.doc 2015-11-01 21:21 1.6K
rightbin.doc 2015-11-01 21:21 1.6K
inductive_type_store.doc 2015-11-01 21:21 1.6K
REWRITE_CONV.doc 2015-11-01 21:21 1.6K
prioritize_real.doc 2015-11-01 21:21 1.6K
REAL_ARITH_TAC.doc 2015-11-01 21:21 1.6K
prioritize_int.doc 2015-11-01 21:21 1.6K
INST_UPPERCASE.doc 2015-11-01 21:21 1.6K
ASSUME_TAC.doc 2015-11-01 21:21 1.6K
TRANS_TAC.doc 2015-11-01 21:21 1.6K
CONDS_CELIM_CONV.doc 2015-11-01 21:21 1.5K
MATCH_MP_TAC.doc 2015-11-01 21:21 1.5K
REAL_RAT_REDUCE_CONV.doc 2015-11-01 21:21 1.5K
NUM_REDUCE_CONV.doc 2015-11-01 21:21 1.5K
SUB_CONV.doc 2015-11-01 21:21 1.5K
leftbin.doc 2015-11-01 21:21 1.5K
qmap.doc 2015-11-01 21:21 1.5K
lex.doc 2015-11-01 21:21 1.5K
the_overload_skeletons.doc 2015-11-01 21:21 1.5K
GEN_PART_MATCH.doc 2015-11-01 21:21 1.5K
CHOOSE_THEN.doc 2015-11-01 21:21 1.5K
print_unambiguous_comprehensions.doc 2015-11-01 21:21 1.5K
prove_cases_thm.doc 2015-11-01 21:21 1.5K
NUM_LT_CONV.doc 2015-11-01 21:21 1.5K
verbose.doc 2015-11-01 21:21 1.5K
DEPTH_BINOP_CONV.doc 2015-11-01 21:21 1.5K
ASM_INT_ARITH_TAC.doc 2015-11-01 21:21 1.5K
REAL_FIELD.doc 2015-11-01 21:21 1.5K
SELECT_CONV.doc 2015-11-01 21:21 1.4K
TAUT.doc 2015-11-01 21:21 1.4K
HYP_UPPERCASE.doc 2015-11-01 21:21 1.4K
type_invention_error.doc 2015-11-01 21:21 1.4K
BOOL_CASES_TAC.doc 2015-11-01 21:21 1.4K
GEN_MESON_TAC.doc 2015-11-01 21:21 1.4K
SKOLEM_CONV.doc 2015-11-01 21:21 1.4K
foldr.doc 2015-11-01 21:21 1.4K
REFUTE_THEN.doc 2015-11-01 21:21 1.4K
SPECL.doc 2015-11-01 21:21 1.4K
NNFC_CONV.doc 2015-11-01 21:21 1.4K
CASE_REWRITE_TAC.doc 2015-11-01 21:21 1.4K
vfree_in.doc 2015-11-01 21:21 1.4K
NUM_SIMPLIFY_CONV.doc 2015-11-01 21:21 1.4K
make_overloadable.doc 2015-11-01 21:21 1.4K
X_CHOOSE_TAC.doc 2015-11-01 21:21 1.4K
REAL_INT_RED_CONV.doc 2015-11-01 21:21 1.4K
basic_congs.doc 2015-11-01 21:21 1.4K
INT_OF_REAL_THM.doc 2015-11-01 21:21 1.4K
NNF_CONV.doc 2015-11-01 21:21 1.4K
DISCH_THEN.doc 2015-11-01 21:21 1.4K
ITAUT.doc 2015-11-01 21:21 1.3K
CLAIM_TAC.doc 2015-11-01 21:21 1.3K
ASM_ARITH_TAC.doc 2015-11-01 21:21 1.3K
foldl.doc 2015-11-01 21:21 1.3K
NUMBER_TAC.doc 2015-11-01 21:21 1.3K
inst.doc 2015-11-01 21:21 1.3K
INT_ARITH_TAC.doc 2015-11-01 21:21 1.3K
type_match.doc 2015-11-01 21:21 1.3K
PROP_ATOM_CONV.doc 2015-11-01 21:21 1.3K
mk_gabs.doc 2015-11-01 21:21 1.3K
extend_basic_convs.doc 2015-11-01 21:21 1.3K
REAL_RAT_MUL_CONV.doc 2015-11-01 21:21 1.3K
reverse_interface_mapping.doc 2015-11-01 21:21 1.3K
INT_RED_CONV.doc 2015-11-01 21:21 1.3K
PINST.doc 2015-11-01 21:21 1.3K
disjuncts.doc 2015-11-01 21:21 1.3K
CONJUNCTS_THEN.doc 2015-11-01 21:21 1.3K
REAL_RAT_INV_CONV.doc 2015-11-01 21:21 1.3K
REPEAT_TCL.doc 2015-11-01 21:21 1.3K
NUM_MOD_CONV.doc 2015-11-01 21:21 1.3K
ASSUM_LIST.doc 2015-11-01 21:21 1.3K
NUM_REDUCE_TAC.doc 2015-11-01 21:21 1.3K
comment_token.doc 2015-11-01 21:21 1.3K
POP_ASSUM_LIST.doc 2015-11-01 21:21 1.3K
elistof.doc 2015-11-01 21:21 1.3K
SELECT_ELIM_TAC.doc 2015-11-01 21:21 1.3K
TRANS.doc 2015-11-01 21:21 1.3K
CHANGED_CONV.doc 2015-11-01 21:21 1.3K
NUM_REL_CONV.doc 2015-11-01 21:21 1.3K
extend_basic_congs.doc 2015-11-01 21:21 1.3K
ORDERED_IMP_REWR_CONV.doc 2015-11-01 21:21 1.3K
REAL_INT_REDUCE_CONV.doc 2015-11-01 21:21 1.3K
the_inductive_definitions.doc 2015-11-01 21:21 1.3K
VALID.doc 2015-11-01 21:21 1.3K
NUM_DIV_CONV.doc 2015-11-01 21:21 1.3K
NUM_SUB_CONV.doc 2015-11-01 21:21 1.2K
listof.doc 2015-11-01 21:21 1.2K
REAL_RAT_ABS_CONV.doc 2015-11-01 21:21 1.2K
apply_prover.doc 2015-11-01 21:21 1.2K
REAL_RAT_POW_CONV.doc 2015-11-01 21:21 1.2K
augment.doc 2015-11-01 21:21 1.2K
INST_TYPE.doc 2015-11-01 21:21 1.2K
variant.doc 2015-11-01 21:21 1.2K
REAL_RAT_SUB_CONV.doc 2015-11-01 21:21 1.2K
MK_COMB_UPPERCASE.doc 2015-11-01 21:21 1.2K
FIRST_ASSUM.doc 2015-11-01 21:21 1.2K
REAL_RAT_DIV_CONV.doc 2015-11-01 21:21 1.2K
the_type_definitions.doc 2015-11-01 21:21 1.2K
INT_REDUCE_CONV.doc 2015-11-01 21:21 1.2K
mk_rewrites.doc 2015-11-01 21:21 1.2K
term_match.doc 2015-11-01 21:21 1.2K
REAL_POLY_POW_CONV.doc 2015-11-01 21:21 1.2K
INTEGER_TAC.doc 2015-11-01 21:21 1.2K
REAL_POLY_SUB_CONV.doc 2015-11-01 21:21 1.2K
PAT_CONV.doc 2015-11-01 21:21 1.2K
REAL_POLY_MUL_CONV.doc 2015-11-01 21:21 1.2K
REAL_RAT_MAX_CONV.doc 2015-11-01 21:21 1.2K
REAL_POLY_ADD_CONV.doc 2015-11-01 21:21 1.2K
new_axiom.doc 2015-11-01 21:21 1.2K
REAL_RAT_MIN_CONV.doc 2015-11-01 21:21 1.2K
net_of_thm.doc 2015-11-01 21:21 1.2K
REAL_RAT_ADD_CONV.doc 2015-11-01 21:21 1.2K
SPEC.doc 2015-11-01 21:21 1.2K
REAL_RAT_NEG_CONV.doc 2015-11-01 21:21 1.2K
FREEZE_THEN.doc 2015-11-01 21:21 1.2K
NUM_NORMALIZE_CONV.doc 2015-11-01 21:21 1.2K
SUBS_CONV.doc 2015-11-01 21:21 1.2K
ORELSE.doc 2015-11-01 21:21 1.2K
instantiate.doc 2015-11-01 21:21 1.2K
vsubst.doc 2015-11-01 21:21 1.2K
ideal_cofactors.doc 2015-11-01 21:21 1.2K
DISJ_CASES_TAC.doc 2015-11-01 21:21 1.2K
BINOP_TAC.doc 2015-11-01 21:21 1.2K
SIMPLE_DISJ_CASES.doc 2015-11-01 21:21 1.2K
subst.doc 2015-11-01 21:21 1.2K
parse_as_infix.doc 2015-11-01 21:21 1.2K
typify_universal_set.doc 2015-11-01 21:21 1.1K
basic_convs.doc 2015-11-01 21:21 1.1K
GEN_BETA_CONV.doc 2015-11-01 21:21 1.1K
REAL_POLY_NEG_CONV.doc 2015-11-01 21:21 1.1K
define_finite_type.doc 2015-11-01 21:21 1.1K
conjuncts.doc 2015-11-01 21:21 1.1K
FIRST_X_ASSUM.doc 2015-11-01 21:21 1.1K
SUBGOAL_TAC.doc 2015-11-01 21:21 1.1K
NUM_CANCEL_CONV.doc 2015-11-01 21:21 1.1K
CACHE_CONV.doc 2015-11-01 21:21 1.1K
MP_CONV.doc 2015-11-01 21:21 1.1K
CHOOSE_TAC.doc 2015-11-01 21:21 1.1K
NUM_EXP_CONV.doc 2015-11-01 21:21 1.1K
CHAR_EQ_CONV.doc 2015-11-01 21:21 1.1K
NUMBER_RULE.doc 2015-11-01 21:21 1.1K
NO_TAC.doc 2015-11-01 21:21 1.1K
INSTANTIATE_UPPERCASE.doc 2015-11-01 21:21 1.1K
ALL_TAC.doc 2015-11-01 21:21 1.1K
REPEAT_UPPERCASE.doc 2015-11-01 21:21 1.1K
CONJUNCTS_THEN2.doc 2015-11-01 21:21 1.1K
merge_nets.doc 2015-11-01 21:21 1.1K
REAL_RAT_EQ_CONV.doc 2015-11-01 21:21 1.1K
NUM_LE_CONV.doc 2015-11-01 21:21 1.1K
NUM_GE_CONV.doc 2015-11-01 21:21 1.1K
WEAK_CNF_CONV.doc 2015-11-01 21:21 1.1K
BETA.doc 2015-11-01 21:21 1.1K
ASSOC_CONV.doc 2015-11-01 21:21 1.1K
PROVE_HYP.doc 2015-11-01 21:21 1.1K
REAL_IDEAL_CONV.doc 2015-11-01 21:21 1.1K
term_order.doc 2015-11-01 21:21 1.1K
TRY.doc 2015-11-01 21:21 1.1K
SUBST_VAR_TAC.doc 2015-11-01 21:21 1.1K
CONV_RULE.doc 2015-11-01 21:21 1.1K
alphaorder.doc 2015-11-01 21:21 1.0K
REAL_INT_POW_CONV.doc 2015-11-01 21:21 1.0K
IMP_REWR_CONV.doc 2015-11-01 21:21 1.0K
NUM_GT_CONV.doc 2015-11-01 21:21 1.0K
BETA_CONV.doc 2015-11-01 21:21 1.0K
many.doc 2015-11-01 21:21 1.0K
ARITH_RULE.doc 2015-11-01 21:21 1.0K
TOP_SWEEP_CONV.doc 2015-11-01 21:21 1.0K
FORALL_UNWIND_CONV.doc 2015-11-01 21:21 1.0K
ABBREV_TAC.doc 2015-11-01 21:21 1.0K
PATH_CONV.doc 2015-11-01 21:21 1.0K
ASM_CASES_TAC.doc 2015-11-01 21:21 1.0K
fix.doc 2015-11-01 21:21 1.0K
REAL_RAT_LT_CONV.doc 2015-11-01 21:21 1.0K
REAL_RAT_LE_CONV.doc 2015-11-01 21:21 1.0K
REAL_RAT_GE_CONV.doc 2015-11-01 21:21 1.0K
SELECT_RULE.doc 2015-11-01 21:21 1.0K
PURE_ONCE_ASM_REWRITE_TAC.doc 2015-11-01 21:21 1.0K
list_mk_binop.doc 2015-11-01 21:21 1.0K
THENC.doc 2015-11-01 21:21 1.0K
MAP_EVERY.doc 2015-11-01 21:21 1.0K
NUM_EQ_CONV.doc 2015-11-01 21:21 1.0K
ABS_CONV.doc 2015-11-01 21:21 1.0K
GABS_CONV.doc 2015-11-01 21:21 1.0K
REAL_RAT_GT_CONV.doc 2015-11-01 21:21 1.0K
NUM_PRE_CONV.doc 2015-11-01 21:21 1.0K
LET_TAC.doc 2015-11-01 21:21 1.0K
atleast.doc 2015-11-01 21:21 1.0K
NUM_FACT_CONV.doc 2015-11-01 21:21 1.0K
ONCE_ASM_REWRITE_RULE.doc 2015-11-01 21:21 1.0K
the_specifications.doc 2015-11-01 21:21 1.0K
b.doc 2015-11-01 21:21 1.0K
WEAK_DNF_CONV.doc 2015-11-01 21:21 1.0K
REAL_INT_ABS_CONV.doc 2015-11-01 21:21 1.0K
choose.doc 2015-11-01 21:21 1.0K
meson_brand.doc 2015-11-01 21:21 1.0K
GEN.doc 2015-11-01 21:21 1.0K
r.doc 2015-11-01 21:21 1.0K
FAIL_TAC.doc 2015-11-01 21:21 1.0K
REAL_INT_MUL_CONV.doc 2015-11-01 21:21 1.0K
PURE_ONCE_REWRITE_TAC.doc 2015-11-01 21:21 1.0K
REAL_INT_SUB_CONV.doc 2015-11-01 21:21 1.0K
REAL_INT_NEG_CONV.doc 2015-11-01 21:21 1.0K
EXISTS_EQUATION.doc 2015-11-01 21:21 1.0K
REAL_INT_EQ_CONV.doc 2015-11-01 21:21 1.0K
CHOOSE_UPPERCASE.doc 2015-11-01 21:21 1.0K
.orparser.doc 2015-11-01 21:21 1.0K
meson_skew.doc 2015-11-01 21:21 1.0K
possibly.doc 2015-11-01 21:21 1.0K
REAL_INT_ADD_CONV.doc 2015-11-01 21:21 1.0K
RATOR_CONV.doc 2015-11-01 21:21 1.0K
NUM_SUC_CONV.doc 2015-11-01 21:21 1.0K
SPEC_ALL.doc 2015-11-01 21:21 1.0K
EQ_MP.doc 2015-11-01 21:21 1.0K
mk_thm.doc 2015-11-01 21:21 1.0K
list_mk_icomb.doc 2015-11-01 21:21 1.0K
EXISTS_UPPERCASE.doc 2015-11-01 21:21 1.0K
ASM_REWRITE_RULE.doc 2015-11-01 21:21 1.0K
mk_const.doc 2015-11-01 21:21 1.0K
aconv.doc 2015-11-01 21:21 1.0K
try_user_printer.doc 2015-11-01 21:21 1.0K
REWRITES_CONV.doc 2015-11-01 21:21 1.0K
.joinparsers.doc 2015-11-01 21:21 1.0K
finished.doc 2015-11-01 21:21 1.0K
deep_alpha.doc 2015-11-01 21:21 1.0K
X_META_EXISTS_TAC.doc 2015-11-01 21:21 1.0K
needs.doc 2015-11-01 21:21 972
META_SPEC_TAC.doc 2015-11-01 21:21 971
CNF_CONV.doc 2015-11-01 21:21 970
theorems.doc 2015-11-01 21:21 967
REPEATC.doc 2015-11-01 21:21 967
ONCE_SIMP_TAC.doc 2015-11-01 21:21 966
new_type.doc 2015-11-01 21:21 964
CONJ_ACI_RULE.doc 2015-11-01 21:21 964
.valmod.doc 2015-11-01 21:21 964
some.doc 2015-11-01 21:21 963
ISPECL.doc 2015-11-01 21:21 963
lhand.doc 2015-11-01 21:21 962
mk_primed_var.doc 2015-11-01 21:21 961
injectivity.doc 2015-11-01 21:21 961
meson_split_limit.doc 2015-11-01 21:21 960
MATCH_ACCEPT_TAC.doc 2015-11-01 21:21 959
definitions.doc 2015-11-01 21:21 958
INT_NEG_CONV.doc 2015-11-01 21:21 958
new_type_abbrev.doc 2015-11-01 21:21 955
ignore_constant_varstruct.doc 2015-11-01 21:21 954
RAND_CONV.doc 2015-11-01 21:21 954
INT_EQ_CONV.doc 2015-11-01 21:21 952
DEDUCT_ANTISYM_RULE.doc 2015-11-01 21:21 951
undefine.doc 2015-11-01 21:21 948
UNWIND_CONV.doc 2015-11-01 21:21 948
PURE_ASM_REWRITE_TAC.doc 2015-11-01 21:21 948
META_EXISTS_TAC.doc 2015-11-01 21:21 948
set_basic_convs.doc 2015-11-01 21:21 946
DISJ_ACI_RULE.doc 2015-11-01 21:21 945
mapf.doc 2015-11-01 21:21 944
meson_prefine.doc 2015-11-01 21:21 941
mk_mconst.doc 2015-11-01 21:21 939
ss_of_maker.doc 2015-11-01 21:21 938
REAL_INT_LT_CONV.doc 2015-11-01 21:21 938
REAL_INT_LE_CONV.doc 2015-11-01 21:21 938
nothing.doc 2015-11-01 21:21 937
NUM_EVEN_CONV.doc 2015-11-01 21:21 937
GENL.doc 2015-11-01 21:21 935
applyd.doc 2015-11-01 21:21 934
REAL_INT_GE_CONV.doc 2015-11-01 21:21 934
EVERY_CONV.doc 2015-11-01 21:21 934
PRESIMP_CONV.doc 2015-11-01 21:21 931
dest_gabs.doc 2015-11-01 21:21 930
dest_small_numeral.doc 2015-11-01 21:21 929
REAL_INT_GT_CONV.doc 2015-11-01 21:21 928
.pipeparser.doc 2015-11-01 21:21 928
ISPEC.doc 2015-11-01 21:21 927
a.doc 2015-11-01 21:21 924
NUM_ODD_CONV.doc 2015-11-01 21:21 924
INSTANTIATE_ALL.doc 2015-11-01 21:21 923
DISCH_ALL.doc 2015-11-01 21:21 922
unspaced_binops.doc 2015-11-01 21:21 921
MK_EXISTS_UPPERCASE.doc 2015-11-01 21:21 921
LAMBDA_ELIM_CONV.doc 2015-11-01 21:21 920
MK_FORALL_UPPERCASE.doc 2015-11-01 21:21 919
DNF_CONV.doc 2015-11-01 21:21 918
NUM_MULT_CONV.doc 2015-11-01 21:21 916
tryapplyd.doc 2015-11-01 21:21 911
distinctness.doc 2015-11-01 21:21 911
X_GEN_TAC.doc 2015-11-01 21:21 911
ASM_FOL_TAC.doc 2015-11-01 21:21 911
ACCEPT_TAC.doc 2015-11-01 21:21 911
loadt.doc 2015-11-01 21:21 904
PURE_REWRITE_RULE.doc 2015-11-01 21:21 904
ONCE_SIMPLIFY_CONV.doc 2015-11-01 21:21 904
NUM_TO_INT_CONV.doc 2015-11-01 21:21 904
graph.doc 2015-11-01 21:21 903
ss_of_prover.doc 2015-11-01 21:21 902
extend_rectype_net.doc 2015-11-01 21:21 902
GEN_ALPHA_CONV.doc 2015-11-01 21:21 899
EXPAND_CASES_CONV.doc 2015-11-01 21:21 899
free_in.doc 2015-11-01 21:21 898
INT_LT_CONV.doc 2015-11-01 21:21 897
file_on_path.doc 2015-11-01 21:21 895
NUM_MIN_CONV.doc 2015-11-01 21:21 890
NUM_MAX_CONV.doc 2015-11-01 21:21 890
SIMPLIFY_CONV.doc 2015-11-01 21:21 888
MONO_TAC.doc 2015-11-01 21:21 888
prebroken_binops.doc 2015-11-01 21:21 887
NUM_ADD_CONV.doc 2015-11-01 21:21 887
EVERY_ASSUM.doc 2015-11-01 21:21 887
strip_ncomb.doc 2015-11-01 21:21 880
IMP_ANTISYM_RULE.doc 2015-11-01 21:21 880
SIMPLE_CHOOSE.doc 2015-11-01 21:21 879
print_all_thm.doc 2015-11-01 21:21 876
IMP_TRANS.doc 2015-11-01 21:21 876
ALPHA_CONV.doc 2015-11-01 21:21 875
BETA_RULE.doc 2015-11-01 21:21 871
EXISTS_TAC.doc 2015-11-01 21:21 870
dest_numeral.doc 2015-11-01 21:21 868
ss_of_conv.doc 2015-11-01 21:21 864
genvar.doc 2015-11-01 21:21 861
dom.doc 2015-11-01 21:21 860
MK_DISJ_UPPERCASE.doc 2015-11-01 21:21 859
RECALL_ACCEPT_TAC.doc 2015-11-01 21:21 856
checkpoint.doc 2015-11-01 21:21 855
ONCE_REWRITE_RULE.doc 2015-11-01 21:21 855
BINDER_CONV.doc 2015-11-01 21:21 855
ss_of_thms.doc 2015-11-01 21:21 853
PURE_ASM_REWRITE_RULE.doc 2015-11-01 21:21 853
INT_ARITH.doc 2015-11-01 21:21 853
basic_prover.doc 2015-11-01 21:21 850
defined.doc 2015-11-01 21:21 848
SET_TAC.doc 2015-11-01 21:21 847
net_of_conv.doc 2015-11-01 21:21 846
term_union.doc 2015-11-01 21:21 844
SPEC_VAR.doc 2015-11-01 21:21 844
STRING_EQ_CONV.doc 2015-11-01 21:21 843
mk_setenum.doc 2015-11-01 21:21 842
REPEAT_GTCL.doc 2015-11-01 21:21 839
ss_of_congs.doc 2015-11-01 21:21 838
is_undefined.doc 2015-11-01 21:21 838
SET_RULE.doc 2015-11-01 21:21 838
string_of_thm.doc 2015-11-01 21:21 836
BETA_TAC.doc 2015-11-01 21:21 836
union_prime.doc 2015-11-01 21:21 835
unparse_as_binder.doc 2015-11-01 21:21 833
ONCE_ASM_SIMP_TAC.doc 2015-11-01 21:21 832
GSYM.doc 2015-11-01 21:21 831
MK_CONJ_UPPERCASE.doc 2015-11-01 21:21 829
EVERY.doc 2015-11-01 21:21 829
PURE_SIMP_TAC.doc 2015-11-01 21:21 828
RING_AND_IDEAL_CONV.doc 2015-11-01 21:21 825
mk_binary.doc 2015-11-01 21:21 824
list_mk_exists.doc 2015-11-01 21:21 823
EQ_IMP_RULE.doc 2015-11-01 21:21 822
remove_type_abbrev.doc 2015-11-01 21:21 821
ran.doc 2015-11-01 21:21 821
mk_fset.doc 2015-11-01 21:21 818
meson_depth.doc 2015-11-01 21:21 814
mem_prime.doc 2015-11-01 21:21 813
find_path.doc 2015-11-01 21:21 813
cases.doc 2015-11-01 21:21 812
REAL_LET_IMP.doc 2015-11-01 21:21 811
report_timing.doc 2015-11-01 21:21 810
ARITH_TAC.doc 2015-11-01 21:21 807
undefined.doc 2015-11-01 21:21 805
tysubst.doc 2015-11-01 21:21 805
RULE_ASSUM_TAC.doc 2015-11-01 21:21 805
GEN_TAC.doc 2015-11-01 21:21 803
ss_of_provers.doc 2015-11-01 21:21 802
EVERY_TCL.doc 2015-11-01 21:21 801
DISCH_TAC.doc 2015-11-01 21:21 801
REAL_INT_RAT_CONV.doc 2015-11-01 21:21 799
ONCE_REWRITE_CONV.doc 2015-11-01 21:21 797
mk_fthm.doc 2015-11-01 21:21 791
top_thm.doc 2015-11-01 21:21 790
net_of_cong.doc 2015-11-01 21:21 790
INT_POW_CONV.doc 2015-11-01 21:21 790
EXPAND_TAC.doc 2015-11-01 21:21 788
subtract_prime.doc 2015-11-01 21:21 787
ONCE_SIMP_CONV.doc 2015-11-01 21:21 782
.singlefun.doc 2015-11-01 21:21 780
print_to_string.doc 2015-11-01 21:21 778
SIMPLE_EXISTS.doc 2015-11-01 21:21 778
mk_numeral.doc 2015-11-01 21:21 776
PURE_REWRITE_CONV.doc 2015-11-01 21:21 774
ONCE_SIMP_RULE.doc 2015-11-01 21:21 774
CONJ_CANON_CONV.doc 2015-11-01 21:21 774
meson_dcutin.doc 2015-11-01 21:21 772
insert_prime.doc 2015-11-01 21:21 772
mk_icomb.doc 2015-11-01 21:21 769
hol_expand_directory.doc 2015-11-01 21:21 769
ADD_ASSUM.doc 2015-11-01 21:21 769
DISJ_CANON_CONV.doc 2015-11-01 21:21 768
parse_term.doc 2015-11-01 21:21 767
REAL_LE_IMP.doc 2015-11-01 21:21 767
SIMP_TAC.doc 2015-11-01 21:21 766
follow_path.doc 2015-11-01 21:21 764
prove.doc 2015-11-01 21:21 763
MP.doc 2015-11-01 21:21 763
loads.doc 2015-11-01 21:21 761
LE_IMP.doc 2015-11-01 21:21 759
PRENEX_CONV.doc 2015-11-01 21:21 758
parse_inductive_type_specification.doc 2015-11-01 21:21 756
mk_realintconst.doc 2015-11-01 21:21 756
BINOP_CONV.doc 2015-11-01 21:21 756
load_on_path.doc 2015-11-01 21:21 755
apply.doc 2015-11-01 21:21 755
INT_MIN_CONV.doc 2015-11-01 21:21 754
INT_MAX_CONV.doc 2015-11-01 21:21 754
prove_monotonicity_hyps.doc 2015-11-01 21:21 748
set_basic_rewrites.doc 2015-11-01 21:21 745
PURE_SIMP_RULE.doc 2015-11-01 21:21 744
GEN_ALL.doc 2015-11-01 21:21 744
retypecheck.doc 2015-11-01 21:21 742
mk_binder.doc 2015-11-01 21:21 742
freesin.doc 2015-11-01 21:21 742
rat_of_term.doc 2015-11-01 21:21 740
binops.doc 2015-11-01 21:21 740
INT_ABS_CONV.doc 2015-11-01 21:21 740
type_subst.doc 2015-11-01 21:21 739
compose_insts.doc 2015-11-01 21:21 739
SYM.doc 2015-11-01 21:21 739
mk_vartype.doc 2015-11-01 21:21 738
ASM_SIMP_TAC.doc 2015-11-01 21:21 737
funpow.doc 2015-11-01 21:21 736
GENERAL_REWRITE_CONV.doc 2015-11-01 21:21 734
PURE_ASM_SIMP_TAC.doc 2015-11-01 21:21 733
delete_user_printer.doc 2015-11-01 21:21 732
set_basic_congs.doc 2015-11-01 21:21 731
mergesort.doc 2015-11-01 21:21 731
mk_intconst.doc 2015-11-01 21:21 728
get_infix_status.doc 2015-11-01 21:21 728
mk_list.doc 2015-11-01 21:21 727
forall2.doc 2015-11-01 21:21 727
INT_MUL_CONV.doc 2015-11-01 21:21 726
axioms.doc 2015-11-01 21:21 725
INT_SUB_CONV.doc 2015-11-01 21:21 724
is_ratconst.doc 2015-11-01 21:21 722
basic_rectype_net.doc 2015-11-01 21:21 721
FIRST_TCL.doc 2015-11-01 21:21 720
unreserve_words.doc 2015-11-01 21:21 718
dest_setenum.doc 2015-11-01 21:21 718
PURE_ONCE_ASM_REWRITE_RULE.doc 2015-11-01 21:21 718
mk_type.doc 2015-11-01 21:21 717
AP_THM.doc 2015-11-01 21:21 717
INT_ADD_CONV.doc 2015-11-01 21:21 716
ALL_THEN.doc 2015-11-01 21:21 715
FIRST_CONV.doc 2015-11-01 21:21 714
types.doc 2015-11-01 21:21 713
RIGHT_BETAS.doc 2015-11-01 21:21 713
PURE_ONCE_REWRITE_RULE.doc 2015-11-01 21:21 711
strip_gabs.doc 2015-11-01 21:21 710
issymb.doc 2015-11-01 21:21 710
PURE_SIMP_CONV.doc 2015-11-01 21:21 709
list_mk_comb.doc 2015-11-01 21:21 708
term_of_preterm.doc 2015-11-01 21:21 707
strings_of_file.doc 2015-11-01 21:21 707
is_binder.doc 2015-11-01 21:21 707
shareout.doc 2015-11-01 21:21 705
rev_itlist2.doc 2015-11-01 21:21 704
is_binary.doc 2015-11-01 21:21 703
define_type_raw.doc 2015-11-01 21:21 701
splitlist.doc 2015-11-01 21:21 700
AUGMENT_SIMPSET.doc 2015-11-01 21:21 699
dest_char.doc 2015-11-01 21:21 698
empty_net.doc 2015-11-01 21:21 696
FIRST.doc 2015-11-01 21:21 696
rev_splitlist.doc 2015-11-01 21:21 695
mk_small_numeral.doc 2015-11-01 21:21 695
is_gabs.doc 2015-11-01 21:21 695
ASM_MESON_TAC.doc 2015-11-01 21:21 695
startup_banner.doc 2015-11-01 21:21 694
variants.doc 2015-11-01 21:21 691
hol_dir.doc 2015-11-01 21:21 689
ABS_TAC.doc 2015-11-01 21:21 688
term_of_rat.doc 2015-11-01 21:21 687
PURE_ONCE_REWRITE_CONV.doc 2015-11-01 21:21 687
unions_prime.doc 2015-11-01 21:21 685
parse_as_binder.doc 2015-11-01 21:21 685
basic_net.doc 2015-11-01 21:21 685
COMB2_CONV.doc 2015-11-01 21:21 685
HAS_SIZE_CONV.doc 2015-11-01 21:21 684
mapfilter.doc 2015-11-01 21:21 682
mk_let.doc 2015-11-01 21:21 681
ETA_CONV.doc 2015-11-01 21:21 681
meson_chatty.doc 2015-11-01 21:21 680
CONJUNCTS_UPPERCASE.doc 2015-11-01 21:21 680
rev_assocd.doc 2015-11-01 21:21 679
MK_BINOP_UPPERCASE.doc 2015-11-01 21:21 678
do_list.doc 2015-11-01 21:21 677
CCONTR.doc 2015-11-01 21:21 676
gcd_num.doc 2015-11-01 21:21 675
alpha.doc 2015-11-01 21:21 675
numdom.doc 2015-11-01 21:21 674
itlist2.doc 2015-11-01 21:21 674
file_of_string.doc 2015-11-01 21:21 673
AP_TERM.doc 2015-11-01 21:21 673
dest_comb.doc 2015-11-01 21:21 672
time.doc 2015-11-01 21:21 671
REMOVE_THEN.doc 2015-11-01 21:21 671
striplist.doc 2015-11-01 21:21 670
UNDISCH_THEN.doc 2015-11-01 21:21 669
ORELSEC.doc 2015-11-01 21:21 667
remark.doc 2015-11-01 21:21 665
SPEC_TAC.doc 2015-11-01 21:21 665
dest_binder.doc 2015-11-01 21:21 662
INT_LE_CONV.doc 2015-11-01 21:21 661
mk_binop.doc 2015-11-01 21:21 658
fail.doc 2015-11-01 21:21 658
assocd.doc 2015-11-01 21:21 658
increasing.doc 2015-11-01 21:21 657
INT_GE_CONV.doc 2015-11-01 21:21 657
string_of_file.doc 2015-11-01 21:21 656
intersect.doc 2015-11-01 21:21 656
NUMSEG_CONV.doc 2015-11-01 21:21 656
MP_TAC.doc 2015-11-01 21:21 656
EXISTENCE.doc 2015-11-01 21:21 656
num_of_string.doc 2015-11-01 21:21 655
unhide_constant.doc 2015-11-01 21:21 654
dest_realintconst.doc 2015-11-01 21:21 653
merge.doc 2015-11-01 21:21 652
INT_GT_CONV.doc 2015-11-01 21:21 651
term_unify.doc 2015-11-01 21:21 650
LIST_CONV.doc 2015-11-01 21:21 648
TOP_SWEEP_SQCONV.doc 2015-11-01 21:21 647
is_iff.doc 2015-11-01 21:21 646
UNDISCH_ALL.doc 2015-11-01 21:21 646
hide_constant.doc 2015-11-01 21:21 644
MK_COMB_TAC.doc 2015-11-01 21:21 644
type_vars_in_term.doc 2015-11-01 21:21 641
type_of_pretype.doc 2015-11-01 21:21 641
reserved_words.doc 2015-11-01 21:21 639
freesl.doc 2015-11-01 21:21 635
denominator.doc 2015-11-01 21:21 635
num_CONV.doc 2015-11-01 21:21 634
occurs_in.doc 2015-11-01 21:21 630
dest_fun_ty.doc 2015-11-01 21:21 630
make_args.doc 2015-11-01 21:21 624
numerator.doc 2015-11-01 21:21 623
mk_flist.doc 2015-11-01 21:21 622
CONTR.doc 2015-11-01 21:21 622
unparse_as_infix.doc 2015-11-01 21:21 621
dest_binop.doc 2015-11-01 21:21 621
ALPHA_UPPERCASE.doc 2015-11-01 21:21 621
TAC_PROOF.doc 2015-11-01 21:21 620
load_path.doc 2015-11-01 21:21 619
is_binop.doc 2015-11-01 21:21 618
CHANGED_TAC.doc 2015-11-01 21:21 617
dest_intconst.doc 2015-11-01 21:21 615
SIMP_RULE.doc 2015-11-01 21:21 614
top_goal.doc 2015-11-01 21:21 613
COMB_CONV.doc 2015-11-01 21:21 612
get_type_arity.doc 2015-11-01 21:21 610
check.doc 2015-11-01 21:21 610
REPLICATE_TAC.doc 2015-11-01 21:21 609
extend_basic_rewrites.doc 2015-11-01 21:21 608
dest_iff.doc 2015-11-01 21:21 608
prefixes.doc 2015-11-01 21:21 607
is_hidden.doc 2015-11-01 21:21 607
help_path.doc 2015-11-01 21:21 607
string_of_term.doc 2015-11-01 21:21 606
g.doc 2015-11-01 21:21 605
parse_pretype.doc 2015-11-01 21:21 604
CONTR_TAC.doc 2015-11-01 21:21 604
ONCE_DEPTH_SQCONV.doc 2015-11-01 21:21 603
parse_preterm.doc 2015-11-01 21:21 602
GEN_SIMPLIFY_CONV.doc 2015-11-01 21:21 602
find_terms.doc 2015-11-01 21:21 599
preterm_of_term.doc 2015-11-01 21:21 598
DISCH.doc 2015-11-01 21:21 598
is_realintconst.doc 2015-11-01 21:21 597
is_const.doc 2015-11-01 21:21 596
dest_binary.doc 2015-11-01 21:21 596
new_constant.doc 2015-11-01 21:21 593
dest_let.doc 2015-11-01 21:21 593
decreasing.doc 2015-11-01 21:21 593
pretype_of_type.doc 2015-11-01 21:21 590
EQ_TAC.doc 2015-11-01 21:21 590
reduce_interface.doc 2015-11-01 21:21 589
dest_type.doc 2015-11-01 21:21 589
strip_comb.doc 2015-11-01 21:21 588
ASM.doc 2015-11-01 21:21 588
mk_comb.doc 2015-11-01 21:21 587
basic_ss.doc 2015-11-01 21:21 586
ORELSE_TCL.doc 2015-11-01 21:21 586
nsplit.doc 2015-11-01 21:21 584
mk_char.doc 2015-11-01 21:21 581
list_mk_disj.doc 2015-11-01 21:21 580
binders.doc 2015-11-01 21:21 580
AP_THM_TAC.doc 2015-11-01 21:21 579
DEPTH_SQCONV.doc 2015-11-01 21:21 577
THEN_TCL.doc 2015-11-01 21:21 575
subtract.doc 2015-11-01 21:21 574
remove_interface.doc 2015-11-01 21:21 573
quotexpander.doc 2015-11-01 21:21 573
inst_goal.doc 2015-11-01 21:21 573
TOP_DEPTH_SQCONV.doc 2015-11-01 21:21 573
NOT_INTRO.doc 2015-11-01 21:21 573
union.doc 2015-11-01 21:21 572
list_mk_conj.doc 2015-11-01 21:21 571
exists.doc 2015-11-01 21:21 568
REDEPTH_SQCONV.doc 2015-11-01 21:21 567
LAND_CONV.doc 2015-11-01 21:21 565
repeat.doc 2015-11-01 21:21 564
list_mk_forall.doc 2015-11-01 21:21 564
forall.doc 2015-11-01 21:21 564
CHEAT_TAC.doc 2015-11-01 21:21 562
refine.doc 2015-11-01 21:21 559
is_intconst.doc 2015-11-01 21:21 559
index.doc 2015-11-01 21:21 559
equals_goal.doc 2015-11-01 21:21 559
USE_THEN.doc 2015-11-01 21:21 559
NOT_ELIM.doc 2015-11-01 21:21 556
thm_frees.doc 2015-11-01 21:21 554
name_of.doc 2015-11-01 21:21 553
frees.doc 2015-11-01 21:21 553
the_interface.doc 2015-11-01 21:21 552
lcm_num.doc 2015-11-01 21:21 552
insert.doc 2015-11-01 21:21 549
parses_as_binder.doc 2015-11-01 21:21 548
install_parser.doc 2015-11-01 21:21 547
set_eq.doc 2015-11-01 21:21 544
is_setenum.doc 2015-11-01 21:21 544
implode.doc 2015-11-01 21:21 544
AP_TERM_TAC.doc 2015-11-01 21:21 543
ABS.doc 2015-11-01 21:21 542
reserve_words.doc 2015-11-01 21:21 539
null_inst.doc 2015-11-01 21:21 538
try_user_parser.doc 2015-11-01 21:21 537
print_type.doc 2015-11-01 21:21 532
loaded_files.doc 2015-11-01 21:21 531
TRY_CONV.doc 2015-11-01 21:21 531
rev_assoc.doc 2015-11-01 21:21 530
list_mk_gabs.doc 2015-11-01 21:21 530
gcd.doc 2015-11-01 21:21 529
print_term.doc 2015-11-01 21:21 526
mk_iff.doc 2015-11-01 21:21 524
tryfind.doc 2015-11-01 21:21 523
is_eq.doc 2015-11-01 21:21 523
equals_thm.doc 2015-11-01 21:21 522
p.doc 2015-11-01 21:21 520
dest_imp.doc 2015-11-01 21:21 518
CONTRAPOS_CONV.doc 2015-11-01 21:21 516
subset.doc 2015-11-01 21:21 515
top_realgoal.doc 2015-11-01 21:21 513
dest_string.doc 2015-11-01 21:21 512
allpairs.doc 2015-11-01 21:21 510
partition.doc 2015-11-01 21:21 509
CONJ_PAIR.doc 2015-11-01 21:21 509
pp_print_qtype.doc 2015-11-01 21:21 505
empty_ss.doc 2015-11-01 21:21 505
pp_print_type.doc 2015-11-01 21:21 503
mk_fun_ty.doc 2015-11-01 21:21 503
unparse_as_prefix.doc 2015-11-01 21:21 502
assoc.doc 2015-11-01 21:21 502
strip_abs.doc 2015-11-01 21:21 500
flush_goalstack.doc 2015-11-01 21:21 500
ASSUME.doc 2015-11-01 21:21 499
itlist.doc 2015-11-01 21:21 498
is_type.doc 2015-11-01 21:21 493
setify.doc 2015-11-01 21:21 492
it.doc 2015-11-01 21:21 492
UNDISCH_TAC.doc 2015-11-01 21:21 492
installed_parsers.doc 2015-11-01 21:21 491
pp_print_term.doc 2015-11-01 21:21 489
null_meta.doc 2015-11-01 21:21 486
dest_cons.doc 2015-11-01 21:21 483
NO_THEN.doc 2015-11-01 21:21 483
pp_print_qterm.doc 2015-11-01 21:21 482
mk_string.doc 2015-11-01 21:21 481
string_of_type.doc 2015-11-01 21:21 480
mk_cons.doc 2015-11-01 21:21 480
delete_parser.doc 2015-11-01 21:21 480
mk_abs.doc 2015-11-01 21:21 479
BETAS_CONV.doc 2015-11-01 21:21 478
parse_type.doc 2015-11-01 21:21 477
dest_const.doc 2015-11-01 21:21 477
REFL_TAC.doc 2015-11-01 21:21 477
UNDISCH.doc 2015-11-01 21:21 476
parse_as_prefix.doc 2015-11-01 21:21 474
warn.doc 2015-11-01 21:21 473
mk_var.doc 2015-11-01 21:21 472
dest_vartype.doc 2015-11-01 21:21 472
is_vartype.doc 2015-11-01 21:21 468
CONJ_TAC.doc 2015-11-01 21:21 468
explode.doc 2015-11-01 21:21 462
current_goalstack.doc 2015-11-01 21:21 462
rator.doc 2015-11-01 21:21 459
is_reserved_word.doc 2015-11-01 21:21 459
EQF_INTRO.doc 2015-11-01 21:21 459
unions.doc 2015-11-01 21:21 458
dest_abs.doc 2015-11-01 21:21 456
print_qtype.doc 2015-11-01 21:21 454
REFL.doc 2015-11-01 21:21 454
curry.doc 2015-11-01 21:21 453
SYM_CONV.doc 2015-11-01 21:21 453
print_fpf.doc 2015-11-01 21:21 451
is_let.doc 2015-11-01 21:21 451
find_term.doc 2015-11-01 21:21 449
distinctness_store.doc 2015-11-01 21:21 449
injectivity_store.doc 2015-11-01 21:21 448
infixes.doc 2015-11-01 21:21 448
rev_itlist.doc 2015-11-01 21:21 447
end_itlist.doc 2015-11-01 21:21 447
uniq.doc 2015-11-01 21:21 445
print_qterm.doc 2015-11-01 21:21 444
isalnum.doc 2015-11-01 21:21 444
strip_exists.doc 2015-11-01 21:21 436
isbra.doc 2015-11-01 21:21 435
strip_forall.doc 2015-11-01 21:21 431
isalpha.doc 2015-11-01 21:21 431
get_const_type.doc 2015-11-01 21:21 431
find.doc 2015-11-01 21:21 431
chop_list.doc 2015-11-01 21:21 430
the_inductive_types.doc 2015-11-01 21:21 425
hyp.doc 2015-11-01 21:21 425
is_prefix.doc 2015-11-01 21:21 423
print_goalstack.doc 2015-11-01 21:21 421
concl.doc 2015-11-01 21:21 421
map2.doc 2015-11-01 21:21 420
variables.doc 2015-11-01 21:21 418
remove.doc 2015-11-01 21:21 418
EQF_ELIM.doc 2015-11-01 21:21 418
filter.doc 2015-11-01 21:21 417
DENUMERAL.doc 2015-11-01 21:21 417
bty.doc 2015-11-01 21:21 414
aty.doc 2015-11-01 21:21 414
DISJ1.doc 2015-11-01 21:21 414
list_mk_abs.doc 2015-11-01 21:21 413
dest_exists.doc 2015-11-01 21:21 413
is_comb.doc 2015-11-01 21:21 412
dest_pair.doc 2015-11-01 21:21 412
EQT_ELIM.doc 2015-11-01 21:21 412
mk_uexists.doc 2015-11-01 21:21 411
.upto.doc 2015-11-01 21:21 409
mk_exists.doc 2015-11-01 21:21 408
mk_forall.doc 2015-11-01 21:21 406
pp_print_thm.doc 2015-11-01 21:21 405
pow10.doc 2015-11-01 21:21 405
dest_forall.doc 2015-11-01 21:21 405
CONJ.doc 2015-11-01 21:21 403
is_abs.doc 2015-11-01 21:21 402
DISJ2.doc 2015-11-01 21:21 402
pow2.doc 2015-11-01 21:21 401
mk_goalstate.doc 2015-11-01 21:21 401
CONJUNCT2.doc 2015-11-01 21:21 394
ANTS_TAC.doc 2015-11-01 21:21 394
CONJUNCT1.doc 2015-11-01 21:21 393
ALL_CONV.doc 2015-11-01 21:21 392
print_goal.doc 2015-11-01 21:21 391
isspace.doc 2015-11-01 21:21 390
el.doc 2015-11-01 21:21 390
temp_path.doc 2015-11-01 21:21 389
dest_var.doc 2015-11-01 21:21 389
dest_uexists.doc 2015-11-01 21:21 387
can.doc 2015-11-01 21:21 387
num_10.doc 2015-11-01 21:21 380
is_var.doc 2015-11-01 21:21 380
print_num.doc 2015-11-01 21:21 379
num_0.doc 2015-11-01 21:21 378
issep.doc 2015-11-01 21:21 378
num_2.doc 2015-11-01 21:21 376
num_1.doc 2015-11-01 21:21 376
mk_conj.doc 2015-11-01 21:21 373
dest_cond.doc 2015-11-01 21:21 373
tyvars.doc 2015-11-01 21:21 369
is_pair.doc 2015-11-01 21:21 368
dest_select.doc 2015-11-01 21:21 365
type_abbrevs.doc 2015-11-01 21:21 362
isnum.doc 2015-11-01 21:21 361
dest_list.doc 2015-11-01 21:21 361
rotate.doc 2015-11-01 21:21 360
mk_disj.doc 2015-11-01 21:21 359
rand.doc 2015-11-01 21:21 353
print_thm.doc 2015-11-01 21:21 351
mk_imp.doc 2015-11-01 21:21 351
flat.doc 2015-11-01 21:21 351
bool_ty.doc 2015-11-01 21:21 348
report.doc 2015-11-01 21:21 346
dest_thm.doc 2015-11-01 21:21 346
map.doc 2015-11-01 21:21 345
is_uexists.doc 2015-11-01 21:21 342
use_file.doc 2015-11-01 21:21 341
dest_disj.doc 2015-11-01 21:21 341
EQT_INTRO.doc 2015-11-01 21:21 335
mk_neg.doc 2015-11-01 21:21 332
uncurry.doc 2015-11-01 21:21 323
is_numeral.doc 2015-11-01 21:21 322
by.doc 2015-11-01 21:21 322
dest_eq.doc 2015-11-01 21:21 320
hol_version.doc 2015-11-01 21:21 318
mk_cond.doc 2015-11-01 21:21 317
mem.doc 2015-11-01 21:21 314
is_cons.doc 2015-11-01 21:21 309
DISJ2_TAC.doc 2015-11-01 21:21 308
is_exists.doc 2015-11-01 21:21 307
constants.doc 2015-11-01 21:21 307
mk_pair.doc 2015-11-01 21:21 306
DISJ1_TAC.doc 2015-11-01 21:21 303
lhs.doc 2015-11-01 21:21 301
is_forall.doc 2015-11-01 21:21 301
mk_eq.doc 2015-11-01 21:21 298
bndvar.doc 2015-11-01 21:21 294
is_imp.doc 2015-11-01 21:21 288
rhs.doc 2015-11-01 21:21 287
dest_neg.doc 2015-11-01 21:21 286
replicate.doc 2015-11-01 21:21 283
is_list.doc 2015-11-01 21:21 281
is_select.doc 2015-11-01 21:21 280
body.doc 2015-11-01 21:21 280
zip.doc 2015-11-01 21:21 278
is_cond.doc 2015-11-01 21:21 278
F_F.doc 2015-11-01 21:21 277
butlast.doc 2015-11-01 21:21 269
is_disj.doc 2015-11-01 21:21 266
is_conj.doc 2015-11-01 21:21 266
is_neg.doc 2015-11-01 21:21 265
unzip.doc 2015-11-01 21:21 264
dest_conj.doc 2015-11-01 21:21 259
mk_select.doc 2015-11-01 21:21 254
exactly.doc 2015-11-01 21:21 253
tl.doc 2015-11-01 21:21 250
name.doc 2015-11-01 21:21 250
dpty.doc 2015-11-01 21:21 239
omit.doc 2015-11-01 21:21 237
C.doc 2015-11-01 21:21 225
last.doc 2015-11-01 21:21 222
hd.doc 2015-11-01 21:21 213
W.doc 2015-11-01 21:21 203
o.doc 2015-11-01 21:21 199
K.doc 2015-11-01 21:21 182
type_of.doc 2015-11-01 21:21 181
I.doc 2015-11-01 21:21 174
rev.doc 2015-11-01 21:21 172
length.doc 2015-11-01 21:21 170
NO_CONV.doc 2015-11-01 21:21 164
orelse_tcl_.doc 2015-11-01 21:21 162
then_tcl_.doc 2015-11-01 21:21 154
f_f_.doc 2015-11-01 21:21 136
thenl_.doc 2015-11-01 21:21 129
orelse_.doc 2015-11-01 21:21 128
orelsec_.doc 2015-11-01 21:21 126
then_.doc 2015-11-01 21:21 120
thenc_.doc 2015-11-01 21:21 118