Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
eliminated Bali.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 9b19cbb0af28;
authorwenzelm
Sun, 13 Mar 2011 23:12:38 +0100
changeset 41960 8a399da4cde1
parent 41959 b460124855b8
child 41961 fdd37cfcd4a3
eliminated Bali.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 9b19cbb0af28;
src/HOL/Bali/Bali.thy file | annotate | diff | comparison | revisions
src/HOL/Bali/ROOT.ML file | annotate | diff | comparison | revisions
src/HOL/IsaMakefile file | annotate | diff | comparison | revisions 
--- a/src/HOL/Bali/Bali.thy	Sun Mar 13 22:55:50 2011 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-(*  Author:     David von Oheimb
-    Copyright   1999 Technische Universitaet Muenchen
-*)
-
-header {* The Hoare logic for Bali. *}
-
-theory Bali
-imports AxExample AxSound AxCompl Trans
-begin
-
-end
--- a/src/HOL/Bali/ROOT.ML	Sun Mar 13 22:55:50 2011 +0100
+++ b/src/HOL/Bali/ROOT.ML	Sun Mar 13 23:12:38 2011 +0100
@@ -1,1 +1,1 @@
-use_thys ["Bali"];
+use_thys ["AxExample", "AxSound", "AxCompl", "Trans"];
--- a/src/HOL/IsaMakefile	Sun Mar 13 22:55:50 2011 +0100
+++ b/src/HOL/IsaMakefile	Sun Mar 13 23:12:38 2011 +0100
@@ -992,15 +992,14 @@
 
 HOL-Bali: HOL $(LOG)/HOL-Bali.gz
 
-$(LOG)/HOL-Bali.gz: $(OUT)/HOL Bali/Bali.thy Bali/AxCompl.thy		\
-  Bali/AxExample.thy Bali/AxSem.thy Bali/AxSound.thy Bali/Basis.thy	\
-  Bali/Conform.thy Bali/Decl.thy Bali/DeclConcepts.thy Bali/Eval.thy	\
-  Bali/Evaln.thy Bali/Example.thy Bali/Name.thy Bali/ROOT.ML		\
-  Bali/State.thy Bali/Table.thy Bali/Term.thy Bali/Trans.thy		\
-  Bali/Type.thy Bali/TypeRel.thy Bali/TypeSafe.thy Bali/Value.thy	\
-  Bali/WellForm.thy Bali/DefiniteAssignment.thy				\
-  Bali/DefiniteAssignmentCorrect.thy Bali/WellType.thy			\
-  Bali/document/root.tex
+$(LOG)/HOL-Bali.gz: $(OUT)/HOL Bali/AxCompl.thy Bali/AxExample.thy	\
+  Bali/AxSem.thy Bali/AxSound.thy Bali/Basis.thy Bali/Conform.thy	\
+  Bali/Decl.thy Bali/DeclConcepts.thy Bali/Eval.thy Bali/Evaln.thy	\
+  Bali/Example.thy Bali/Name.thy Bali/ROOT.ML Bali/State.thy		\
+  Bali/Table.thy Bali/Term.thy Bali/Trans.thy Bali/Type.thy		\
+  Bali/TypeRel.thy Bali/TypeSafe.thy Bali/Value.thy Bali/WellForm.thy	\
+  Bali/DefiniteAssignment.thy Bali/DefiniteAssignmentCorrect.thy	\
+  Bali/WellType.thy Bali/document/root.tex
 	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Bali
isabelle