equal
deleted
inserted
replaced
94 simple_inductive (in rel) |
94 simple_inductive (in rel) |
95 accpart' |
95 accpart' |
96 where |
96 where |
97 accpartI: "(\<And>y. R y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x" |
97 accpartI: "(\<And>y. R y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x" |
98 (*<*)ML %no{*fun filtered_input str = |
98 (*<*)ML %no{*fun filtered_input str = |
99 filter Token.is_proper (Outer_Syntax.scan Position.none str) |
99 filter Token.is_proper (Outer_Syntax.scan (Keyword.get_lexicons ()) Position.none str) |
100 fun parse p input = Scan.finite Token.stopper (Scan.error p) input*}(*>*) |
100 fun parse p input = Scan.finite Token.stopper (Scan.error p) input*}(*>*) |
101 text {* |
101 text {* |
102 Note that in these definitions the parameter @{text R}, standing for the |
102 Note that in these definitions the parameter @{text R}, standing for the |
103 relation, is left implicit. For the moment we will ignore this kind |
103 relation, is left implicit. For the moment we will ignore this kind |
104 of implicit parameters and rely on the fact that the infrastructure will |
104 of implicit parameters and rely on the fact that the infrastructure will |