forked from afp-mirror/Core_DOM
Deleted unused exceptions.
This commit is contained in:
parent
0bbda09de8
commit
cebefb53dc
|
@ -36,9 +36,8 @@ theory BaseMonad
|
|||
begin
|
||||
subsection\<open>Datatypes\<close>
|
||||
|
||||
datatype exception = NotFoundError | SegmentationFault | HierarchyRequestError | AssertException
|
||||
| NonTerminationException | InvokeError | TypeError | DebugException nat | NotSupportedError
|
||||
| InvalidStateError
|
||||
datatype exception = NotFoundError | HierarchyRequestError | NotSupportedError | SegmentationFault
|
||||
| AssertException | NonTerminationException | InvokeError | TypeError
|
||||
|
||||
lemma finite_set_in [simp]: "x \<in> fset FS \<longleftrightarrow> x |\<in>| FS"
|
||||
by (meson notin_fset)
|
||||
|
|
Reference in New Issue