src/HOL/Datatype.thy
changeset 21060 bc1fa6f47ced
parent 21046 fe1db2f991a7
child 21079 747d716e98d0
     1.1 --- a/src/HOL/Datatype.thy	Fri Oct 20 10:44:36 2006 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Fri Oct 20 10:44:37 2006 +0200
     1.3 @@ -731,7 +731,7 @@
     1.4    "is_none None = True"
     1.5    "is_none (Some x) = False"
     1.6  
     1.7 -lemma is_none_none [code inline]:
     1.8 +lemma is_none_none [code inline, symmetric, normal post]:
     1.9      "(x = None) = (is_none x)" 
    1.10    by (cases x) simp_all
    1.11