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