isabelle: src/HOL/UNITY/ROOT.ML@1a88db6e7c7e (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
6216 05d99c0bbfa0 add_path / reset_path; wenzelm parents: 6012 diff changeset	14	add_path "../Lex"; (to find Prefix.thy)
6012 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	time_use_thy"UNITY";
fe887910e32e specifications as sets of programs paulson parents: 5638 diff changeset	17
4776 1f9362e769c1 New UNITY theory paulson parents: diff changeset	18	time_use_thy "Deadlock";
1f9362e769c1 New UNITY theory paulson parents: diff changeset	19	time_use_thy "WFair";
1f9362e769c1 New UNITY theory paulson parents: diff changeset	20	time_use_thy "Common";
1f9362e769c1 New UNITY theory paulson parents: diff changeset	21	time_use_thy "Network";
1f9362e769c1 New UNITY theory paulson parents: diff changeset	22	time_use_thy "Token";
1f9362e769c1 New UNITY theory paulson parents: diff changeset	23	time_use_thy "Channel";
1f9362e769c1 New UNITY theory paulson parents: diff changeset	24	time_use_thy "Mutex";
1f9362e769c1 New UNITY theory paulson parents: diff changeset	25	time_use_thy "FP";
1f9362e769c1 New UNITY theory paulson parents: diff changeset	26	time_use_thy "Reach";
5253 82a5ca6290aa New record type of programs paulson parents: 4776 diff changeset	27	time_use_thy "Handshake";
5357 6efb2b87610c New theory Lift paulson parents: 5253 diff changeset	28	time_use_thy "Lift";
5620 3ac11c4af76a tidying and renaming paulson parents: 5430 diff changeset	29	time_use_thy "Comp";
5648 fe887910e32e specifications as sets of programs paulson parents: 5638 diff changeset	30	time_use_thy "Client";
6295 351b3c2b0d83 removed the infernal States, eqStates, compatible, etc. paulson parents: 6216 diff changeset	31	time_use_thy "Extend";
351b3c2b0d83 removed the infernal States, eqStates, compatible, etc. paulson parents: 6216 diff changeset	32	time_use_thy "PPROD";
5430 4a179dba527a New UNITY theory, the N-S protocol paulson parents: 5357 diff changeset	33
6216 05d99c0bbfa0 add_path / reset_path; wenzelm parents: 6012 diff changeset	34	add_path "../Auth"; (to find Public.thy)
5430 4a179dba527a New UNITY theory, the N-S protocol paulson parents: 5357 diff changeset	35	use_thy"NSP_Bad";
6216 05d99c0bbfa0 add_path / reset_path; wenzelm parents: 6012 diff changeset	36
05d99c0bbfa0 add_path / reset_path; wenzelm parents: 6012 diff changeset	37	reset_path ();

author	paulson
	Wed, 03 Mar 1999 10:50:42 +0100
changeset 6299	1a88db6e7c7e
parent 6295	351b3c2b0d83
child 6349	f7750d816c21
permissions	-rw-r--r--