isabelle: src/HOLCF/IMP/ROOT.ML@6a422b22ba02 (annotated)

2798 f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	1	(* Title: HOLCF/IMP/ROOT.ML
f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	2	ID: $Id$
f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	3	Author: Tobias Nipkow
f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	4	Copyright 1997 TU Muenchen
f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	5	*)
f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	6
f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	7	(*Load theories from ../meta_theory without generating HTML files
f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	8	(has already been done by HOL/IMP/ROOT.ML)*)
f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	9	val old_make_html = !make_html;
f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	10	make_html := false;
f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	11	loadpath := ["../../HOL/IMP"];
f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	12
f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	13	use_thy "Natural";
f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	14
f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	15	make_html := old_make_html;
f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	16	loadpath := ["."];
f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	17
3663 e2d1e1151314 Loads HoareEx now. nipkow parents: 2798 diff changeset	18	use_thy "HoareEx";

author	wenzelm
	Sun, 25 Oct 1998 12:33:27 +0100
changeset 5769	6a422b22ba02
parent 5210	54aaa779b6b4
child 6217	9dac1ee185e3
permissions	-rw-r--r--