--- a/src/HOL/IOA/ABP/Correctness.ML Fri Sep 08 13:23:04 1995 +0200
+++ b/src/HOL/IOA/ABP/Correctness.ML Fri Sep 08 14:52:22 1995 +0200
@@ -394,49 +394,3 @@
qed "system_refinement";
-
-(************************************************************************
- I n t e r a c t i v e A b s t r a c t i o n
-*************************************************************************)
-
-goal Correctness.thy
- "ioa_implements system_ioa system_fin_ioa";
-
-(* ------------------- Rewriting ----------------------------*)
-by (simp_tac (impl_ss addsimps [ioa_implements_def]) 1);
-by (rtac conjI 1);
-by (simp_tac (sys_ss addsimps ext_ss) 1);
-
-(* ------------------- Lemmata ------------------------------*)
-by (rtac trace_inclusion 1);
-by (rtac system_refinement 4);
-
-(* -------------------- Rewriting ---------------------------*)
-by (ALLGOALS (simp_tac impl_ss));
-by (simp_tac (sys_ss addsimps ext_ss) 1);
-
-qed"interactive_abstraction";
-
-
-
-
-
-(***********************************************************************
- Illustrative ISABELLE Examples
-************************************************************************)
-
-(*** Cantor's Theorem: There is no surjection from a set to its powerset. ***)
-
-goal Set.thy
- "~ (? f:: 'a=>'a set. ! S. ? x. f(x) = S)";
-
-by (best_tac (set_cs addSEs [equalityCE]) 1);
-qed "cantor1";
-
-(***** Theorem 2 *)
-val prems = goalw Lfp.thy [image_def] "inj(f) ==> Inv(f)``(f``X) = X";
-by (cut_facts_tac prems 1);
-by (rtac equalityI 1);
-by (fast_tac (set_cs addEs [Inv_f_f RS ssubst]) 1);
-by (fast_tac (set_cs addEs [Inv_f_f RS ssubst]) 1);
-qed "inv_image_comp";
\ No newline at end of file