equal
deleted
inserted
replaced
101 |
101 |
102 fun generalize_tac f = CSUBGOAL (fn (p, i) => PRIMITIVE (fn st => |
102 fun generalize_tac f = CSUBGOAL (fn (p, i) => PRIMITIVE (fn st => |
103 let |
103 let |
104 fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"} |
104 fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"} |
105 fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t) |
105 fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t) |
106 val ts = sort (fn (a,b) => Term.fast_term_ord (term_of a, term_of b)) (f p) |
106 val ts = sort (fn (a,b) => TermOrd.fast_term_ord (term_of a, term_of b)) (f p) |
107 val p' = fold_rev gen ts p |
107 val p' = fold_rev gen ts p |
108 in implies_intr p' (implies_elim st (fold forall_elim ts (assume p'))) end)); |
108 in implies_intr p' (implies_elim st (fold forall_elim ts (assume p'))) end)); |
109 |
109 |
110 local |
110 local |
111 val ss1 = comp_ss |
111 val ss1 = comp_ss |