equal
deleted
inserted
replaced
400 else |
400 else |
401 (do clj \<leftarrow> get_clause a j; |
401 (do clj \<leftarrow> get_clause a j; |
402 res_thm' l cli clj |
402 res_thm' l cli clj |
403 done))" |
403 done))" |
404 |
404 |
|
405 primrec |
|
406 foldM :: "('a \<Rightarrow> 'b \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b Heap" |
|
407 where |
|
408 "foldM f [] s = return s" |
|
409 | "foldM f (x#xs) s = f x s \<guillemotright>= foldM f xs" |
|
410 |
405 fun doProofStep2 :: "Clause option array \<Rightarrow> ProofStep \<Rightarrow> Clause list \<Rightarrow> Clause list Heap" |
411 fun doProofStep2 :: "Clause option array \<Rightarrow> ProofStep \<Rightarrow> Clause list \<Rightarrow> Clause list Heap" |
406 where |
412 where |
407 "doProofStep2 a (Conflict saveTo (i, rs)) rcs = |
413 "doProofStep2 a (Conflict saveTo (i, rs)) rcs = |
408 (do |
414 (do |
409 cli \<leftarrow> get_clause a i; |
415 cli \<leftarrow> get_clause a i; |