author  blanchet 
Tue, 13 May 2014 11:10:23 +0200  
changeset 56946  10d9bd4ea94f 
parent 54148  c8cc5ab4a863 
child 57255  488046fdda59 
permissions  rwrr 
39951
ff60a6e4edfe
factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.)  the theories now reflect the directory structure
blanchet
parents:
diff
changeset

1 
(* Title: HOL/ATP.thy 
ff60a6e4edfe
factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.)  the theories now reflect the directory structure
blanchet
parents:
diff
changeset

2 
Author: Fabian Immler, TU Muenchen 
ff60a6e4edfe
factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.)  the theories now reflect the directory structure
blanchet
parents:
diff
changeset

3 
Author: Jasmin Blanchette, TU Muenchen 
ff60a6e4edfe
factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.)  the theories now reflect the directory structure
blanchet
parents:
diff
changeset

4 
*) 
ff60a6e4edfe
factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.)  the theories now reflect the directory structure
blanchet
parents:
diff
changeset

5 

39958  6 
header {* Automatic Theorem Provers (ATPs) *} 
39951
ff60a6e4edfe
factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.)  the theories now reflect the directory structure
blanchet
parents:
diff
changeset

7 

ff60a6e4edfe
factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.)  the theories now reflect the directory structure
blanchet
parents:
diff
changeset

8 
theory ATP 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

9 
imports Meson 
39951
ff60a6e4edfe
factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.)  the theories now reflect the directory structure
blanchet
parents:
diff
changeset

10 
begin 
ff60a6e4edfe
factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.)  the theories now reflect the directory structure
blanchet
parents:
diff
changeset

11 

48891  12 
ML_file "Tools/lambda_lifting.ML" 
13 
ML_file "Tools/monomorph.ML" 

14 
ML_file "Tools/ATP/atp_util.ML" 

15 
ML_file "Tools/ATP/atp_problem.ML" 

16 
ML_file "Tools/ATP/atp_proof.ML" 

17 
ML_file "Tools/ATP/atp_proof_redirect.ML" 

18 

56946  19 

43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

20 
subsection {* Higherorder reasoning helpers *} 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

21 

54148  22 
definition fFalse :: bool where 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

23 
"fFalse \<longleftrightarrow> False" 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

24 

54148  25 
definition fTrue :: bool where 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

26 
"fTrue \<longleftrightarrow> True" 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

27 

54148  28 
definition fNot :: "bool \<Rightarrow> bool" where 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

29 
"fNot P \<longleftrightarrow> \<not> P" 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

30 

54148  31 
definition fComp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where 
47946
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

32 
"fComp P = (\<lambda>x. \<not> P x)" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

33 

54148  34 
definition fconj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

35 
"fconj P Q \<longleftrightarrow> P \<and> Q" 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

36 

54148  37 
definition fdisj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

38 
"fdisj P Q \<longleftrightarrow> P \<or> Q" 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

39 

54148  40 
definition fimplies :: "bool \<Rightarrow> bool \<Rightarrow> bool" where 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

41 
"fimplies P Q \<longleftrightarrow> (P \<longrightarrow> Q)" 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

42 

54148  43 
definition fAll :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where 
43678  44 
"fAll P \<longleftrightarrow> All P" 
45 

54148  46 
definition fEx :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where 
43678  47 
"fEx P \<longleftrightarrow> Ex P" 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

48 

56946  49 
definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where 
50 
"fequal x y \<longleftrightarrow> (x = y)" 

51 

47946
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

52 
lemma fTrue_ne_fFalse: "fFalse \<noteq> fTrue" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

53 
unfolding fFalse_def fTrue_def by simp 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

54 

33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

55 
lemma fNot_table: 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

56 
"fNot fFalse = fTrue" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

57 
"fNot fTrue = fFalse" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

58 
unfolding fFalse_def fTrue_def fNot_def by auto 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

59 

33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

60 
lemma fconj_table: 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

61 
"fconj fFalse P = fFalse" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

62 
"fconj P fFalse = fFalse" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

63 
"fconj fTrue fTrue = fTrue" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

64 
unfolding fFalse_def fTrue_def fconj_def by auto 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

65 

33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

66 
lemma fdisj_table: 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

67 
"fdisj fTrue P = fTrue" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

