diff -r 17098171d46a -r 6f79647cf536 src/HOL/TLA/Memory/ProcedureInterface.ML
--- a/src/HOL/TLA/Memory/ProcedureInterface.ML	Fri Dec 01 17:22:33 2006 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +0,0 @@
-(*
-    File:        ProcedureInterface.ML
-    ID:          $Id$
-    Author:      Stephan Merz
-    Copyright:   1997 University of Munich
-
-    Procedure interface (theorems and proofs)
-*)
-
-Addsimps [slice_def];
-val mem_css = (claset(), simpset());
-
-(* ---------------------------------------------------------------------------- *)
-
-val Procedure_defs = [caller_def, rtrner_def, Calling_def,
-                      Call_def, Return_def,
-                      PLegalCaller_def, LegalCaller_def,
-                      PLegalReturner_def, LegalReturner_def];
-
-(* Calls and returns change their subchannel *)
-Goal "|- Call ch p v --> <Call ch p v>_((caller ch)!p)";
-by (auto_tac (mem_css addsimps2 [angle_def,Call_def,caller_def,Calling_def]));
-qed "Call_changed";
-
-Goal "|- Return ch p v --> <Return ch p v>_((rtrner ch)!p)";
-by (auto_tac (mem_css addsimps2 [angle_def,Return_def,rtrner_def,Calling_def]));
-qed "Return_changed";
-