equal
deleted
inserted
replaced
119 fun myfoldr f [x] = x |
119 fun myfoldr f [x] = x |
120 | myfoldr f (x::xs) = f (x,myfoldr f xs) |
120 | myfoldr f (x::xs) = f (x,myfoldr f xs) |
121 | myfoldr f [] = error "SpecificationPackage.process_spec internal error" |
121 | myfoldr f [] = error "SpecificationPackage.process_spec internal error" |
122 |
122 |
123 val rew_imps = alt_props |> |
123 val rew_imps = alt_props |> |
124 map (ObjectLogic.atomize_cterm o Thm.read_cterm thy o rpair Term.propT o snd) |
124 map (ObjectLogic.atomize o Thm.read_cterm thy o rpair Term.propT o snd) |
125 val props' = rew_imps |> |
125 val props' = rew_imps |> |
126 map (HOLogic.dest_Trueprop o term_of o snd o Thm.dest_equals o cprop_of) |
126 map (HOLogic.dest_Trueprop o term_of o snd o Thm.dest_equals o cprop_of) |
127 |
127 |
128 fun proc_single prop = |
128 fun proc_single prop = |
129 let |
129 let |