equal
deleted
inserted
replaced
1 theory Ind_Interface |
1 theory Ind_Interface |
2 imports Ind_Intro Simple_Inductive_Package |
2 imports Ind_Intro Simple_Inductive_Package |
|
3 keywords "simple_inductive2" :: thy_decl |
3 begin |
4 begin |
4 |
5 |
5 section {* Parsing and Typing the Specification\label{sec:interface} *} |
6 section {* Parsing and Typing the Specification\label{sec:interface} *} |
6 |
7 |
7 text_raw {* |
8 text_raw {* |
131 fun add_inductive pred_specs rule_specs lthy = lthy*}(*>*) |
132 fun add_inductive pred_specs rule_specs lthy = lthy*}(*>*) |
132 ML_val %linenosgray{*val specification : (local_theory -> local_theory) parser = |
133 ML_val %linenosgray{*val specification : (local_theory -> local_theory) parser = |
133 spec_parser >> |
134 spec_parser >> |
134 (fn (pred_specs, rule_specs) => add_inductive_cmd pred_specs rule_specs) |
135 (fn (pred_specs, rule_specs) => add_inductive_cmd pred_specs rule_specs) |
135 |
136 |
136 val _ = Outer_Syntax.local_theory "simple_inductive2" |
137 val _ = Outer_Syntax.local_theory ("simple_inductive2", Keyword.thy_decl) |
137 "definition of simple inductive predicates" |
138 "definition of simple inductive predicates" |
138 Keyword.thy_decl specification*} |
139 specification*} |
139 |
140 |
140 text {* |
141 text {* |
141 We call @{ML_ind local_theory in Outer_Syntax} with the kind-indicator |
142 We call @{ML_ind local_theory in Outer_Syntax} with the kind-indicator |
142 @{ML_ind thy_decl in Keyword} since the package does not need to open |
143 @{ML_ind thy_decl in Keyword} since the package does not need to open |
143 up any proof (see Section~\ref{sec:newcommand}). |
144 up any proof (see Section~\ref{sec:newcommand}). |