# HG changeset patch
# User lcp
# Date 776682803 -7200
# Node ID ab2c867829ec3dcdaff7165e44a20d26647e10f9
# Parent  97a879e8d01b47b6e43a0cdae451ae8598f0d93c
addition of string escapes

diff -r 97a879e8d01b -r ab2c867829ec src/ZF/IMP/Com.thy
--- a/src/ZF/IMP/Com.thy	Fri Aug 12 11:01:18 1994 +0200
+++ b/src/ZF/IMP/Com.thy	Fri Aug 12 11:13:23 1994 +0200
@@ -70,7 +70,8 @@
     ori   "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |] \
 \	    ==> <b0 ori b1,sigma> -b-> (w0 or w1)"
 
-  type_intrs "bexp.intrs @ [apply_funtype, and_type, or_type, bool_1I, bool_0I, not_type]"
+  type_intrs "bexp.intrs @   \
+\	      [apply_funtype, and_type, or_type, bool_1I, bool_0I, not_type]"
   type_elims "[make_elim(evala.dom_subset RS subsetD)]"
 
 
@@ -123,6 +124,7 @@
 
   con_defs   "[assign_def]"
   type_intrs "bexp.intrs @ com.intrs @ [if_type,lam_type,apply_type]"
-  type_elims "[make_elim(evala.dom_subset RS subsetD), make_elim(evalb.dom_subset RS subsetD) ]"
+  type_elims "[make_elim(evala.dom_subset RS subsetD),   \
+\	      make_elim(evalb.dom_subset RS subsetD) ]"
 
 end