Hoare.ML -> hoare.ML
authorkleing
Sat Nov 09 00:12:25 2002 +0100 (2002-11-09)
changeset 13703a36a0d417133
parent 13702 c7cf8fa66534
child 13704 854501b1e957
Hoare.ML -> hoare.ML
src/HOL/IsaMakefile
src/HOL/Isar_examples/Hoare.thy
     1.1 --- a/src/HOL/IsaMakefile	Fri Nov 08 10:34:40 2002 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Sat Nov 09 00:12:25 2002 +0100
     1.3 @@ -627,7 +627,7 @@
     1.4    Isar_examples/Puzzle.thy Isar_examples/Summation.thy \
     1.5    Isar_examples/ROOT.ML Isar_examples/document/proof.sty \
     1.6    Isar_examples/document/root.bib Isar_examples/document/root.tex \
     1.7 -  Isar_examples/document/style.tex Hoare/Hoare.ML
     1.8 +  Isar_examples/document/style.tex Hoare/hoare.ML
     1.9  	@$(ISATOOL) usedir $(OUT)/HOL Isar_examples
    1.10  
    1.11  
     2.1 --- a/src/HOL/Isar_examples/Hoare.thy	Fri Nov 08 10:34:40 2002 +0100
     2.2 +++ b/src/HOL/Isar_examples/Hoare.thy	Sat Nov 09 00:12:25 2002 +0100
     2.3 @@ -8,7 +8,7 @@
     2.4  header {* Hoare Logic *}
     2.5  
     2.6  theory Hoare = Main
     2.7 -files ("~~/src/HOL/Hoare/Hoare.ML"):
     2.8 +files ("~~/src/HOL/Hoare/hoare.ML"):
     2.9  
    2.10  subsection {* Abstract syntax and semantics *}
    2.11  
    2.12 @@ -411,11 +411,11 @@
    2.13  *}
    2.14  
    2.15  ML {* val Valid_def = thm "Valid_def" *}
    2.16 -use "~~/src/HOL/Hoare/Hoare.ML"
    2.17 +use "~~/src/HOL/Hoare/hoare.ML"
    2.18  
    2.19  method_setup hoare = {*
    2.20    Method.no_args
    2.21      (Method.SIMPLE_METHOD' HEADGOAL (hoare_tac (K all_tac))) *}
    2.22    "verification condition generator for Hoare logic"
    2.23  
    2.24 -end
    2.25 \ No newline at end of file
    2.26 +end