src/HOL/Decision_Procs/MIR.thy
changeset 38795 848be46708dc
parent 38786 e46e7a9cb622
child 41413 64cd30d6b0b8
     1.1 --- a/src/HOL/Decision_Procs/MIR.thy	Fri Aug 27 10:55:20 2010 +0200
     1.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Fri Aug 27 10:56:46 2010 +0200
     1.3 @@ -5837,9 +5837,9 @@
     1.4        @{code Dvd} (HOLogic.dest_numeral t1, num_of_term vs t2)
     1.5    | fm_of_term vs (@{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t1 $ t2) =
     1.6        @{code Iff} (fm_of_term vs t1, fm_of_term vs t2)
     1.7 -  | fm_of_term vs (@{term "op &"} $ t1 $ t2) =
     1.8 +  | fm_of_term vs (@{term HOL.conj} $ t1 $ t2) =
     1.9        @{code And} (fm_of_term vs t1, fm_of_term vs t2)
    1.10 -  | fm_of_term vs (@{term "op |"} $ t1 $ t2) =
    1.11 +  | fm_of_term vs (@{term HOL.disj} $ t1 $ t2) =
    1.12        @{code Or} (fm_of_term vs t1, fm_of_term vs t2)
    1.13    | fm_of_term vs (@{term HOL.implies} $ t1 $ t2) =
    1.14        @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)