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