isabelle: src/HOL/UNITY/ROOT.ML@0d334465f29a (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
6349 f7750d816c21 removed foo_build_completed -- now handled by session management (via usedir); wenzelm parents: 6299 diff changeset	9	writeln"Root file for HOL/UNITY";
4776 1f9362e769c1 New UNITY theory paulson parents: diff changeset	10
1f9362e769c1 New UNITY theory paulson parents: diff changeset	11	set proof_timing;
5648 fe887910e32e specifications as sets of programs paulson parents: 5638 diff changeset	12
6216 05d99c0bbfa0 add_path / reset_path; wenzelm parents: 6012 diff changeset	13	add_path "../Lex"; (to find Prefix.thy)
6012 1894bfc4aee9 Addition of the States component; parts of Comp not working paulson parents: 5899 diff changeset	14
5648 fe887910e32e specifications as sets of programs paulson parents: 5638 diff changeset	15	time_use_thy"UNITY";
fe887910e32e specifications as sets of programs paulson parents: 5638 diff changeset	16
4776 1f9362e769c1 New UNITY theory paulson parents: diff changeset	17	time_use_thy "Deadlock";
1f9362e769c1 New UNITY theory paulson parents: diff changeset	18	time_use_thy "WFair";
1f9362e769c1 New UNITY theory paulson parents: diff changeset	19	time_use_thy "Common";
1f9362e769c1 New UNITY theory paulson parents: diff changeset	20	time_use_thy "Network";
1f9362e769c1 New UNITY theory paulson parents: diff changeset	21	time_use_thy "Token";
1f9362e769c1 New UNITY theory paulson parents: diff changeset	22	time_use_thy "Channel";
1f9362e769c1 New UNITY theory paulson parents: diff changeset	23	time_use_thy "Mutex";
1f9362e769c1 New UNITY theory paulson parents: diff changeset	24	time_use_thy "FP";
1f9362e769c1 New UNITY theory paulson parents: diff changeset	25	time_use_thy "Reach";
5253 82a5ca6290aa New record type of programs paulson parents: 4776 diff changeset	26	time_use_thy "Handshake";
5357 6efb2b87610c New theory Lift paulson parents: 5253 diff changeset	27	time_use_thy "Lift";
5620 3ac11c4af76a tidying and renaming paulson parents: 5430 diff changeset	28	time_use_thy "Comp";
5648 fe887910e32e specifications as sets of programs paulson parents: 5638 diff changeset	29	time_use_thy "Client";
6295 351b3c2b0d83 removed the infernal States, eqStates, compatible, etc. paulson parents: 6216 diff changeset	30	time_use_thy "Extend";
351b3c2b0d83 removed the infernal States, eqStates, compatible, etc. paulson parents: 6216 diff changeset	31	time_use_thy "PPROD";
5430 4a179dba527a New UNITY theory, the N-S protocol paulson parents: 5357 diff changeset	32
6216 05d99c0bbfa0 add_path / reset_path; wenzelm parents: 6012 diff changeset	33	add_path "../Auth"; (to find Public.thy)
5430 4a179dba527a New UNITY theory, the N-S protocol paulson parents: 5357 diff changeset	34	use_thy"NSP_Bad";
6216 05d99c0bbfa0 add_path / reset_path; wenzelm parents: 6012 diff changeset	35
05d99c0bbfa0 add_path / reset_path; wenzelm parents: 6012 diff changeset	36	reset_path ();

author	wenzelm
	Thu, 22 Apr 1999 15:03:50 +0200
changeset 6485	0d334465f29a
parent 6349	f7750d816c21
child 6536	281d44905cab
permissions	-rw-r--r--