equal
deleted
inserted
replaced
1031 fast_tac HOL_cs 1]) |
1031 fast_tac HOL_cs 1]) |
1032 take_lemmas; |
1032 take_lemmas; |
1033 in pg [] goal (K tacs) end; |
1033 in pg [] goal (K tacs) end; |
1034 end; (* local *) |
1034 end; (* local *) |
1035 |
1035 |
1036 val inducts = ProjectRule.projections (ProofContext.init thy) ind; |
1036 val inducts = Project_Rule.projections (ProofContext.init thy) ind; |
1037 fun ind_rule (dname, rule) = ((Binding.empty, [rule]), [Induct.induct_type dname]); |
1037 fun ind_rule (dname, rule) = ((Binding.empty, [rule]), [Induct.induct_type dname]); |
1038 val induct_failed = (Thm.prop_of ind = Thm.prop_of TrueI); |
1038 val induct_failed = (Thm.prop_of ind = Thm.prop_of TrueI); |
1039 |
1039 |
1040 in thy |> Sign.add_path comp_dnam |
1040 in thy |> Sign.add_path comp_dnam |
1041 |> snd o PureThy.add_thmss [ |
1041 |> snd o PureThy.add_thmss [ |