equal
deleted
inserted
replaced
1 theory ComputeHOL |
1 theory ComputeHOL |
2 imports Main "~~/src/Tools/Compute_Oracle/Compute_Oracle" |
2 imports Main "~~/src/Tools/Compute_Oracle/Compute_Oracle" |
3 begin |
3 begin |
4 |
4 |
5 lemma Trueprop_eq_eq: "Trueprop X == (X == True)" by (simp add: atomize_eq) |
5 lemma Trueprop_eq_eq: "Trueprop X == (X == True)" by (simp add: atomize_eq) |
6 lemma meta_eq_trivial: "x == y \<Longrightarrow> x == y" by simp |
6 lemma meta_eq_trivial: "x == y \<Longrightarrow> x == y" by simp |