src/HOL/Matrix_LP/ComputeNumeral.thy
Fri, 28 Oct 2022 06:34:26 +0000 haftmann restructured
Sun, 21 Aug 2022 06:18:23 +0000 haftmann streamlined
Wed, 17 Feb 2016 21:51:57 +0100 haftmann dropped various legacy fact bindings
Tue, 17 Nov 2015 12:32:08 +0000 paulson Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
Tue, 10 Nov 2015 14:18:41 +0000 paulson Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
Thu, 13 Aug 2015 15:22:11 +0200 haftmann qualified adjust_*
less more (0) -6 tip