src/HOL/HOLCF/ROOT.ML
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 42151 4da4fc77664b
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:
42151
4da4fc77664b tuned headers;
wenzelm
parents: 41413
diff changeset
     1
(*  Title:      HOL/HOLCF/ROOT.ML
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1361
diff changeset
     2
    Author:     Franz Regensburger
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     3
16841
228d663cc9b3 use all files in HOLCF.thy;
wenzelm
parents: 16483
diff changeset
     4
HOLCF -- a semantic extension of HOL by the LCF logic.
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     5
*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     6
41413
64cd30d6b0b8 explicit file specifications -- avoid secondary load path;
wenzelm
parents: 40774
diff changeset
     7
no_document use_thys ["~~/src/HOL/Library/Nat_Bijection", "~~/src/HOL/Library/Countable"];
29921
3d50e96bcd6b fixed document
nipkow
parents: 22707
diff changeset
     8
40505
702708d26c9b reorder chapters for generated document
huffman
parents: 39982
diff changeset
     9
use_thys ["Plain_HOLCF", "Fixrec", "HOLCF"];