# HG changeset patch
# User mueller
# Date 810564742 -7200
# Node ID 27130da22f52dddea2fe9a2d7f6748c8b927e1c3
# Parent  81fc4d8e3eda2c2877fb11a69477f80e25eeae20
*** empty log message ***

diff -r 81fc4d8e3eda -r 27130da22f52 src/HOL/IOA/ABP/Correctness.ML
--- 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