src/HOL/TLA/Memory/ProcedureInterface.ML

-(* 
+(*
     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, 
+val Procedure_defs = [caller_def, rtrner_def, Calling_def,
                       Call_def, Return_def,
-		      PLegalCaller_def, LegalCaller_def,
-		      PLegalReturner_def, LegalReturner_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";