| changeset 37872 | d83659570337 |
| parent 32491 | d5d8bea0cd94 |
| child 38273 | d31a34569542 |
--- a/src/HOL/Matrix/ComputeHOL.thy Wed Jul 21 15:31:38 2010 +0200 +++ b/src/HOL/Matrix/ComputeHOL.thy Wed Jul 21 15:44:36 2010 +0200 @@ -1,5 +1,5 @@ theory ComputeHOL -imports Complex_Main "~~/src/Tools/Compute_Oracle/Compute_Oracle" +imports Complex_Main "Compute_Oracle/Compute_Oracle" begin lemma Trueprop_eq_eq: "Trueprop X == (X == True)" by (simp add: atomize_eq)