isabelle: src/HOL/UNITY/ROOT.ML@9dd06eeda95c (annotated)

4776 1f9362e769c1 New UNITY theory paulson parents: diff changeset	1	(* Title: HOL/UNITY/ROOT
1f9362e769c1 New UNITY theory paulson parents: diff changeset	2	ID: $Id$
1f9362e769c1 New UNITY theory paulson parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
1f9362e769c1 New UNITY theory paulson parents: diff changeset	4	Copyright 1998 University of Cambridge
1f9362e769c1 New UNITY theory paulson parents: diff changeset	5
1f9362e769c1 New UNITY theory paulson parents: diff changeset	6	Root file for UNITY proofs.
1f9362e769c1 New UNITY theory paulson parents: diff changeset	7	*)
1f9362e769c1 New UNITY theory paulson parents: diff changeset	8
1f9362e769c1 New UNITY theory paulson parents: diff changeset	9	HOL_build_completed; (Make examples fail if HOL did)
1f9362e769c1 New UNITY theory paulson parents: diff changeset	10
1f9362e769c1 New UNITY theory paulson parents: diff changeset	11	writeln"Root file for HOL/UNITY";
1f9362e769c1 New UNITY theory paulson parents: diff changeset	12	set proof_timing;
5648 fe887910e32e specifications as sets of programs paulson parents: 5638 diff changeset	13
6012 1894bfc4aee9 Addition of the States component; parts of Comp not working paulson parents: 5899 diff changeset	14
1894bfc4aee9 Addition of the States component; parts of Comp not working paulson parents: 5899 diff changeset	15
5648 fe887910e32e specifications as sets of programs paulson parents: 5638 diff changeset	16	loadpath := "../Lex" :: !loadpath; (to find Prefix.thy)
fe887910e32e specifications as sets of programs paulson parents: 5638 diff changeset	17	time_use_thy"UNITY";
fe887910e32e specifications as sets of programs paulson parents: 5638 diff changeset	18
4776 1f9362e769c1 New UNITY theory paulson parents: diff changeset	19	time_use_thy "Deadlock";
1f9362e769c1 New UNITY theory paulson parents: diff changeset	20	time_use_thy "WFair";
1f9362e769c1 New UNITY theory paulson parents: diff changeset	21	time_use_thy "Common";
1f9362e769c1 New UNITY theory paulson parents: diff changeset	22	time_use_thy "Network";
1f9362e769c1 New UNITY theory paulson parents: diff changeset	23	time_use_thy "Token";
1f9362e769c1 New UNITY theory paulson parents: diff changeset	24	time_use_thy "Channel";
1f9362e769c1 New UNITY theory paulson parents: diff changeset	25	time_use_thy "Mutex";
1f9362e769c1 New UNITY theory paulson parents: diff changeset	26	time_use_thy "FP";
1f9362e769c1 New UNITY theory paulson parents: diff changeset	27	time_use_thy "Reach";
5253 82a5ca6290aa New record type of programs paulson parents: 4776 diff changeset	28	time_use_thy "Handshake";
5357 6efb2b87610c New theory Lift paulson parents: 5253 diff changeset	29	time_use_thy "Lift";
5620 3ac11c4af76a tidying and renaming paulson parents: 5430 diff changeset	30	time_use_thy "Comp";
5648 fe887910e32e specifications as sets of programs paulson parents: 5638 diff changeset	31	time_use_thy "Client";
6012 1894bfc4aee9 Addition of the States component; parts of Comp not working paulson parents: 5899 diff changeset	32	(**
1894bfc4aee9 Addition of the States component; parts of Comp not working paulson parents: 5899 diff changeset	33	time_use_thy "PPX";
1894bfc4aee9 Addition of the States component; parts of Comp not working paulson parents: 5899 diff changeset	34	**)
5430 4a179dba527a New UNITY theory, the N-S protocol paulson parents: 5357 diff changeset	35
5620 3ac11c4af76a tidying and renaming paulson parents: 5430 diff changeset	36	loadpath := "../Auth" :: !loadpath; (to find Public.thy)
5430 4a179dba527a New UNITY theory, the N-S protocol paulson parents: 5357 diff changeset	37	use_thy"NSP_Bad";

author	oheimb
	Fri, 11 Dec 1998 18:56:30 +0100
changeset 6027	9dd06eeda95c
parent 6012	1894bfc4aee9
child 6216	05d99c0bbfa0
permissions	-rw-r--r--