equal
deleted
inserted
replaced
109 fun myfoldr f [x] = x |
109 fun myfoldr f [x] = x |
110 | myfoldr f (x::xs) = f (x,myfoldr f xs) |
110 | myfoldr f (x::xs) = f (x,myfoldr f xs) |
111 | myfoldr f [] = error "Choice_Specification.process_spec internal error" |
111 | myfoldr f [] = error "Choice_Specification.process_spec internal error" |
112 |
112 |
113 val rew_imps = alt_props |> |
113 val rew_imps = alt_props |> |
114 map (ObjectLogic.atomize o Thm.cterm_of thy o Syntax.read_prop_global thy o snd) |
114 map (Object_Logic.atomize o Thm.cterm_of thy o Syntax.read_prop_global thy o snd) |
115 val props' = rew_imps |> |
115 val props' = rew_imps |> |
116 map (HOLogic.dest_Trueprop o term_of o snd o Thm.dest_equals o cprop_of) |
116 map (HOLogic.dest_Trueprop o term_of o snd o Thm.dest_equals o cprop_of) |
117 |
117 |
118 fun proc_single prop = |
118 fun proc_single prop = |
119 let |
119 let |