equal
deleted
inserted
replaced
23 let |
23 let |
24 fun conv env p = |
24 fun conv env p = |
25 case (term_of p) of |
25 case (term_of p) of |
26 Const(s,T)$_$_ => |
26 Const(s,T)$_$_ => |
27 if domain_type T = HOLogic.boolT |
27 if domain_type T = HOLogic.boolT |
28 andalso member (op =) [@{const_name "op &"}, @{const_name "op |"}, |
28 andalso member (op =) [@{const_name HOL.conj}, @{const_name HOL.disj}, |
29 @{const_name HOL.implies}, @{const_name "op ="}] s |
29 @{const_name HOL.implies}, @{const_name "op ="}] s |
30 then binop_conv (conv env) p |
30 then binop_conv (conv env) p |
31 else atcv env p |
31 else atcv env p |
32 | Const(@{const_name Not},_)$_ => arg_conv (conv env) p |
32 | Const(@{const_name Not},_)$_ => arg_conv (conv env) p |
33 | Const(@{const_name Ex},_)$Abs(s,_,_) => |
33 | Const(@{const_name Ex},_)$Abs(s,_,_) => |