diff -r 132634d24019 -r 8b8406ad9edd IMP/Denotation.ML
--- a/IMP/Denotation.ML	Fri Jan 19 12:49:36 1996 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-(*  Title: 	HOL/IMP/Denotation.ML
-    ID:         $Id$
-    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
-    Copyright   1994 TUM
-*)
-
-open Denotation;
-
-(**** Rewrite Rules for A,B,C ****)
-
-val A_simps =
-     [A_nat,A_loc,A_op1,A_op2];
-
-val B_simps = map (fn t => t RS eq_reflection)
-     [B_true,B_false,B_op,B_not,B_and,B_or]
-
-val C_simps = map (fn t => t RS eq_reflection)
-  [C_skip,C_assign,C_comp,C_if,C_while]; 
-
-(**** mono (Gamma(b,c)) ****)
-
-qed_goalw "Gamma_mono" Denotation.thy [mono_def,Gamma_def]
-	"mono(Gamma(b,c))"
-     (fn _ => [(best_tac comp_cs 1)]);