src/HOL/Statespace/ROOT.ML
changeset 48722 a5e3ba7cbb2a
parent 48721 866f6d5baf4c
child 48723 0829e958f0aa
equal deleted inserted replaced
48721:866f6d5baf4c 48722:a5e3ba7cbb2a
     1 use_thys ["StateSpaceEx"];