--- 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)]);