68 
"fdisj P fTrue = fTrue" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

69 
"fdisj fFalse fFalse = fFalse" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

70 
unfolding fFalse_def fTrue_def fdisj_def by auto 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

71 

33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

72 
lemma fimplies_table: 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

73 
"fimplies P fTrue = fTrue" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

74 
"fimplies fFalse P = fTrue" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

75 
"fimplies fTrue fFalse = fFalse" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

76 
unfolding fFalse_def fTrue_def fimplies_def by auto 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

77 

33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

78 
lemma fAll_table: 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

79 
"Ex (fComp P) \<or> fAll P = fTrue" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

80 
"All P \<or> fAll P = fFalse" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

81 
unfolding fFalse_def fTrue_def fComp_def fAll_def by auto 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

82 

33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

83 
lemma fEx_table: 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

84 
"All (fComp P) \<or> fEx P = fTrue" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

85 
"Ex P \<or> fEx P = fFalse" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

86 
unfolding fFalse_def fTrue_def fComp_def fEx_def by auto 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

87 

56946  88 
lemma fequal_table: 
89 
"fequal x x = fTrue" 

90 
"x = y \<or> fequal x y = fFalse" 

91 
unfolding fFalse_def fTrue_def fequal_def by auto 

92 

47946
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

93 
lemma fNot_law: 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

94 
"fNot P \<noteq> P" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

95 
unfolding fNot_def by auto 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

96 

33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

97 
lemma fComp_law: 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

98 
"fComp P x \<longleftrightarrow> \<not> P x" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

99 
unfolding fComp_def .. 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

100 

33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

101 
lemma fconj_laws: 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

102 
"fconj P P \<longleftrightarrow> P" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

103 
"fconj P Q \<longleftrightarrow> fconj Q P" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

104 
"fNot (fconj P Q) \<longleftrightarrow> fdisj (fNot P) (fNot Q)" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

105 
unfolding fNot_def fconj_def fdisj_def by auto 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

106 

33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

107 
lemma fdisj_laws: 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

108 
"fdisj P P \<longleftrightarrow> P" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

109 
"fdisj P Q \<longleftrightarrow> fdisj Q P" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

110 
"fNot (fdisj P Q) \<longleftrightarrow> fconj (fNot P) (fNot Q)" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

111 
unfolding fNot_def fconj_def fdisj_def by auto 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

112 

33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

113 
lemma fimplies_laws: 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

114 
"fimplies P Q \<longleftrightarrow> fdisj (\<not> P) Q" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

115 
"fNot (fimplies P Q) \<longleftrightarrow> fconj P (fNot Q)" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

116 
unfolding fNot_def fconj_def fdisj_def fimplies_def by auto 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

117 

33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

118 
lemma fAll_law: 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

119 
"fNot (fAll R) \<longleftrightarrow> fEx (fComp R)" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

120 
unfolding fNot_def fComp_def fAll_def fEx_def by auto 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

121 

33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

122 
lemma fEx_law: 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

123 
"fNot (fEx R) \<longleftrightarrow> fAll (fComp R)" 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

124 
unfolding fNot_def fComp_def fAll_def fEx_def by auto 
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
46320
diff
changeset

125 

56946  126 
lemma fequal_laws: 
127 
"fequal x y = fequal y x" 

128 
"fequal x y = fFalse \<or> fequal y z = fFalse \<or> fequal x z = fTrue" 

129 
"fequal x y = fFalse \<or> fequal (f x) (f y) = fTrue" 

130 
unfolding fFalse_def fTrue_def fequal_def by auto 

131 

132 

43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

133 
subsection {* Setup *} 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

134 

48891  135 
ML_file "Tools/ATP/atp_problem_generate.ML" 
136 
ML_file "Tools/ATP/atp_proof_reconstruct.ML" 

137 
ML_file "Tools/ATP/atp_systems.ML" 

43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
40178
diff
changeset

138 

39951
ff60a6e4edfe
factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.)  the theories now reflect the directory structure
blanchet
parents:
diff
changeset

139 
setup ATP_Systems.setup 
ff60a6e4edfe
factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.)  the theories now reflect the directory structure
blanchet
parents:
diff
changeset

140 

ff60a6e4edfe
factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.)  the theories now reflect the directory structure
blanchet
parents:
diff
changeset

141 
end 