Skip to content

Commit

Permalink
Move the congruent semantics correspondence theory to proofs/
Browse files Browse the repository at this point in the history
  • Loading branch information
agomezl committed Jan 3, 2018
1 parent d02f59a commit bf7b0cf
Showing 1 changed file with 1 addition and 1 deletion.
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ open preamble

open semBakeryTheory semCongBakeryTheory astBakeryTheory

val _ = new_theory "semProof";
val _ = new_theory "congProof";

(* semBakery$label to semCongBakery$label conversion *)
val toCong_def = Define`
Expand Down

0 comments on commit bf7b0cf

Please sign in to comment.