src/HOL/Induct/ROOT.ML
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 39616 8052101883c3
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
39616
8052101883c3 renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents: 35247
diff changeset
     1
Unsynchronized.setmp quick_and_dirty true
33615
261abc2e3155 uniform use of simultabeous use_thys;
wenzelm
parents: 28827
diff changeset
     2
  use_thys ["Common_Patterns"];
24607
fc06b84acd81 added Induct/Common_Patterns.thy;
wenzelm
parents: 24104
diff changeset
     3
35247
0831bd85eee5 moved reduced Induct/SList back from AFP.
nipkow
parents: 33688
diff changeset
     4
use_thys ["QuoDataType", "QuoNestedDataType", "Term", "SList",
33688
1a97dcd8dc6a moved old SList, LList, LFilter to AFP/Lazy-Lists-II;
wenzelm
parents: 33615
diff changeset
     5
  "ABexp", "Tree", "Ordinals", "Sigma_Algebra", "Comb", "PropLog", "Com"];