Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
addition of string escapes
authorlcp
Fri, 12 Aug 1994 11:13:23 +0200
changeset 514 ab2c867829ec
parent 513 97a879e8d01b
child 515 abcc438e7c27
addition of string escapes
src/ZF/IMP/Com.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle