equal
deleted
inserted
replaced
1 (* Title: HOL/Tools/induct_attrib.ML |
1 (* Title: Pure/Isar/induct_attrib.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Markus Wenzel, TU Muenchen |
3 Author: Markus Wenzel, TU Muenchen |
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
5 |
5 |
6 Declaration of rules for cases and induction. |
6 Declaration of rules for cases and induction. |
57 fun print_rules kind sg rs = |
57 fun print_rules kind sg rs = |
58 let val thms = map snd (NetRules.rules rs) |
58 let val thms = map snd (NetRules.rules rs) |
59 in Pretty.writeln (Pretty.big_list kind (map (Display.pretty_thm_sg sg) thms)) end; |
59 in Pretty.writeln (Pretty.big_list kind (map (Display.pretty_thm_sg sg) thms)) end; |
60 |
60 |
61 |
61 |
62 (* theory data kind 'HOL/induction' *) |
62 (* theory data kind 'Isar/induction' *) |
63 |
63 |
64 structure GlobalInductArgs = |
64 structure GlobalInductArgs = |
65 struct |
65 struct |
66 val name = "HOL/induction"; |
66 val name = "Isar/induction"; |
67 type T = (rules * rules) * (rules * rules); |
67 type T = (rules * rules) * (rules * rules); |
68 |
68 |
69 val empty = ((type_rules, set_rules), (type_rules, set_rules)); |
69 val empty = ((type_rules, set_rules), (type_rules, set_rules)); |
70 val copy = I; |
70 val copy = I; |
71 val prep_ext = I; |
71 val prep_ext = I; |
90 structure GlobalInduct = TheoryDataFun(GlobalInductArgs); |
90 structure GlobalInduct = TheoryDataFun(GlobalInductArgs); |
91 val print_global_rules = GlobalInduct.print; |
91 val print_global_rules = GlobalInduct.print; |
92 val dest_global_rules = GlobalInductArgs.dest o GlobalInduct.get; |
92 val dest_global_rules = GlobalInductArgs.dest o GlobalInduct.get; |
93 |
93 |
94 |
94 |
95 (* proof data kind 'HOL/induction' *) |
95 (* proof data kind 'Isar/induction' *) |
96 |
96 |
97 structure LocalInductArgs = |
97 structure LocalInductArgs = |
98 struct |
98 struct |
99 val name = "HOL/induction"; |
99 val name = "Isar/induction"; |
100 type T = GlobalInductArgs.T; |
100 type T = GlobalInductArgs.T; |
101 |
101 |
102 fun init thy = GlobalInduct.get thy; |
102 fun init thy = GlobalInduct.get thy; |
103 fun print x = GlobalInductArgs.print (ProofContext.sign_of x); |
103 fun print x = GlobalInductArgs.print (ProofContext.sign_of x); |
104 end; |
104 end; |