equal
deleted
inserted
replaced
53 (fn prems=> |
53 (fn prems=> |
54 [ (REPEAT (resolve_tac (prems@[ProdE]) 1)) ]); |
54 [ (REPEAT (resolve_tac (prems@[ProdE]) 1)) ]); |
55 |
55 |
56 (** Tactics for type checking **) |
56 (** Tactics for type checking **) |
57 |
57 |
58 fun is_rigid_elem (Const("Elem",_) $ a $ _) = not (is_Var (head_of a)) |
58 fun is_rigid_elem (Const("CTT.Elem",_) $ a $ _) = not (is_Var (head_of a)) |
59 | is_rigid_elem _ = false; |
59 | is_rigid_elem _ = false; |
60 |
60 |
61 (*Try solving a:A by assumption provided a is rigid!*) |
61 (*Try solving a:A by assumption provided a is rigid!*) |
62 val test_assume_tac = SUBGOAL(fn (prem,i) => |
62 val test_assume_tac = SUBGOAL(fn (prem,i) => |
63 if is_rigid_elem (Logic.strip_assums_concl prem) |
63 if is_rigid_elem (Logic.strip_assums_concl prem) |