src/HOLCF/IOA/meta_theory/ioa_package.ML
changeset 10203 746eb6791aed
parent 9317 7a72952ca068
child 12339 f0b62ad4e1a6
equal deleted inserted replaced
10202:9e8b4bebc940 10203:746eb6791aed
   225 if (chead mem inp) then
   225 if (chead mem inp) then
   226 (
   226 (
   227 error("Input action " ^ tr ^ " was not specified")
   227 error("Input action " ^ tr ^ " was not specified")
   228 ) else (
   228 ) else (
   229 if (chead mem (out@int)) then
   229 if (chead mem (out@int)) then
   230 (writeln("Action " ^ tr ^ " was completedly disabled due to missing specification")) else print("");
   230 (writeln("Action " ^ tr ^ " was completedly disabled due to missing specification")) else ();
   231 (tr ^ " => False",tr ^ " => False")) |
   231 (tr ^ " => False",tr ^ " => False")) |
   232 write_alt thy (chead,ctrm) inp out int ((a,b,c,d,e)::r) =
   232 write_alt thy (chead,ctrm) inp out int ((a,b,c,d,e)::r) =
   233 let
   233 let
   234 fun hd_of (Const(a,_)) = a |
   234 fun hd_of (Const(a,_)) = a |
   235 hd_of (t $ _) = hd_of t |
   235 hd_of (t $ _) = hd_of t |