src/HOL/Computational_Algebra/Computational_Algebra.thy
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 65417 fc41a5650fb1
child 66276 acc3b7dd0b21
permissions -rw-r--r--
executable domain membership checks
haftmann@65417
     1
haftmann@65417
     2
section \<open>Pieces of computational Algebra\<close>
haftmann@65417
     3
haftmann@65417
     4
theory Computational_Algebra
haftmann@65417
     5
imports
haftmann@65417
     6
  Euclidean_Algorithm
haftmann@65417
     7
  Factorial_Ring
haftmann@65417
     8
  Formal_Power_Series
haftmann@65417
     9
  Fraction_Field
haftmann@65417
    10
  Fundamental_Theorem_Algebra
haftmann@65417
    11
  Normalized_Fraction
haftmann@65417
    12
  Polynomial_FPS
haftmann@65417
    13
  Polynomial
haftmann@65417
    14
  Primes
haftmann@65417
    15
begin
haftmann@65417
    16
haftmann@65417
    17
end
haftmann@65417
    18