Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/ZF/Coind/Dynamic.thy
changeset 76213 e44d86131648
parent 46822 95f1e700b712 
--- a/src/ZF/Coind/Dynamic.thy	Tue Sep 27 13:34:54 2022 +0200
+++ b/src/ZF/Coind/Dynamic.thy	Tue Sep 27 16:51:35 2022 +0100
@@ -11,28 +11,28 @@
   domains "EvalRel" \<subseteq> "ValEnv * Exp * Val"
   intros
     eval_constI:
-      " [| ve \<in> ValEnv; c \<in> Const |] ==>   
+      " \<lbrakk>ve \<in> ValEnv; c \<in> Const\<rbrakk> \<Longrightarrow>   
        <ve,e_const(c),v_const(c)>:EvalRel"
     eval_varI:
-      " [| ve \<in> ValEnv; x \<in> ExVar; x \<in> ve_dom(ve) |] ==>   
+      " \<lbrakk>ve \<in> ValEnv; x \<in> ExVar; x \<in> ve_dom(ve)\<rbrakk> \<Longrightarrow>   
        <ve,e_var(x),ve_app(ve,x)>:EvalRel" 
     eval_fnI:
-      " [| ve \<in> ValEnv; x \<in> ExVar; e \<in> Exp |] ==>   
+      " \<lbrakk>ve \<in> ValEnv; x \<in> ExVar; e \<in> Exp\<rbrakk> \<Longrightarrow>   
        <ve,e_fn(x,e),v_clos(x,e,ve)>:EvalRel "  
     eval_fixI:
-      " [| ve \<in> ValEnv; x \<in> ExVar; e \<in> Exp; f \<in> ExVar; cl \<in> Val;   
-          v_clos(x,e,ve_owr(ve,f,cl))=cl |] ==>   
+      " \<lbrakk>ve \<in> ValEnv; x \<in> ExVar; e \<in> Exp; f \<in> ExVar; cl \<in> Val;   
+          v_clos(x,e,ve_owr(ve,f,cl))=cl\<rbrakk> \<Longrightarrow>   
        <ve,e_fix(f,x,e),cl>:EvalRel " 
     eval_appI1:
-      " [| ve \<in> ValEnv; e1 \<in> Exp; e2 \<in> Exp; c1 \<in> Const; c2 \<in> Const;   
+      " \<lbrakk>ve \<in> ValEnv; e1 \<in> Exp; e2 \<in> Exp; c1 \<in> Const; c2 \<in> Const;   
           <ve,e1,v_const(c1)>:EvalRel;   
-          <ve,e2,v_const(c2)>:EvalRel |] ==>   
+          <ve,e2,v_const(c2)>:EvalRel\<rbrakk> \<Longrightarrow>   
        <ve,e_app(e1,e2),v_const(c_app(c1,c2))>:EvalRel "
     eval_appI2:
-      " [| ve \<in> ValEnv; vem \<in> ValEnv; e1 \<in> Exp; e2 \<in> Exp; em \<in> Exp; xm \<in> ExVar; v \<in> Val;   
+      " \<lbrakk>ve \<in> ValEnv; vem \<in> ValEnv; e1 \<in> Exp; e2 \<in> Exp; em \<in> Exp; xm \<in> ExVar; v \<in> Val;   
           <ve,e1,v_clos(xm,em,vem)>:EvalRel;   
           <ve,e2,v2>:EvalRel;   
-          <ve_owr(vem,xm,v2),em,v>:EvalRel |] ==>   
+          <ve_owr(vem,xm,v2),em,v>:EvalRel\<rbrakk> \<Longrightarrow>   
        <ve,e_app(e1,e2),v>:EvalRel "
   type_intros c_appI ve_appI ve_empI ve_owrI Exp.intros Val_ValEnv.intros
isabelle