equal
deleted
inserted
replaced
84 end |
84 end |
85 in |
85 in |
86 map instantiate rew_ths |
86 map instantiate rew_ths |
87 end |
87 end |
88 |
88 |
89 fun is_compound ((Const ("Not", _)) $ t) = |
89 fun is_compound ((Const (@{const_name "Not"}, _)) $ t) = |
90 error "is_compound: Negation should not occur; preprocessing is defect" |
90 error "is_compound: Negation should not occur; preprocessing is defect" |
91 | is_compound ((Const ("Ex", _)) $ _) = true |
91 | is_compound ((Const (@{const_name "Ex"}, _)) $ _) = true |
92 | is_compound ((Const (@{const_name "op |"}, _)) $ _ $ _) = true |
92 | is_compound ((Const (@{const_name "op |"}, _)) $ _ $ _) = true |
93 | is_compound ((Const ("op &", _)) $ _ $ _) = |
93 | is_compound ((Const (@{const_name "op &"}, _)) $ _ $ _) = |
94 error "is_compound: Conjunction should not occur; preprocessing is defect" |
94 error "is_compound: Conjunction should not occur; preprocessing is defect" |
95 | is_compound _ = false |
95 | is_compound _ = false |
96 |
96 |
97 fun flatten constname atom (defs, thy) = |
97 fun flatten constname atom (defs, thy) = |
98 if is_compound atom then |
98 if is_compound atom then |