395 (True, table) |
395 (True, table) |
396 | aux (Const (@{const_name False}, _)) table = |
396 | aux (Const (@{const_name False}, _)) table = |
397 (False, table) |
397 (False, table) |
398 | aux (Const (@{const_name Not}, _) $ x) table = |
398 | aux (Const (@{const_name Not}, _) $ x) table = |
399 apfst Not (aux x table) |
399 apfst Not (aux x table) |
400 | aux (Const (@{const_name "op |"}, _) $ x $ y) table = |
400 | aux (Const (@{const_name HOL.disj}, _) $ x $ y) table = |
401 let |
401 let |
402 val (fm1, table1) = aux x table |
402 val (fm1, table1) = aux x table |
403 val (fm2, table2) = aux y table1 |
403 val (fm2, table2) = aux y table1 |
404 in |
404 in |
405 (Or (fm1, fm2), table2) |
405 (Or (fm1, fm2), table2) |
406 end |
406 end |
407 | aux (Const (@{const_name "op &"}, _) $ x $ y) table = |
407 | aux (Const (@{const_name HOL.conj}, _) $ x $ y) table = |
408 let |
408 let |
409 val (fm1, table1) = aux x table |
409 val (fm1, table1) = aux x table |
410 val (fm2, table2) = aux y table1 |
410 val (fm2, table2) = aux y table1 |
411 in |
411 in |
412 (And (fm1, fm2), table2) |
412 (And (fm1, fm2), table2) |