--- a/src/HOLCF/IOA/meta_theory/Seq.thy Wed Jun 07 01:51:22 2006 +0200
+++ b/src/HOLCF/IOA/meta_theory/Seq.thy Wed Jun 07 01:59:17 2006 +0200
@@ -114,27 +114,10 @@
sfinite_0: "nil:sfinite"
sfinite_n: "[|tr:sfinite;a~=UU|] ==> (a##tr) : sfinite"
-ML {* use_legacy_bindings (the_context ()) *}
-ML {*
-structure seq =
-struct
- open seq
- val injects = [injects]
- val inverts = [inverts]
- val finites = [finites]
- val take_lemmas = [take_lemmas]
-end
-structure sfinite =
-struct
- open sfinite
- val elim = elims
- val elims = [elims]
-end
-*}
-
declare sfinite.intros [simp]
declare seq.rews [simp]
+
subsection {* recursive equations of operators *}
subsubsection {* smap *}
@@ -508,6 +491,4 @@
apply simp
done
-ML {* use_legacy_bindings (the_context ()) *}
-
end