remove unused syntax for as_pat, lazy_pat
authorhuffman
Mon Mar 22 22:42:34 2010 -0700 (2010-03-22)
changeset 359209ef9a20cfba1
parent 35919 676c6005ad03
child 35921 cd1b01664810
remove unused syntax for as_pat, lazy_pat
src/HOLCF/Fixrec.thy
     1.1 --- a/src/HOLCF/Fixrec.thy	Mon Mar 22 22:41:41 2010 -0700
     1.2 +++ b/src/HOLCF/Fixrec.thy	Mon Mar 22 22:42:34 2010 -0700
     1.3 @@ -419,10 +419,6 @@
     1.4  
     1.5  subsection {* Wildcards, as-patterns, and lazy patterns *}
     1.6  
     1.7 -syntax
     1.8 -  "_as_pat" :: "[idt, 'a] \<Rightarrow> 'a" (infixr "\<as>" 10)
     1.9 -  "_lazy_pat" :: "'a \<Rightarrow> 'a" ("\<lazy> _" [1000] 1000)
    1.10 -
    1.11  definition
    1.12    wild_pat :: "'a \<rightarrow> unit maybe" where
    1.13    "wild_pat = (\<Lambda> x. return\<cdot>())"
    1.14 @@ -438,24 +434,14 @@
    1.15  text {* Parse translations (patterns) *}
    1.16  translations
    1.17    "_pat _" => "CONST wild_pat"
    1.18 -  "_pat (_as_pat x y)" => "CONST as_pat (_pat y)"
    1.19 -  "_pat (_lazy_pat x)" => "CONST lazy_pat (_pat x)"
    1.20  
    1.21  text {* Parse translations (variables) *}
    1.22  translations
    1.23    "_variable _ r" => "_variable _noargs r"
    1.24 -  "_variable (_as_pat x y) r" => "_variable (_args x y) r"
    1.25 -  "_variable (_lazy_pat x) r" => "_variable x r"
    1.26  
    1.27  text {* Print translations *}
    1.28  translations
    1.29    "_" <= "_match (CONST wild_pat) _noargs"
    1.30 -  "_as_pat x (_match p v)" <= "_match (CONST as_pat p) (_args (_variable x) v)"
    1.31 -  "_lazy_pat (_match p v)" <= "_match (CONST lazy_pat p) v"
    1.32 -
    1.33 -text {* Lazy patterns in lambda abstractions *}
    1.34 -translations
    1.35 -  "_cabs (_lazy_pat p) r" == "CONST Fixrec.cases oo (_Case1 (_lazy_pat p) r)"
    1.36  
    1.37  lemma wild_pat [simp]: "branch wild_pat\<cdot>(unit_when\<cdot>r)\<cdot>x = return\<cdot>r"
    1.38  by (simp add: branch_def wild_pat_def)