equal
deleted
inserted
replaced
248 end |
248 end |
249 |
249 |
250 thm rel.accpartI' |
250 thm rel.accpartI' |
251 thm rel.accpart'.induct |
251 thm rel.accpart'.induct |
252 |
252 |
253 ML{*val (result, lthy) = SimpleInductivePackage.add_inductive |
|
254 [(Binding.name "trcl'", NONE, NoSyn)] [(Binding.name "r", SOME "'a \<Rightarrow> 'a \<Rightarrow> bool", NoSyn)] |
|
255 [((Binding.name "base", []), "\<And>x. trcl' r x x"), ((Binding.name "step", []), "\<And>x y z. trcl' r x y \<Longrightarrow> r y z \<Longrightarrow> trcl' r x z")] |
|
256 (TheoryTarget.init NONE @{theory}) |
|
257 *} |
|
258 (*>*) |
253 (*>*) |
259 |
254 |
260 text {* |
255 text {* |
261 |
256 |
262 In this context, it is important to note that Isabelle distinguishes |
257 In this context, it is important to note that Isabelle distinguishes |
458 |
453 |
459 (FIXME : needs to be adjusted to new parser type) |
454 (FIXME : needs to be adjusted to new parser type) |
460 |
455 |
461 {\it |
456 {\it |
462 The whole parser for our command has type |
457 The whole parser for our command has type |
463 @{ML_text [display] "OuterLex.token list -> |
458 @{text [display] "OuterLex.token list -> |
464 (Toplevel.transition -> Toplevel.transition) * OuterLex.token list"} |
459 (Toplevel.transition -> Toplevel.transition) * OuterLex.token list"} |
465 which is abbreviated by @{ML_text OuterSyntax.parser_fn}. The new command can be added |
460 which is abbreviated by @{text OuterSyntax.parser_fn}. The new command can be added |
466 to the system via the function |
461 to the system via the function |
467 @{ML_text [display] "OuterSyntax.command : |
462 @{text [display] "OuterSyntax.command : |
468 string -> string -> OuterKeyword.T -> OuterSyntax.parser_fn -> unit"} |
463 string -> string -> OuterKeyword.T -> OuterSyntax.parser_fn -> unit"} |
469 which imperatively updates the parser table behind the scenes. } |
464 which imperatively updates the parser table behind the scenes. } |
470 |
465 |
471 In addition to the parser, this |
466 In addition to the parser, this |
472 function takes two strings representing the name of the command and a short description, |
467 function takes two strings representing the name of the command and a short description, |