src/HOL/Combinatorics/Combinatorics.thy
author haftmann
Sun, 09 May 2021 05:48:50 +0000
changeset 73648 1bd3463e30b8
parent 73623 5020054b3a16
permissions -rw-r--r--
more elementary swap
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
73477
1d8a79aa2a99 dedicated session for combinatorial material
haftmann
parents:
diff changeset
     1
1d8a79aa2a99 dedicated session for combinatorial material
haftmann
parents:
diff changeset
     2
section \<open>Basic combinatorics in Isabelle/HOL (and the Archive of Formal Proofs)\<close>
1d8a79aa2a99 dedicated session for combinatorial material
haftmann
parents:
diff changeset
     3
1d8a79aa2a99 dedicated session for combinatorial material
haftmann
parents:
diff changeset
     4
theory Combinatorics
1d8a79aa2a99 dedicated session for combinatorial material
haftmann
parents:
diff changeset
     5
imports
73623
5020054b3a16 tuned theory structure
haftmann
parents: 73622
diff changeset
     6
  Transposition
73477
1d8a79aa2a99 dedicated session for combinatorial material
haftmann
parents:
diff changeset
     7
  Stirling
1d8a79aa2a99 dedicated session for combinatorial material
haftmann
parents:
diff changeset
     8
  Permutations
1d8a79aa2a99 dedicated session for combinatorial material
haftmann
parents:
diff changeset
     9
  List_Permutation
1d8a79aa2a99 dedicated session for combinatorial material
haftmann
parents:
diff changeset
    10
  Multiset_Permutations
1d8a79aa2a99 dedicated session for combinatorial material
haftmann
parents:
diff changeset
    11
  Cycles
73622
4dc3baf45d6a more appropriate location
haftmann
parents: 73477
diff changeset
    12
  Perm
73648
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    13
  Orbits
73477
1d8a79aa2a99 dedicated session for combinatorial material
haftmann
parents:
diff changeset
    14
begin
1d8a79aa2a99 dedicated session for combinatorial material
haftmann
parents:
diff changeset
    15
1d8a79aa2a99 dedicated session for combinatorial material
haftmann
parents:
diff changeset
    16
end