isabelle: src/HOL/UNITY/ROOT.ML@d4b895d3afa7 (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";
7513 879ae27f5e6f new example HOL/UNITY/TimerArray paulson parents: 7240 diff changeset	30	time_use_thy "TimerArray";
8251 9be357df93d4 New treatment of "guarantees" with polymorphic components and bijections. paulson parents: 8128 diff changeset	31	(**
8128 3a5864b465e2 still working; a bit of polishing paulson parents: 7513 diff changeset	32	time_use_thy "Alloc";
8251 9be357df93d4 New treatment of "guarantees" with polymorphic components and bijections. paulson parents: 8128 diff changeset	33	**)
5430 4a179dba527a New UNITY theory, the N-S protocol paulson parents: 5357 diff changeset	34
6216 05d99c0bbfa0 add_path / reset_path; wenzelm parents: 6012 diff changeset	35	add_path "../Auth"; (to find Public.thy)
5430 4a179dba527a New UNITY theory, the N-S protocol paulson parents: 5357 diff changeset	36	use_thy"NSP_Bad";
6216 05d99c0bbfa0 add_path / reset_path; wenzelm parents: 6012 diff changeset	37
05d99c0bbfa0 add_path / reset_path; wenzelm parents: 6012 diff changeset	38	reset_path ();

author	paulson
	Wed, 23 Feb 2000 10:45:08 +0100
changeset 8286	d4b895d3afa7
parent 8251	9be357df93d4
child 8314	463f63a9a7f2
permissions	-rw-r--r--