equal
deleted
inserted
replaced
124 | myfoldr f [] = error "SpecificationPackage.process_spec internal error" |
124 | myfoldr f [] = error "SpecificationPackage.process_spec internal error" |
125 |
125 |
126 fun typ_equiv t u = Sign.typ_instance thy (t,u) andalso Sign.typ_instance thy (u,t); |
126 fun typ_equiv t u = Sign.typ_instance thy (t,u) andalso Sign.typ_instance thy (u,t); |
127 |
127 |
128 val rew_imps = alt_props |> |
128 val rew_imps = alt_props |> |
129 map (ObjectLogic.atomize_cterm thy o Thm.read_cterm thy o rpair Term.propT o snd) |
129 map (ObjectLogic.atomize_cterm o Thm.read_cterm thy o rpair Term.propT o snd) |
130 val props' = rew_imps |> |
130 val props' = rew_imps |> |
131 map (HOLogic.dest_Trueprop o term_of o snd o dest_equals o cprop_of) |
131 map (HOLogic.dest_Trueprop o term_of o snd o dest_equals o cprop_of) |
132 |
132 |
133 fun proc_single prop = |
133 fun proc_single prop = |
134 let |
134 let |