split IOA/ROOT.ML into two files for ABP and NTP
authorclasohm
Mon Sep 11 12:38:20 1995 +0200 (1995-09-11)
changeset 1253131f72e2cd56
parent 1252 27130da22f52
child 1254 a28e04685adc
split IOA/ROOT.ML into two files for ABP and NTP
src/HOL/IOA/ROOT.ML
src/HOL/IOA/ROOT_ABP.ML
src/HOL/IOA/ROOT_NTP.ML
src/HOL/Makefile
     1.1 --- a/src/HOL/IOA/ROOT.ML	Fri Sep 08 14:52:22 1995 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,37 +0,0 @@
     1.4 -(*  Title:      HOL/IOA/ROOT.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Tobias Nipkow & Konrad Slind
     1.7 -    Copyright   1994  TU Muenchen
     1.8 -
     1.9 -This is the ROOT file for the theory of I/O-Automata.
    1.10 -The formalization is by a semantic model of I/O-Automata.
    1.11 -For details see
    1.12 -
    1.13 -@inproceedings{Nipkow-Slind-IOA,
    1.14 -author={Tobias Nipkow and Konrad Slind},
    1.15 -title={{I/O} Automata in {Isabelle/HOL}},
    1.16 -booktitle={Proc.\ TYPES Workshop 1994},
    1.17 -publisher=Springer,
    1.18 -series=LNCS,
    1.19 -note={To appear}}
    1.20 -ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz
    1.21 -
    1.22 -and
    1.23 -
    1.24 -@inproceedings{Mueller-Nipkow,
    1.25 -author={Olaf M\"uller and Tobias Nipkow},
    1.26 -title={Combining Model Checking and Deduction for {I/O}-Automata},
    1.27 -booktitle={Proc.\ TACAS Workshop},
    1.28 -organization={Aarhus University, BRICS report},
    1.29 -year=1995}
    1.30 -ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz
    1.31 -
    1.32 -Should be executed in the subdirectory HOL.
    1.33 -*)
    1.34 -goals_limit := 1;
    1.35 -
    1.36 -loadpath := ["IOA/meta_theory","IOA/NTP"];
    1.37 -use_thy "Correctness";
    1.38 -
    1.39 -loadpath := ["IOA/meta_theory","IOA/ABP"];
    1.40 -use_thy "Correctness";
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/IOA/ROOT_ABP.ML	Mon Sep 11 12:38:20 1995 +0200
     2.3 @@ -0,0 +1,34 @@
     2.4 +(*  Title:      HOL/IOA/ROOT_ABP.ML
     2.5 +    ID:         $Id$
     2.6 +    Author:     Tobias Nipkow & Konrad Slind
     2.7 +    Copyright   1994  TU Muenchen
     2.8 +
     2.9 +This is the ROOT file for the theory of I/O-Automata (ABP subdirectory).
    2.10 +The formalization is by a semantic model of I/O-Automata.
    2.11 +For details see
    2.12 +
    2.13 +@inproceedings{Nipkow-Slind-IOA,
    2.14 +author={Tobias Nipkow and Konrad Slind},
    2.15 +title={{I/O} Automata in {Isabelle/HOL}},
    2.16 +booktitle={Proc.\ TYPES Workshop 1994},
    2.17 +publisher=Springer,
    2.18 +series=LNCS,
    2.19 +note={To appear}}
    2.20 +ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz
    2.21 +
    2.22 +and
    2.23 +
    2.24 +@inproceedings{Mueller-Nipkow,
    2.25 +author={Olaf M\"uller and Tobias Nipkow},
    2.26 +title={Combining Model Checking and Deduction for {I/O}-Automata},
    2.27 +booktitle={Proc.\ TACAS Workshop},
    2.28 +organization={Aarhus University, BRICS report},
    2.29 +year=1995}
    2.30 +ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz
    2.31 +
    2.32 +Should be executed in the subdirectory HOL.
    2.33 +*)
    2.34 +goals_limit := 1;
    2.35 +
    2.36 +loadpath := ["IOA/meta_theory","IOA/ABP"];
    2.37 +use_thy "Correctness";
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/IOA/ROOT_NTP.ML	Mon Sep 11 12:38:20 1995 +0200
     3.3 @@ -0,0 +1,34 @@
     3.4 +(*  Title:      HOL/IOA/ROOT_NTP.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     Tobias Nipkow & Konrad Slind
     3.7 +    Copyright   1994  TU Muenchen
     3.8 +
     3.9 +This is the ROOT file for the theory of I/O-Automata (NTP subdirectory).
    3.10 +The formalization is by a semantic model of I/O-Automata.
    3.11 +For details see
    3.12 +
    3.13 +@inproceedings{Nipkow-Slind-IOA,
    3.14 +author={Tobias Nipkow and Konrad Slind},
    3.15 +title={{I/O} Automata in {Isabelle/HOL}},
    3.16 +booktitle={Proc.\ TYPES Workshop 1994},
    3.17 +publisher=Springer,
    3.18 +series=LNCS,
    3.19 +note={To appear}}
    3.20 +ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz
    3.21 +
    3.22 +and
    3.23 +
    3.24 +@inproceedings{Mueller-Nipkow,
    3.25 +author={Olaf M\"uller and Tobias Nipkow},
    3.26 +title={Combining Model Checking and Deduction for {I/O}-Automata},
    3.27 +booktitle={Proc.\ TACAS Workshop},
    3.28 +organization={Aarhus University, BRICS report},
    3.29 +year=1995}
    3.30 +ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz
    3.31 +
    3.32 +Should be executed in the subdirectory HOL.
    3.33 +*)
    3.34 +goals_limit := 1;
    3.35 +
    3.36 +loadpath := ["IOA/meta_theory","IOA/NTP"];
    3.37 +use_thy "Correctness";
     4.1 --- a/src/HOL/Makefile	Fri Sep 08 14:52:22 1995 +0200
     4.2 +++ b/src/HOL/Makefile	Mon Sep 11 12:38:20 1995 +0200
     4.3 @@ -87,7 +87,8 @@
     4.4   $(IOA_MT_NAMES:%=IOA/meta_theory/%.thy) $(IOA_MT_NAMES:%=IOA/meta_theory/%.ML)
     4.5  
     4.6  IOA:    $(BIN)/HOL  $(IOA_FILES)
     4.7 -	echo 'exit_use"IOA/ROOT.ML";quit();' | $(LOGIC)
     4.8 +	echo 'exit_use"IOA/ROOT_NTP.ML";quit();' | $(LOGIC)
     4.9 +	echo 'exit_use"IOA/ROOT_ABP.ML";quit();' | $(LOGIC)
    4.10  
    4.11  ##Properties of substitutions
    4.12  SUBST_NAMES = AList Setplus Subst Unifier UTerm UTLemmas