equal
deleted
inserted
replaced
121 |
121 |
122 val ctrans: thm |
122 val ctrans: thm |
123 val o_apply: thm |
123 val o_apply: thm |
124 val set_mp: thm |
124 val set_mp: thm |
125 val set_rev_mp: thm |
125 val set_rev_mp: thm |
|
126 val subset_UNIV: thm |
126 val Pair_eqD: thm |
127 val Pair_eqD: thm |
127 val Pair_eqI: thm |
128 val Pair_eqI: thm |
128 val mk_sym: thm -> thm |
129 val mk_sym: thm -> thm |
129 val mk_trans: thm -> thm -> thm |
130 val mk_trans: thm -> thm -> thm |
130 val mk_unabs_def: int -> thm -> thm |
131 val mk_unabs_def: int -> thm -> thm |
522 (*TODO: antiquote heavily used theorems once*) |
523 (*TODO: antiquote heavily used theorems once*) |
523 val ctrans = @{thm ordLeq_transitive}; |
524 val ctrans = @{thm ordLeq_transitive}; |
524 val o_apply = @{thm o_apply}; |
525 val o_apply = @{thm o_apply}; |
525 val set_mp = @{thm set_mp}; |
526 val set_mp = @{thm set_mp}; |
526 val set_rev_mp = @{thm set_rev_mp}; |
527 val set_rev_mp = @{thm set_rev_mp}; |
|
528 val subset_UNIV = @{thm subset_UNIV}; |
527 val Pair_eqD = @{thm iffD1[OF Pair_eq]}; |
529 val Pair_eqD = @{thm iffD1[OF Pair_eq]}; |
528 val Pair_eqI = @{thm iffD2[OF Pair_eq]}; |
530 val Pair_eqI = @{thm iffD2[OF Pair_eq]}; |
529 |
531 |
530 fun mk_nthN 1 t 1 = t |
532 fun mk_nthN 1 t 1 = t |
531 | mk_nthN _ t 1 = HOLogic.mk_fst t |
533 | mk_nthN _ t 1 = HOLogic.mk_fst t |