src/HOL/Plain.thy
author huffman
Mon Jan 12 12:09:54 2009 -0800 (2009-01-12)
changeset 29460 ad87e5d1488b
parent 29304 5c71a6da989d
child 29609 a010aab5bed0
permissions -rw-r--r--
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
haftmann@27368
     1
header {* Plain HOL *}
haftmann@27368
     2
haftmann@27368
     3
theory Plain
haftmann@27368
     4
imports Datatype FunDef Record SAT Extraction
haftmann@27368
     5
begin
haftmann@27368
     6
wenzelm@29304
     7
text {*
wenzelm@29304
     8
  Plain bootstrap of fundamental HOL tools and packages; does not
wenzelm@29304
     9
  include @{text Hilbert_Choice}.
wenzelm@29304
    10
*}
wenzelm@29304
    11
haftmann@27368
    12
ML {* path_add "~~/src/HOL/Library" *}
haftmann@27368
    13
haftmann@27368
    14
end