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

author	wenzelm
	Fri, 27 Aug 1999 18:59:27 +0200
changeset 7380	2bcee6a460d8
parent 7240	a509730e424b
child 7513	879ae27f5e6f
permissions	-rw-r--r--