doc-src/IsarImplementation/Thy/locale.thy
author huffman
Sun, 24 Sep 2006 07:14:02 +0200
changeset 20694 76c49548d14c
parent 20520 05fd007bdeb9
permissions -rw-r--r--
real_norm_def [simp]
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     1
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     2
(* $Id$ *)
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     3
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     4
theory "locale" imports base begin
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     5
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     6
chapter {* Structured specifications *}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     7
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     8
section {* Specification elements *}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     9
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    10
text FIXME
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    11
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 18537
diff changeset
    12
20520
wenzelm
parents: 20477
diff changeset
    13
section {* Type-inference *}
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    14
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    15
text FIXME
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    16
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 18537
diff changeset
    17
20477
wenzelm
parents: 20451
diff changeset
    18
section {* Local theories *}
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 18537
diff changeset
    19
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 18537
diff changeset
    20
text {*
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 18537
diff changeset
    21
  FIXME
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 18537
diff changeset
    22
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 18537
diff changeset
    23
  \glossary{Local theory}{FIXME}
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 18537
diff changeset
    24
*}
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 18537
diff changeset
    25
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    26
end