equal
deleted
inserted
replaced
65 let fun get ls (Const ("op |",_) $ o1 $ o2) = |
65 let fun get ls (Const ("op |",_) $ o1 $ o2) = |
66 case o2 of |
66 case o2 of |
67 Const ("op |",_) $ _ $ _ => get (ls @ [o1]) o2 |
67 Const ("op |",_) $ _ $ _ => get (ls @ [o1]) o2 |
68 | _ => ls @ [o1, o2] |
68 | _ => ls @ [o1, o2] |
69 in (((list2isalist bool) o (get [])) ors) |
69 in (((list2isalist bool) o (get [])) ors) |
70 handle _ => raise error ("or2list: no ORs= "^(term2str ors)) end |
70 handle _ => error ("or2list: no ORs= "^(term2str ors)) end |
71 ); |
71 ); |
72 (*>val t = HOLogic.true_const; |
72 (*>val t = HOLogic.true_const; |
73 > val t' = or2list t; |
73 > val t' = or2list t; |
74 > term2str t'; |
74 > term2str t'; |
75 "Atools.UniversalList" |
75 "Atools.UniversalList" |