| author | huffman |
| Sun, 19 Feb 2006 02:11:27 +0100 | |
| changeset 19105 | 3aabd46340e0 |
| parent 17923 | 18c66ca0c776 |
| child 23152 | 9497234a2743 |
| permissions | -rw-r--r-- |
| clasohm@1479 | 1 |
(* Title: HOLCF/HOLCF.thy |
| nipkow@243 | 2 |
ID: $Id$ |
| clasohm@1479 | 3 |
Author: Franz Regensburger |
| nipkow@243 | 4 |
|
| wenzelm@16841 | 5 |
HOLCF -- a semantic extension of HOL by the LCF logic. |
| nipkow@243 | 6 |
*) |
| nipkow@243 | 7 |
|
| huffman@15650 | 8 |
theory HOLCF |
| huffman@19105 | 9 |
imports Sprod Ssum Up Lift Discrete One Tr Domain Main |
| wenzelm@16841 | 10 |
uses |
| wenzelm@16841 | 11 |
"holcf_logic.ML" |
| wenzelm@16841 | 12 |
"cont_consts.ML" |
| wenzelm@16841 | 13 |
"domain/library.ML" |
| wenzelm@16841 | 14 |
"domain/syntax.ML" |
| wenzelm@16841 | 15 |
"domain/axioms.ML" |
| wenzelm@16841 | 16 |
"domain/theorems.ML" |
| wenzelm@16841 | 17 |
"domain/extender.ML" |
| wenzelm@16841 | 18 |
"adm_tac.ML" |
| wenzelm@16841 | 19 |
|
| huffman@15650 | 20 |
begin |
| huffman@15650 | 21 |
|
| wenzelm@16841 | 22 |
ML_setup {*
|
| wenzelm@17876 | 23 |
change_simpset (fn simpset => simpset addSolver |
| wenzelm@17612 | 24 |
(mk_solver' "adm_tac" (fn ss => |
| wenzelm@17876 | 25 |
adm_tac (cut_facts_tac (Simplifier.prems_of_ss ss) THEN' cont_tacRs ss)))); |
| wenzelm@16841 | 26 |
*} |
| wenzelm@16841 | 27 |
|
| huffman@15650 | 28 |
end |