equal
deleted
inserted
replaced
894 Rules need to be classified as @{attribute (Pure) intro}, |
894 Rules need to be classified as @{attribute (Pure) intro}, |
895 @{attribute (Pure) elim}, or @{attribute (Pure) dest}; here the |
895 @{attribute (Pure) elim}, or @{attribute (Pure) dest}; here the |
896 ``@{text "!"}'' indicator refers to ``safe'' rules, which may be |
896 ``@{text "!"}'' indicator refers to ``safe'' rules, which may be |
897 applied aggressively (without considering back-tracking later). |
897 applied aggressively (without considering back-tracking later). |
898 Rules declared with ``@{text "?"}'' are ignored in proof search (the |
898 Rules declared with ``@{text "?"}'' are ignored in proof search (the |
899 single-step @{method rule} method still observes these). An |
899 single-step @{method (Pure) rule} method still observes these). An |
900 explicit weight annotation may be given as well; otherwise the |
900 explicit weight annotation may be given as well; otherwise the |
901 number of rule premises will be taken into account here. |
901 number of rule premises will be taken into account here. |
902 *} |
902 *} |
903 |
903 |
904 |
904 |
1417 \begin{matharray}{rcl} |
1417 \begin{matharray}{rcl} |
1418 @{command_def (HOL) "code_module"} & : & @{text "theory \<rightarrow> theory"} \\ |
1418 @{command_def (HOL) "code_module"} & : & @{text "theory \<rightarrow> theory"} \\ |
1419 @{command_def (HOL) "code_library"} & : & @{text "theory \<rightarrow> theory"} \\ |
1419 @{command_def (HOL) "code_library"} & : & @{text "theory \<rightarrow> theory"} \\ |
1420 @{command_def (HOL) "consts_code"} & : & @{text "theory \<rightarrow> theory"} \\ |
1420 @{command_def (HOL) "consts_code"} & : & @{text "theory \<rightarrow> theory"} \\ |
1421 @{command_def (HOL) "types_code"} & : & @{text "theory \<rightarrow> theory"} \\ |
1421 @{command_def (HOL) "types_code"} & : & @{text "theory \<rightarrow> theory"} \\ |
1422 @{attribute_def (HOL) code} & : & @{text attribute} \\ |
1422 @{attribute_def code} & : & @{text attribute} \\ |
1423 \end{matharray} |
1423 \end{matharray} |
1424 |
1424 |
1425 @{rail " |
1425 @{rail " |
1426 ( @@{command (HOL) code_module} | @@{command (HOL) code_library} ) modespec? @{syntax name}? \\ |
1426 ( @@{command (HOL) code_module} | @@{command (HOL) code_library} ) modespec? @{syntax name}? \\ |
1427 ( @'file' name ) ? ( @'imports' ( @{syntax name} + ) ) ? \\ |
1427 ( @'file' name ) ? ( @'imports' ( @{syntax name} + ) ) ? \\ |
1450 ; |
1450 ; |
1451 |
1451 |
1452 attachment: 'attach' modespec? '{' @{syntax text} '}' |
1452 attachment: 'attach' modespec? '{' @{syntax text} '}' |
1453 ; |
1453 ; |
1454 |
1454 |
1455 @@{attribute (HOL) code} (name)? |
1455 @@{attribute code} name? |
1456 "} |
1456 "} |
1457 *} |
1457 *} |
1458 |
1458 |
1459 |
1459 |
1460 section {* Definition by specification \label{sec:hol-specification} *} |
1460 section {* Definition by specification \label{sec:hol-specification} *} |